# Theory AOT_ExtendedRelationComprehension

```theory AOT_ExtendedRelationComprehension
imports AOT_RestrictedVariables
begin

section‹Extended Relation Comprehension›

text‹This theory depends on choosing extended models.›
interpretation AOT_ExtendedModel by (standard; auto)

text‹Auxiliary lemma: negations of denoting relations denote.›
AOT_theorem negation_denotes: ‹[λx φ{x}]↓ → [λx ¬φ{x}]↓›
proof(rule "→I")
AOT_assume 0: ‹[λx φ{x}]↓›
AOT_show ‹[λx ¬φ{x}]↓›
proof (rule "safe-ext"[axiom_inst, THEN "→E", OF "&I"])
AOT_show ‹[λx ¬[λx φ{x}]x]↓› by "cqt:2"
next
AOT_have ‹□[λx φ{x}]↓›
using 0 "exist-nec"[THEN "→E"] by blast
moreover AOT_have ‹□[λx φ{x}]↓ → □∀x (¬[λx φ{x}]x ≡ ¬φ{x})›
by(rule RM; safe intro!: GEN "≡I" "→I" "β→C"(2) "β←C"(2) "cqt:2")
ultimately AOT_show ‹□∀x (¬[λx φ{x}]x ≡ ¬φ{x})›
using "→E" by blast
qed
qed

text‹Auxiliary lemma: conjunctions of denoting relations denote.›
AOT_theorem conjunction_denotes: ‹[λx φ{x}]↓ & [λx ψ{x}]↓ → [λx φ{x} & ψ{x}]↓›
proof(rule "→I")
AOT_assume 0: ‹[λx φ{x}]↓ & [λx ψ{x}]↓›
AOT_show ‹[λx φ{x} & ψ{x}]↓›
proof (rule "safe-ext"[axiom_inst, THEN "→E", OF "&I"])
AOT_show ‹[λx [λx φ{x}]x & [λx ψ{x}]x]↓› by "cqt:2"
next
AOT_have ‹□([λx φ{x}]↓ & [λx ψ{x}]↓)›
using 0 "exist-nec"[THEN "→E"] "&E"
"KBasic:3" "df-simplify:2" "intro-elim:3:b" by blast
moreover AOT_have
‹□([λx φ{x}]↓ & [λx ψ{x}]↓) → □∀x ([λx φ{x}]x & [λx ψ{x}]x ≡ φ{x} & ψ{x})›
by(rule RM; auto intro!: GEN "≡I" "→I" "cqt:2" "&I"
intro: "β←C"
dest: "&E" "β→C")
ultimately AOT_show ‹□∀x ([λx φ{x}]x & [λx ψ{x}]x ≡ φ{x} & ψ{x})›
using "→E" by blast
qed
qed

AOT_register_rigid_restricted_type
Ordinary: ‹O!κ›
proof
AOT_modally_strict {
AOT_show ‹∃x O!x›
by (meson "B◇" "T◇" "o-objects-exist:1" "→E")
}
next
AOT_modally_strict {
AOT_show ‹O!κ → κ↓› for κ
by (simp add: "→I" "cqt:5:a[1]"[axiom_inst, THEN "→E", THEN "&E"(2)])
}
next
AOT_modally_strict {
AOT_show ‹∀α(O!α → □O!α)›
}
qed

AOT_register_variable_names
Ordinary: u v r t s

text‹In PLM this is defined in the Natural Numbers chapter,
but since it is helpful for stating the comprehension principles,
AOT_define eqE :: ‹τ ⇒ τ ⇒ φ› (infixl ‹≡⇩E› 50)
eqE: ‹F ≡⇩E G ≡⇩d⇩f F↓ & G↓ & ∀u ([F]u ≡ [G]u)›

text‹Derive existence claims about relations from the axioms.›
AOT_theorem denotes_all: ‹[λx ∀G (□G ≡⇩E F → x[G])]↓›
and denotes_all_neg: ‹[λx ∀G (□G ≡⇩E F → ¬x[G])]↓›
proof -
AOT_have Aux: ‹∀F (□F ≡⇩E G → (x[F] ≡ x[G])), ¬(x[G] ≡ y[G])
❙⊢⇩□ ∃F([F]x & ¬[F]y)› for x y G
proof -
AOT_modally_strict {
AOT_assume 0: ‹∀F (□F ≡⇩E G → (x[F] ≡ x[G]))›
AOT_assume G_prop: ‹¬(x[G] ≡ y[G])›
{
AOT_assume ‹¬∃F([F]x & ¬[F]y)›
AOT_hence 0: ‹∀F ¬([F]x & ¬[F]y)›
by (metis "cqt-further:4" "→E")
AOT_have ‹∀F ([F]x ≡ [F]y)›
proof (rule GEN; rule "≡I"; rule "→I")
fix F
AOT_assume ‹[F]x›
moreover AOT_have ‹¬([F]x & ¬[F]y)›
using 0[THEN "∀E"(2)] by blast
ultimately AOT_show ‹[F]y›
by (metis "&I" "raa-cor:1")
next
fix F
AOT_assume ‹[F]y›
AOT_hence ‹¬[λx ¬[F]x]y›
by (metis "¬¬I" "β→C"(2))
moreover AOT_have ‹¬([λx ¬[F]x]x & ¬[λx ¬[F]x]y)›
apply (rule 0[THEN "∀E"(1)]) by "cqt:2[lambda]"
ultimately AOT_have 1: ‹¬[λx ¬[F]x]x›
by (metis "&I" "raa-cor:3")
{
AOT_assume ‹¬[F]x›
AOT_hence ‹[λx ¬[F]x]x›
by (auto intro!: "β←C"(1) "cqt:2")
AOT_hence ‹p & ¬p› for p
using 1 by (metis "raa-cor:3")
}
AOT_thus ‹[F]x› by (metis "raa-cor:1")
qed
AOT_hence ‹□∀F ([F]x ≡ [F]y)›
using "ind-nec"[THEN "→E"] by blast
AOT_hence ‹∀F □([F]x ≡ [F]y)›
by (metis "CBF" "→E")
} note indistI = this
{
AOT_assume G_prop: ‹x[G] & ¬y[G]›
AOT_hence Ax: ‹A!x›
using "&E"(1) "∃I"(2) "→E" "encoders-are-abstract" by blast

{
AOT_assume Ay: ‹A!y›
{
fix F
{
AOT_assume ‹∀u□([F]u ≡ [G]u)›
AOT_hence ‹□∀u([F]u ≡ [G]u)›
using "Ordinary.res-var-bound-reas[BF]"[THEN "→E"] by simp
AOT_hence ‹□F ≡⇩E G›
by (AOT_subst ‹F ≡⇩E G› ‹∀u ([F]u ≡ [G]u)›)
(auto intro!: "eqE"[THEN "≡Df", THEN "≡S"(1), OF "&I"] "cqt:2")
AOT_hence ‹x[F] ≡ x[G]›
using 0[THEN "∀E"(2)] "≡E" "→E" by meson
AOT_hence ‹x[F]›
using G_prop "&E" "≡E" by blast
}
AOT_hence ‹∀u□([F]u ≡ [G]u) → x[F]›
by (rule "→I")
}
AOT_hence xprop: ‹∀F(∀u□([F]u ≡ [G]u) → x[F])›
by (rule GEN)
moreover AOT_have yprop: ‹¬∀F(∀u□([F]u ≡ [G]u) → y[F])›
proof (rule "raa-cor:2")
AOT_assume ‹∀F(∀u□([F]u ≡ [G]u) → y[F])›
AOT_hence ‹∀F(□∀u([F]u ≡ [G]u) → y[F])›
apply (AOT_subst ‹□∀u([F]u ≡ [G]u)› ‹∀u□([F]u ≡ [G]u)› for: F)
using "Ordinary.res-var-bound-reas[BF]"
"Ordinary.res-var-bound-reas[CBF]"
"intro-elim:2" apply presburger
by simp
AOT_hence A: ‹∀F(□F ≡⇩E G → y[F])›
by (AOT_subst ‹F ≡⇩E G› ‹∀u ([F]u ≡ [G]u)› for: F)
(auto intro!: "eqE"[THEN "≡Df", THEN "≡S"(1), OF "&I"] "cqt:2")
moreover AOT_have ‹□G ≡⇩E G›
by (auto intro!: "eqE"[THEN "≡⇩d⇩fI"] "cqt:2" RN "&I" GEN "→I" "≡I")
ultimately AOT_have ‹y[G]› using "∀E"(2) "→E" by blast
AOT_thus ‹p & ¬p› for p using G_prop "&E" by (metis "raa-cor:3")
qed
AOT_have ‹∃F([F]x & ¬[F]y)›
proof(rule "raa-cor:1")
AOT_assume ‹¬∃F([F]x & ¬[F]y)›
AOT_hence indist: ‹∀F □([F]x ≡ [F]y)› using indistI by blast
AOT_have ‹∀F(∀u□([F]u ≡ [G]u) → y[F])›
using indistinguishable_ord_enc_all[axiom_inst, THEN "→E", OF "&I",
OF "&I", OF "&I", OF "cqt:2[const_var]"[axiom_inst],
OF Ax, OF Ay, OF indist, THEN "≡E"(1), OF xprop].
AOT_thus ‹∀F(∀u□([F]u ≡ [G]u) → y[F]) & ¬∀F(∀u□([F]u ≡ [G]u) → y[F])›
using yprop "&I" by blast
qed
}
moreover {
AOT_assume notAy: ‹¬A!y›
AOT_have ‹∃F([F]x & ¬[F]y)›
apply (rule "∃I"(1)[where τ=‹«A!»›])
using Ax notAy "&I" apply blast
}
ultimately AOT_have ‹∃F([F]x & ¬[F]y)›
by (metis "raa-cor:1")
}
moreover {
AOT_assume G_prop: ‹¬x[G] & y[G]›
AOT_hence Ay: ‹A!y›
by (meson "&E"(2) "encoders-are-abstract" "existential:2[const_var]" "→E")
AOT_hence notOy: ‹¬O!y›
using "≡E"(1) "oa-contingent:3" by blast
{
AOT_assume Ax: ‹A!x›
{
fix F
{
AOT_assume ‹□∀u([F]u ≡ [G]u)›
AOT_hence ‹□F ≡⇩E G›
by (AOT_subst ‹F ≡⇩E G› ‹∀u([F]u ≡ [G]u)›)
(auto intro!: "eqE"[THEN "≡Df", THEN "≡S"(1), OF "&I"] "cqt:2")
AOT_hence ‹x[F] ≡ x[G]›
using 0[THEN "∀E"(2)] "≡E" "→E" by meson
AOT_hence ‹¬x[F]›
using G_prop "&E" "≡E" by blast
}
AOT_hence ‹□∀u([F]u ≡ [G]u) → ¬x[F]›
by (rule "→I")
}
AOT_hence x_prop: ‹∀F(□∀u([F]u ≡ [G]u) → ¬x[F])›
by (rule GEN)
AOT_have x_prop: ‹¬∃F(∀u□([F]u ≡ [G]u) & x[F])›
proof (rule "raa-cor:2")
AOT_assume ‹∃F(∀u □([F]u ≡ [G]u) & x[F])›
then AOT_obtain F where F_prop: ‹∀u □([F]u ≡ [G]u) & x[F]›
using "∃E"[rotated] by blast
AOT_have ‹□([F]u ≡ [G]u)› for u
using F_prop[THEN "&E"(1), THEN "Ordinary.∀E"].
AOT_hence ‹∀u □([F]u ≡ [G]u)›
by (rule Ordinary.GEN)
AOT_hence ‹□∀u([F]u ≡ [G]u)›
by (metis "Ordinary.res-var-bound-reas[BF]" "→E")
AOT_hence ‹¬x[F]›
using x_prop[THEN "∀E"(2), THEN "→E"] by blast
AOT_thus ‹p & ¬p› for p
using F_prop[THEN "&E"(2)] by (metis "raa-cor:3")
qed
AOT_have y_prop: ‹∃F(∀u □([F]u ≡ [G]u) & y[F])›
proof (rule "raa-cor:1")
AOT_assume ‹¬∃F (∀u □([F]u ≡ [G]u) & y[F])›
AOT_hence 0: ‹∀F ¬(∀u □([F]u ≡ [G]u) & y[F])›
using "cqt-further:4"[THEN "→E"] by blast
{
fix F
{
AOT_assume ‹∀u □([F]u ≡ [G]u)›
AOT_hence ‹¬y[F]›
using 0[THEN "∀E"(2)] "&I" "raa-cor:1" by meson
}
AOT_hence ‹(∀u □([F]u ≡ [G]u) → ¬y[F])›
by (rule "→I")
}
AOT_hence A: ‹∀F(∀u □([F]u ≡ [G]u) → ¬y[F])›
by (rule GEN)
moreover AOT_have ‹∀u □([G]u ≡ [G]u)›
by (simp add: RN "oth-class-taut:3:a" "universal-cor" "→I")
ultimately AOT_have ‹¬y[G]›
using "∀E"(2) "→E" by blast
AOT_thus ‹p & ¬p› for p
using G_prop "&E" by (metis "raa-cor:3")
qed
AOT_have ‹∃F([F]x & ¬[F]y)›
proof(rule "raa-cor:1")
AOT_assume ‹¬∃F([F]x & ¬[F]y)›
AOT_hence indist: ‹∀F □([F]x ≡ [F]y)›
using indistI by blast
AOT_thus ‹∃F(∀u □([F]u ≡ [G]u) & x[F]) & ¬∃F(∀u □([F]u ≡ [G]u) & x[F])›
using indistinguishable_ord_enc_ex[axiom_inst, THEN "→E", OF "&I",
OF "&I", OF "&I", OF "cqt:2[const_var]"[axiom_inst],
OF Ax, OF Ay, OF indist, THEN "≡E"(2), OF y_prop]
x_prop "&I" by blast
qed
}
moreover {
AOT_assume notAx: ‹¬A!x›
AOT_hence Ox: ‹O!x›
using "∨E"(3) "oa-exist:3" by blast
AOT_have ‹∃F([F]x & ¬[F]y)›
apply (rule "∃I"(1)[where τ=‹«O!»›])
using Ox notOy "&I" apply blast
}
ultimately AOT_have ‹∃F([F]x & ¬[F]y)›
by (metis "raa-cor:1")
}
ultimately AOT_show ‹∃F([F]x & ¬[F]y)›
using G_prop by (metis "&I" "→I" "≡I" "raa-cor:1")
}
qed

AOT_modally_strict {
fix x y
AOT_assume indist: ‹∀F ([F]x ≡ [F]y)›
AOT_hence nec_indist: ‹□∀F ([F]x ≡ [F]y)›
using "ind-nec" "vdash-properties:10" by blast
AOT_hence indist_nec: ‹∀F □([F]x ≡ [F]y)›
using "CBF" "vdash-properties:10" by blast
AOT_assume 0: ‹∀G (□G ≡⇩E F → x[G])›
AOT_hence 1: ‹∀G (□∀u ([G]u ≡ [F]u) → x[G])›
by (AOT_subst (reverse) ‹∀u ([G]u ≡ [F]u)› ‹G ≡⇩E F› for: G)
(auto intro!: "eqE"[THEN "≡Df", THEN "≡S"(1), OF "&I"] "cqt:2")
AOT_have ‹x[F]›
by (safe intro!: 1[THEN "∀E"(2), THEN "→E"] GEN "→I" RN "≡I")
AOT_have ‹∀G (□G ≡⇩E F → y[G])›
proof(rule "raa-cor:1")
AOT_assume ‹¬∀G (□G ≡⇩E F → y[G])›
AOT_hence ‹∃G ¬(□G ≡⇩E F → y[G])›
using "cqt-further:2" "→E" by blast
then AOT_obtain G where G_prop: ‹¬(□G ≡⇩E F → y[G])›
using "∃E"[rotated] by blast
AOT_hence 1: ‹□G ≡⇩E F & ¬y[G]›
by (metis "≡E"(1) "oth-class-taut:1:b")
AOT_have xG: ‹x[G]›
using 0[THEN "∀E"(2), THEN "→E"] 1[THEN "&E"(1)] by blast
AOT_hence ‹x[G] & ¬y[G]›
using 1[THEN "&E"(2)] "&I" by blast
AOT_hence B: ‹¬(x[G] ≡ y[G])›
using "&E"(2) "≡E"(1) "reductio-aa:1" xG by blast
{
fix H
{
AOT_assume ‹□H ≡⇩E G›
AOT_hence ‹□(H ≡⇩E G & G ≡⇩E F)›
using 1 by (metis "KBasic:3" "con-dis-i-e:1" "con-dis-i-e:2:a"
"intro-elim:3:b")
moreover AOT_have ‹□(H ≡⇩E G & G ≡⇩E F) → □(H ≡⇩E F)›
proof(rule RM)
AOT_modally_strict {
AOT_show ‹H ≡⇩E G & G ≡⇩E F → H ≡⇩E F›
proof (safe intro!: "→I" "eqE"[THEN "≡⇩d⇩fI"] "&I" "cqt:2" Ordinary.GEN)
fix u
AOT_assume ‹H ≡⇩E G & G ≡⇩E F›
AOT_hence ‹∀u ([H]u ≡ [G]u)› and ‹∀u ([G]u ≡ [F]u)›
using "eqE"[THEN "≡⇩d⇩fE"] "&E" by blast+
AOT_thus ‹[H]u ≡ [F]u›
by (auto dest!: "Ordinary.∀E" dest: "≡E")
qed
}
qed
ultimately AOT_have ‹□(H ≡⇩E F)›
using "→E" by blast
AOT_hence ‹x[H]›
using 0[THEN "∀E"(2)] "→E" by blast
AOT_hence ‹x[H] ≡ x[G]›
using xG "≡I" "→I" by blast
}
AOT_hence ‹□H ≡⇩E G → (x[H] ≡ x[G])› by (rule "→I")
}
AOT_hence A: ‹∀H(□H ≡⇩E G → (x[H] ≡ x[G]))›
by (rule GEN)
then AOT_obtain F where F_prop: ‹[F]x & ¬[F]y›
using Aux[OF A, OF B] "∃E"[rotated] by blast
moreover AOT_have ‹[F]y›
using indist[THEN "∀E"(2), THEN "≡E"(1), OF F_prop[THEN "&E"(1)]].
AOT_thus ‹p & ¬p› for p
using F_prop[THEN "&E"(2)] by (metis "raa-cor:3")
qed
} note 0 = this
AOT_modally_strict {
fix x y
AOT_assume ‹∀F ([F]x ≡ [F]y)›
moreover AOT_have ‹∀F ([F]y ≡ [F]x)›
by (metis calculation "cqt-basic:11" "≡E"(2))
ultimately AOT_have ‹∀G (□G ≡⇩E F → x[G]) ≡ ∀G (□G ≡⇩E F → y[G])›
using 0 "≡I" "→I" by auto
} note 1 = this
AOT_show ‹[λx ∀G (□G ≡⇩E F → x[G])]↓›
by (safe intro!: RN GEN "→I" 1 "kirchner-thm:2"[THEN "≡E"(2)])

AOT_modally_strict {
fix x y
AOT_assume indist: ‹∀F ([F]x ≡ [F]y)›
AOT_hence nec_indist: ‹□∀F ([F]x ≡ [F]y)›
using "ind-nec" "vdash-properties:10" by blast
AOT_hence indist_nec: ‹∀F □([F]x ≡ [F]y)›
using "CBF" "vdash-properties:10" by blast
AOT_assume 0: ‹∀G (□G ≡⇩E F → ¬x[G])›
AOT_hence 1: ‹∀G (□∀u ([G]u ≡ [F]u) → ¬x[G])›
by (AOT_subst (reverse) ‹∀u ([G]u ≡ [F]u)› ‹G ≡⇩E F› for: G)
(auto intro!: "eqE"[THEN "≡Df", THEN "≡S"(1), OF "&I"] "cqt:2")
AOT_have ‹¬x[F]›
by (safe intro!: 1[THEN "∀E"(2), THEN "→E"] GEN "→I" RN "≡I")
AOT_have ‹∀G (□G ≡⇩E F → ¬y[G])›
proof(rule "raa-cor:1")
AOT_assume ‹¬∀G (□G ≡⇩E F → ¬y[G])›
AOT_hence ‹∃G ¬(□G ≡⇩E F → ¬y[G])›
using "cqt-further:2" "→E" by blast
then AOT_obtain G where G_prop: ‹¬(□G ≡⇩E F → ¬y[G])›
using "∃E"[rotated] by blast
AOT_hence 1: ‹□G ≡⇩E F & ¬¬y[G]›
by (metis "≡E"(1) "oth-class-taut:1:b")
AOT_hence yG: ‹y[G]›
using G_prop "→I" "raa-cor:3" by blast
moreover AOT_hence 12: ‹¬x[G]›
using 0[THEN "∀E"(2), THEN "→E"] 1[THEN "&E"(1)] by blast
ultimately AOT_have ‹¬x[G] & y[G]›
using "&I" by blast
AOT_hence B: ‹¬(x[G] ≡ y[G])›
by (metis "12" "≡E"(3) "raa-cor:3" yG)
{
fix H
{
AOT_assume 3: ‹□H ≡⇩E G›
AOT_hence ‹□(H ≡⇩E G & G ≡⇩E F)›
using 1
by (metis "KBasic:3" "con-dis-i-e:1" "→I" "intro-elim:3:b"
"reductio-aa:1" G_prop)
moreover AOT_have ‹□(H ≡⇩E G & G ≡⇩E F) → □(H ≡⇩E F)›
proof (rule RM)
AOT_modally_strict {
AOT_show ‹H ≡⇩E G & G ≡⇩E F → H ≡⇩E F›
proof (safe intro!: "→I" "eqE"[THEN "≡⇩d⇩fI"] "&I" "cqt:2" Ordinary.GEN)
fix u
AOT_assume ‹H ≡⇩E G & G ≡⇩E F›
AOT_hence ‹∀u ([H]u ≡ [G]u)› and ‹∀u ([G]u ≡ [F]u)›
using "eqE"[THEN "≡⇩d⇩fE"] "&E" by blast+
AOT_thus ‹[H]u ≡ [F]u›
by (auto dest!: "Ordinary.∀E" dest: "≡E")
qed
}
qed
ultimately AOT_have ‹□(H ≡⇩E F)›
using "→E" by blast
AOT_hence ‹¬x[H]›
using 0[THEN "∀E"(2)] "→E" by blast
AOT_hence ‹x[H] ≡ x[G]›
using 12 "≡I" "→I" by (metis "raa-cor:3")
}
AOT_hence ‹□H ≡⇩E G → (x[H] ≡ x[G])›
by (rule "→I")
}
AOT_hence A: ‹∀H(□H ≡⇩E G → (x[H] ≡ x[G]))›
by (rule GEN)
then AOT_obtain F where F_prop: ‹[F]x & ¬[F]y›
using Aux[OF A, OF B] "∃E"[rotated] by blast
moreover AOT_have ‹[F]y›
using indist[THEN "∀E"(2), THEN "≡E"(1), OF F_prop[THEN "&E"(1)]].
AOT_thus ‹p & ¬p› for p
using F_prop[THEN "&E"(2)] by (metis "raa-cor:3")
qed
} note 0 = this
AOT_modally_strict {
fix x y
AOT_assume ‹∀F ([F]x ≡ [F]y)›
moreover AOT_have ‹∀F ([F]y ≡ [F]x)›
by (metis calculation "cqt-basic:11" "≡E"(2))
ultimately AOT_have ‹∀G (□G ≡⇩E F → ¬x[G]) ≡ ∀G (□G ≡⇩E F → ¬y[G])›
using 0 "≡I" "→I" by auto
} note 1 = this
AOT_show ‹[λx ∀G (□G ≡⇩E F → ¬x[G])]↓›
by (safe intro!: RN GEN "→I" 1 "kirchner-thm:2"[THEN "≡E"(2)])
qed

text‹Reformulate the existence claims in terms of their negations.›

AOT_theorem denotes_ex: ‹[λx ∃G (□G ≡⇩E F & x[G])]↓›
proof (rule "safe-ext"[axiom_inst, THEN "→E", OF "&I"])
AOT_show ‹[λx ¬∀G (□G ≡⇩E F → ¬x[G])]↓›
using denotes_all_neg[THEN negation_denotes[THEN "→E"]].
next
AOT_show ‹□∀x (¬∀G (□G ≡⇩E F → ¬x[G]) ≡ ∃G (□G ≡⇩E F & x[G]))›
by (AOT_subst  ‹□G ≡⇩E F & x[G]› ‹¬(□G ≡⇩E F → ¬x[G])› for: G x)
(auto simp: "conventions:1" "rule-eq-df:1"
intro: "oth-class-taut:4:b"[THEN "≡E"(2)]
"intro-elim:3:f"[OF "cqt-further:3", OF "oth-class-taut:3:b"]
intro!: RN GEN)
qed

AOT_theorem denotes_ex_neg: ‹[λx ∃G (□G ≡⇩E F & ¬x[G])]↓›
proof (rule "safe-ext"[axiom_inst, THEN "→E", OF "&I"])
AOT_show ‹[λx ¬∀G (□G ≡⇩E F → x[G])]↓›
using denotes_all[THEN negation_denotes[THEN "→E"]].
next
AOT_show ‹□∀x (¬∀G (□G ≡⇩E F → x[G]) ≡ ∃G (□G ≡⇩E F & ¬x[G]))›
by (AOT_subst (reverse) ‹□G ≡⇩E F & ¬x[G]› ‹¬(□G ≡⇩E F → x[G])› for: G x)
(auto simp: "oth-class-taut:1:b"
intro: "oth-class-taut:4:b"[THEN "≡E"(2)]
"intro-elim:3:f"[OF "cqt-further:3", OF "oth-class-taut:3:b"]
intro!: RN GEN)
qed

text‹Derive comprehension principles.›

AOT_theorem Comprehension_1:
shows ‹□∀F∀G(□G ≡⇩E F → (φ{F} ≡ φ{G})) → [λx ∃F (φ{F} & x[F])]↓›
proof(rule "→I")
AOT_assume assm: ‹□∀F∀G(□G ≡⇩E F → (φ{F} ≡ φ{G}))›
AOT_modally_strict {
fix x y
AOT_assume 0: ‹∀F∀G (□G ≡⇩E F → (φ{F} ≡ φ{G}))›
AOT_assume indist: ‹∀F ([F]x ≡ [F]y)›
AOT_assume x_prop: ‹∃F (φ{F} & x[F])›
then AOT_obtain F where F_prop: ‹φ{F} & x[F]›
using "∃E"[rotated] by blast
AOT_hence ‹□F ≡⇩E F & x[F]›
by (auto intro!: RN eqE[THEN "≡⇩d⇩fI"] "&I" "cqt:2" GEN "≡I" "→I" dest: "&E")
AOT_hence ‹∃G(□G ≡⇩E F & x[G])›
by (rule "∃I")
AOT_hence ‹[λx ∃G(□G ≡⇩E F & x[G])]x›
by (safe intro!: "β←C" denotes_ex "cqt:2")
AOT_hence ‹[λx ∃G(□G ≡⇩E F & x[G])]y›
using indist[THEN "∀E"(1), OF denotes_ex, THEN "≡E"(1)] by blast
AOT_hence ‹∃G(□G ≡⇩E F & y[G])›
using "β→C" by blast
then AOT_obtain G where ‹□G ≡⇩E F & y[G]›
using "∃E"[rotated] by blast
AOT_hence ‹φ{G} & y[G]›
using 0[THEN "∀E"(2), THEN "∀E"(2), THEN "→E", THEN "≡E"(1)]
F_prop[THEN "&E"(1)] "&E" "&I" by blast
AOT_hence ‹∃F (φ{F} & y[F])›
by (rule "∃I")
} note 1 = this
AOT_modally_strict {
AOT_assume 0: ‹∀F∀G (□G ≡⇩E F → (φ{F} ≡ φ{G}))›
{
fix x y
{
AOT_assume ‹∀F ([F]x ≡ [F]y)›
moreover AOT_have ‹∀F ([F]y ≡ [F]x)›
by (metis calculation "cqt-basic:11" "≡E"(1))
ultimately AOT_have ‹∃F (φ{F} & x[F]) ≡ ∃F (φ{F} & y[F])›
using 0 1[OF 0] "≡I" "→I" by simp
}
AOT_hence ‹∀F ([F]x ≡ [F]y) → (∃F (φ{F} & x[F]) ≡ ∃F (φ{F} & y[F]))›
using "→I" by blast
}
AOT_hence ‹∀x∀y(∀F ([F]x ≡ [F]y) → (∃F (φ{F} & x[F]) ≡  ∃F (φ{F} & y[F])))›
by (auto intro!: GEN)
} note 1 = this
AOT_hence ‹❙⊢⇩□ ∀F∀G (□G ≡⇩E F → (φ{F} ≡ φ{G})) →
∀x∀y(∀F ([F]x ≡ [F]y) → (∃F (φ{F} & x[F]) ≡ ∃F (φ{F} & y[F])))›
by (rule "→I")
AOT_hence ‹□∀F∀G (□G ≡⇩E F → (φ{F} ≡ φ{G})) →
□∀x∀y(∀F ([F]x ≡ [F]y) → (∃F (φ{F} & x[F]) ≡ ∃F (φ{F} & y[F])))›
by (rule RM)
AOT_hence ‹□∀x∀y(∀F ([F]x ≡ [F]y) → (∃F (φ{F} & x[F]) ≡ ∃F (φ{F} & y[F])))›
using "→E" assm by blast
AOT_thus ‹[λx ∃F (φ{F} & x[F])]↓›
by (safe intro!: "kirchner-thm:2"[THEN "≡E"(2)])
qed

AOT_theorem Comprehension_2:
shows ‹□∀F∀G(□G ≡⇩E F → (φ{F} ≡ φ{G})) → [λx ∃F (φ{F} & ¬x[F])]↓›
proof(rule "→I")
AOT_assume assm: ‹□∀F∀G(□G ≡⇩E F → (φ{F} ≡ φ{G}))›
AOT_modally_strict {
fix x y
AOT_assume 0: ‹∀F∀G (□G ≡⇩E F → (φ{F} ≡ φ{G}))›
AOT_assume indist: ‹∀F ([F]x ≡ [F]y)›
AOT_assume x_prop: ‹∃F (φ{F} & ¬x[F])›
then AOT_obtain F where F_prop: ‹φ{F} & ¬x[F]›
using "∃E"[rotated] by blast
AOT_hence ‹□F ≡⇩E F & ¬x[F]›
by (auto intro!: RN eqE[THEN "≡⇩d⇩fI"] "&I" "cqt:2" GEN "≡I" "→I" dest: "&E")
AOT_hence ‹∃G(□G ≡⇩E F & ¬x[G])›
by (rule "∃I")
AOT_hence ‹[λx ∃G(□G ≡⇩E F & ¬x[G])]x›
by (safe intro!: "β←C" denotes_ex_neg "cqt:2")
AOT_hence ‹[λx ∃G(□G ≡⇩E F & ¬x[G])]y›
using indist[THEN "∀E"(1), OF denotes_ex_neg, THEN "≡E"(1)] by blast
AOT_hence ‹∃G(□G ≡⇩E F & ¬y[G])›
using "β→C" by blast
then AOT_obtain G where ‹□G ≡⇩E F & ¬y[G]›
using "∃E"[rotated] by blast
AOT_hence ‹φ{G} & ¬y[G]›
using 0[THEN "∀E"(2), THEN "∀E"(2), THEN "→E", THEN "≡E"(1)]
F_prop[THEN "&E"(1)] "&E" "&I" by blast
AOT_hence ‹∃F (φ{F} & ¬y[F])›
by (rule "∃I")
} note 1 = this
AOT_modally_strict {
AOT_assume 0: ‹∀F∀G (□G ≡⇩E F → (φ{F} ≡ φ{G}))›
{
fix x y
{
AOT_assume ‹∀F ([F]x ≡ [F]y)›
moreover AOT_have ‹∀F ([F]y ≡ [F]x)›
by (metis calculation "cqt-basic:11" "≡E"(1))
ultimately AOT_have ‹∃F (φ{F} & ¬x[F]) ≡ ∃F (φ{F} & ¬y[F])›
using 0 1[OF 0] "≡I" "→I" by simp
}
AOT_hence ‹∀F ([F]x ≡ [F]y) → (∃F (φ{F} & ¬x[F]) ≡ ∃F (φ{F} & ¬y[F]))›
using "→I" by blast
}
AOT_hence ‹∀x∀y(∀F ([F]x ≡ [F]y) → (∃F (φ{F} & ¬x[F]) ≡  ∃F (φ{F} & ¬y[F])))›
by (auto intro!: GEN)
} note 1 = this
AOT_hence ‹❙⊢⇩□ ∀F∀G (□G ≡⇩E F → (φ{F} ≡ φ{G})) →
∀x∀y(∀F ([F]x ≡ [F]y) → (∃F (φ{F} & ¬x[F]) ≡ ∃F (φ{F} & ¬y[F])))›
by (rule "→I")
AOT_hence ‹□∀F∀G (□G ≡⇩E F → (φ{F} ≡ φ{G})) →
□∀x∀y(∀F ([F]x ≡ [F]y) → (∃F (φ{F} & ¬x[F]) ≡ ∃F (φ{F} & ¬y[F])))›
by (rule RM)
AOT_hence ‹□∀x∀y(∀F ([F]x ≡ [F]y) → (∃F (φ{F} & ¬x[F]) ≡ ∃F (φ{F} & ¬y[F])))›
using "→E" assm by blast
AOT_thus ‹[λx ∃F (φ{F} & ¬x[F])]↓›
by (safe intro!: "kirchner-thm:2"[THEN "≡E"(2)])
qed

text‹Derived variants of the comprehension principles above.›

AOT_theorem Comprehension_1':
shows ‹□∀F∀G(□G ≡⇩E F → (φ{F} ≡ φ{G})) → [λx ∀F (x[F] → φ{F})]↓›
proof(rule "→I")
AOT_assume ‹□∀F∀G(□G ≡⇩E F → (φ{F} ≡ φ{G}))›
AOT_hence 0: ‹□∀F∀G(□G ≡⇩E F → (¬φ{F} ≡ ¬φ{G}))›
by (AOT_subst (reverse) ‹¬φ{F} ≡ ¬φ{G}› ‹φ{F} ≡ φ{G}› for: F G)
(auto simp: "oth-class-taut:4:b")
AOT_show ‹[λx ∀F (x[F] → φ{F})]↓›
proof(rule "safe-ext"[axiom_inst, THEN "→E", OF "&I"])
AOT_show ‹[λx ¬∃F(¬φ{F} & x[F])]↓›
using Comprehension_1[THEN "→E", OF 0, THEN negation_denotes[THEN "→E"]].
next
AOT_show ‹□∀x (¬∃F (¬φ{F} & x[F]) ≡ ∀F (x[F] → φ{F}))›
by (AOT_subst (reverse) ‹¬φ{F} & x[F]› ‹¬(x[F] → φ{F})› for: F x)
(auto simp: "oth-class-taut:1:b"[THEN "intro-elim:3:e",
OF "oth-class-taut:2:a"]
intro: "intro-elim:3:f"[OF "cqt-further:3", OF "oth-class-taut:3:a",
symmetric]
intro!: RN GEN)
qed
qed

AOT_theorem Comprehension_2':
shows ‹□∀F∀G(□G ≡⇩E F → (φ{F} ≡ φ{G})) → [λx ∀F (φ{F} → x[F])]↓›
proof(rule "→I")
AOT_assume 0: ‹□∀F∀G(□G ≡⇩E F → (φ{F} ≡ φ{G}))›
AOT_show ‹[λx ∀F (φ{F} → x[F])]↓›
proof(rule "safe-ext"[axiom_inst, THEN "→E", OF "&I"])
AOT_show ‹[λx ¬∃F(φ{F} & ¬x[F])]↓›
using Comprehension_2[THEN "→E", OF 0, THEN negation_denotes[THEN "→E"]].
next
AOT_show ‹□∀x (¬∃F (φ{F} & ¬x[F]) ≡ ∀F (φ{F} → x[F]))›
by (AOT_subst (reverse) ‹φ{F} & ¬x[F]› ‹¬(φ{F} → x[F])› for: F x)
(auto simp: "oth-class-taut:1:b"
intro: "intro-elim:3:f"[OF "cqt-further:3", OF "oth-class-taut:3:a",
symmetric]
intro!: RN GEN)
qed
qed

text‹Derive a combined comprehension principles.›

AOT_theorem Comprehension_3:
‹□∀F∀G(□G ≡⇩E F → (φ{F} ≡ φ{G})) → [λx ∀F (x[F] ≡ φ{F})]↓›
proof(rule "→I")
AOT_assume 0: ‹□∀F∀G(□G ≡⇩E F → (φ{F} ≡ φ{G}))›
AOT_show ‹[λx ∀F (x[F] ≡ φ{F})]↓›
proof(rule "safe-ext"[axiom_inst, THEN "→E", OF "&I"])
AOT_show ‹[λx ∀F (x[F] → φ{F}) & ∀F (φ{F} → x[F])]↓›
by (safe intro!: conjunction_denotes[THEN "→E", OF "&I"]
Comprehension_1'[THEN "→E"]
Comprehension_2'[THEN "→E"] 0)
next
AOT_show ‹□∀x (∀F (x[F] → φ{F}) & ∀F (φ{F} → x[F]) ≡ ∀F (x[F] ≡ φ{F}))›
by (auto intro!: RN GEN "≡I" "→I" "&I" dest: "&E" "∀E"(2) "→E" "≡E"(1,2))
qed
qed

begin
text‹Verify that the original axioms are equivalent to @{thm denotes_ex}
and @{thm denotes_ex_neg}.›
AOT_modally_strict {
fix x y H
AOT_have ‹A!x & A!y & ∀F □([F]x ≡ [F]y) →
(∀G (∀z (O!z → □([G]z ≡ [H]z)) → x[G]) ≡
∀G (∀z (O!z → □([G]z ≡ [H]z)) → y[G]))›
proof(rule "→I")
{
fix x y
AOT_assume ‹A!x›
AOT_assume ‹A!y›
AOT_assume indist: ‹∀F □([F]x ≡ [F]y)›
AOT_assume ‹∀G (∀u □([G]u ≡ [H]u) → x[G])›
AOT_hence ‹∀G (□∀u ([G]u ≡ [H]u) → x[G])›
using "Ordinary.res-var-bound-reas[BF]" "Ordinary.res-var-bound-reas[CBF]"
"intro-elim:2"
by (AOT_subst ‹□∀u ([G]u ≡ [H]u)› ‹∀u □([G]u ≡ [H]u)› for: G) auto
AOT_hence ‹∀G (□G ≡⇩E H → x[G])›
by (AOT_subst ‹G ≡⇩E H› ‹∀u ([G]u ≡ [H]u)› for: G)
(safe intro!: "eqE"[THEN "≡Df", THEN "≡S"(1), OF "&I"] "cqt:2")
AOT_hence ‹¬∃G (□G ≡⇩E H & ¬x[G])›
by (AOT_subst (reverse) ‹(□G ≡⇩E H & ¬x[G])› ‹¬(□G ≡⇩E H → x[G])› for: G)
(auto simp: "oth-class-taut:1:b" "cqt-further:3"[THEN "≡E"(1)])
AOT_hence ‹¬[λx ∃G (□G ≡⇩E H & ¬x[G])]x›
by (auto intro: "β→C")
AOT_hence ‹¬[λx ∃G (□G ≡⇩E H & ¬x[G])]y›
using indist[THEN "∀E"(1), OF denotes_ex_neg,
THEN "qml:2"[axiom_inst, THEN "→E"],
THEN "≡E"(3)] by blast
AOT_hence ‹¬∃G (□G ≡⇩E H & ¬y[G])›
by (safe intro!: "β←C" denotes_ex_neg "cqt:2")
AOT_hence ‹∀G ¬(□G ≡⇩E H & ¬y[G])›
using "cqt-further:4"[THEN "→E"] by blast
AOT_hence ‹∀G(□G ≡⇩E H → y[G])›
by (AOT_subst ‹□G ≡⇩E H → y[G]› ‹¬(□G ≡⇩E H & ¬y[G])› for: G)
(auto simp: "oth-class-taut:1:a")
AOT_hence ‹∀G (□∀u([G]u ≡ [H]u) → y[G])›
by (AOT_subst (reverse) ‹∀u ([G]u ≡ [H]u)› ‹G ≡⇩E H› for: G)
(safe intro!: "eqE"[THEN "≡Df", THEN "≡S"(1), OF "&I"] "cqt:2")
AOT_hence ‹∀G (∀u □([G]u ≡ [H]u) → y[G])›
using "Ordinary.res-var-bound-reas[BF]" "Ordinary.res-var-bound-reas[CBF]"
"intro-elim:2"
by (AOT_subst ‹∀u □([G]u ≡ [H]u)› ‹□∀u ([G]u ≡ [H]u)› for: G) auto
} note 0 = this
AOT_assume ‹A!x & A!y & ∀F □([F]x ≡ [F]y)›
AOT_hence ‹A!x› and ‹A!y› and ‹∀F □([F]x ≡ [F]y)›
using "&E" by blast+
moreover AOT_have ‹∀F □([F]y ≡ [F]x)›
using calculation(3)
apply (safe intro!: CBF[THEN "→E"] dest!: BF[THEN "→E"])
using "RM:3" "cqt-basic:11" "intro-elim:3:b" by fast
ultimately AOT_show ‹∀G (∀u □([G]u ≡ [H]u) → x[G]) ≡
∀G (∀u □([G]u ≡ [H]u) → y[G])›
using 0 by (auto intro!: "≡I" "→I")
qed

AOT_have ‹A!x & A!y & ∀F □([F]x ≡ [F]y) →
(∃G (∀z (O!z → □([G]z ≡ [H]z)) & x[G]) ≡ ∃G (∀z (O!z → □([G]z ≡ [H]z)) & y[G]))›
proof(rule "→I")
{
fix x y
AOT_assume ‹A!x›
AOT_assume ‹A!y›
AOT_assume indist: ‹∀F □([F]x ≡ [F]y)›
AOT_assume x_prop: ‹∃G (∀u □([G]u ≡ [H]u) & x[G])›
AOT_hence ‹∃G (□∀u ([G]u ≡ [H]u) & x[G])›
using "Ordinary.res-var-bound-reas[BF]" "Ordinary.res-var-bound-reas[CBF]"
"intro-elim:2"
by (AOT_subst ‹□∀u ([G]u ≡ [H]u)› ‹∀u □([G]u ≡ [H]u)› for: G) auto
AOT_hence ‹∃G (□G ≡⇩E H & x[G])›
by (AOT_subst ‹G ≡⇩E H› ‹∀u ([G]u ≡ [H]u)› for: G)
(safe intro!: "eqE"[THEN "≡Df", THEN "≡S"(1), OF "&I"] "cqt:2")
AOT_hence ‹[λx ∃G (□G ≡⇩E H & x[G])]x›
by (safe intro!: "β←C" denotes_ex "cqt:2")
AOT_hence ‹[λx ∃G (□G ≡⇩E H & x[G])]y›
using indist[THEN "∀E"(1), OF denotes_ex,
THEN "qml:2"[axiom_inst, THEN "→E"],
THEN "≡E"(1)] by blast
AOT_hence ‹∃G (□G ≡⇩E H & y[G])›
by (rule "β→C")
AOT_hence ‹∃G (□∀u ([G]u ≡ [H]u) & y[G])›
by (AOT_subst (reverse) ‹∀u ([G]u ≡ [H]u)› ‹G ≡⇩E H› for: G)
(safe intro!: "eqE"[THEN "≡Df", THEN "≡S"(1), OF "&I"] "cqt:2")
AOT_hence ‹∃G (∀u □([G]u ≡ [H]u) & y[G])›
using "Ordinary.res-var-bound-reas[BF]"
"Ordinary.res-var-bound-reas[CBF]"
"intro-elim:2"
by (AOT_subst ‹∀u □([G]u ≡ [H]u)› ‹□∀u ([G]u ≡ [H]u)› for: G) auto
} note 0 = this
AOT_assume ‹A!x & A!y & ∀F □([F]x ≡ [F]y)›
AOT_hence ‹A!x› and ‹A!y› and ‹∀F □([F]x ≡ [F]y)›
using "&E" by blast+
moreover AOT_have ‹∀F □([F]y ≡ [F]x)›
using calculation(3)
apply (safe intro!: CBF[THEN "→E"] dest!: BF[THEN "→E"])
using "RM:3" "cqt-basic:11" "intro-elim:3:b" by fast
ultimately AOT_show ‹∃G (∀u □([G]u ≡ [H]u) & x[G]) ≡
∃G (∀u □([G]u ≡ [H]u) & y[G])›
using 0 by (auto intro!: "≡I" "→I")
qed
}
end
end```