# Theory AOT_PossibleWorlds

```(*<*)
theory AOT_PossibleWorlds
imports AOT_PLM AOT_BasicLogicalObjects AOT_RestrictedVariables
begin
(*>*)

section‹Possible Worlds›

AOT_define Situation :: ‹τ ⇒ φ› (‹Situation'(_')›)
situations: ‹Situation(x) ≡⇩d⇩f A!x & ∀F (x[F] → Propositional([F]))›

AOT_theorem "T-sit": ‹TruthValue(x) → Situation(x)›
proof(rule "→I")
AOT_assume ‹TruthValue(x)›
AOT_hence ‹∃p TruthValueOf(x,p)›
using "T-value"[THEN "≡⇩d⇩fE"] by blast
then AOT_obtain p where ‹TruthValueOf(x,p)› using "∃E"[rotated] by blast
AOT_hence θ: ‹A!x & ∀F (x[F] ≡ ∃q((q ≡ p) & F = [λy q]))›
using "tv-p"[THEN "≡⇩d⇩fE"] by blast
AOT_show ‹Situation(x)›
proof(rule situations[THEN "≡⇩d⇩fI"]; safe intro!: "&I" GEN "→I" θ[THEN "&E"(1)])
fix F
AOT_assume ‹x[F]›
AOT_hence ‹∃q((q ≡ p) & F = [λy q])›
using θ[THEN "&E"(2), THEN "∀E"(2)[where β=F], THEN "≡E"(1)] by argo
then AOT_obtain q where ‹(q ≡ p) & F = [λy q]› using "∃E"[rotated] by blast
AOT_hence ‹∃p F = [λy p]› using "&E"(2) "∃I"(2) by metis
AOT_thus ‹Propositional([F])›
by (metis "≡⇩d⇩fI" "prop-prop1")
qed
qed

AOT_theorem "possit-sit:1": ‹Situation(x) ≡ □Situation(x)›
proof(rule "≡I"; rule "→I")
AOT_assume ‹Situation(x)›
AOT_hence 0: ‹A!x & ∀F (x[F] → Propositional([F]))›
using situations[THEN "≡⇩d⇩fE"] by blast
AOT_have 1: ‹□(A!x & ∀F (x[F] → Propositional([F])))›
proof(rule "KBasic:3"[THEN "≡E"(2)]; rule "&I")
AOT_show ‹□A!x› using 0[THEN "&E"(1)] by (metis "oa-facts:2"[THEN "→E"])
next
AOT_have ‹∀F (x[F] → Propositional([F])) → □∀F (x[F] → Propositional([F]))›
by (AOT_subst ‹Propositional([F])› ‹∃p (F = [λy p])› for: F :: ‹<κ>›)
(auto simp: "prop-prop1" "≡Df" "enc-prop-nec:2")
AOT_thus ‹□∀F (x[F] → Propositional([F]))›
using 0[THEN "&E"(2)] "→E" by blast
qed
AOT_show ‹□Situation(x)›
by (AOT_subst ‹Situation(x)› ‹A!x & ∀F (x[F] → Propositional([F]))›)
(auto simp: 1 "≡Df" situations)
next
AOT_show ‹Situation(x)› if ‹□Situation(x)›
using "qml:2"[axiom_inst, THEN "→E", OF that].
qed

AOT_theorem "possit-sit:2": ‹◇Situation(x) ≡ Situation(x)›
using "possit-sit:1"
by (metis "RE◇" "S5Basic:2" "≡E"(1) "≡E"(5) "Commutativity of ≡")

AOT_theorem "possit-sit:3": ‹◇Situation(x) ≡ □Situation(x)›
using "possit-sit:1" "possit-sit:2" by (meson "≡E"(5))

AOT_theorem "possit-sit:4": ‹❙𝒜Situation(x) ≡ Situation(x)›
by (meson "Act-Basic:5" "Act-Sub:2" "RA" "≡E"(1) "≡E"(6) "possit-sit:2")

AOT_theorem "possit-sit:5": ‹Situation(∘p)›
proof (safe intro!: situations[THEN "≡⇩d⇩fI"] "&I" GEN "→I" "prop-prop1"[THEN "≡⇩d⇩fI"])
AOT_have ‹∃F ∘p[F]›
using "tv-id:2"[THEN "prop-enc"[THEN "≡⇩d⇩fE"], THEN "&E"(2)]
"existential:1" "prop-prop2:2" by blast
AOT_thus ‹A!∘p›
by (safe intro!: "encoders-are-abstract"[unvarify x, THEN "→E"]
"t=t-proper:2"[THEN "→E", OF "ext-p-tv:3"])
next
fix F
AOT_assume ‹∘p[F]›
AOT_hence ‹❙ιx(A!x & ∀F (x[F] ≡ ∃q ((q ≡ p) & F = [λy q])))[F]›
using "tv-id:1" "rule=E" by fast
AOT_hence ‹❙𝒜∃q ((q ≡ p) & F = [λy q])›
using "≡E"(1) "desc-nec-encode:1" by fast
AOT_hence ‹∃q ❙𝒜((q ≡ p) & F = [λy q])›
by (metis "Act-Basic:10" "≡E"(1))
then AOT_obtain q where ‹❙𝒜((q ≡ p) & F = [λy q])› using "∃E"[rotated] by blast
AOT_hence ‹❙𝒜F = [λy q]› by (metis "Act-Basic:2" "con-dis-i-e:2:b" "intro-elim:3:a")
AOT_hence ‹F = [λy q]›
using "id-act:1"[unvarify β, THEN "≡E"(2)] by (metis "prop-prop2:2")
AOT_thus ‹∃p F = [λy p]›
using "∃I" by fast
qed

AOT_theorem "possit-sit:6": ‹Situation(⊤)›
proof -
AOT_have true_def: ‹❙⊢⇩□ ⊤ = ❙ιx (A!x & ∀F (x[F] ≡ ∃p(p & F = [λy p])))›
by (simp add: "A-descriptions" "rule-id-df:1[zero]" "the-true:1")
AOT_hence true_den: ‹❙⊢⇩□ ⊤↓›
using "t=t-proper:1" "vdash-properties:6" by blast
AOT_have ‹❙𝒜TruthValue(⊤)›
using "actual-desc:2"[unvarify x, OF true_den, THEN "→E", OF true_def]
using "TV-lem2:1"[unvarify x, OF true_den, THEN "RA",
THEN "act-cond"[THEN "→E"], THEN "→E"]
by blast
AOT_hence ‹❙𝒜Situation(⊤)›
using "T-sit"[unvarify x, OF true_den, THEN "RA",
THEN "act-cond"[THEN "→E"], THEN "→E"] by blast
AOT_thus ‹Situation(⊤)›
using "possit-sit:4"[unvarify x, OF true_den, THEN "≡E"(1)] by blast
qed

AOT_theorem "possit-sit:7": ‹Situation(⊥)›
proof -
AOT_have true_def: ‹❙⊢⇩□ ⊥ = ❙ιx (A!x & ∀F (x[F] ≡ ∃p(¬p & F = [λy p])))›
by (simp add: "A-descriptions" "rule-id-df:1[zero]" "the-true:2")
AOT_hence true_den: ‹❙⊢⇩□ ⊥↓›
using "t=t-proper:1" "vdash-properties:6" by blast
AOT_have ‹❙𝒜TruthValue(⊥)›
using "actual-desc:2"[unvarify x, OF true_den, THEN "→E", OF true_def]
using "TV-lem2:2"[unvarify x, OF true_den, THEN "RA",
THEN "act-cond"[THEN "→E"], THEN "→E"]
by blast
AOT_hence ‹❙𝒜Situation(⊥)›
using "T-sit"[unvarify x, OF true_den, THEN "RA",
THEN "act-cond"[THEN "→E"], THEN "→E"] by blast
AOT_thus ‹Situation(⊥)›
using "possit-sit:4"[unvarify x, OF true_den, THEN "≡E"(1)] by blast
qed

AOT_register_rigid_restricted_type
Situation: ‹Situation(κ)›
proof
AOT_modally_strict {
fix p
AOT_obtain x where ‹TruthValueOf(x,p)›
by (metis "instantiation" "p-has-!tv:1")
AOT_hence ‹∃p TruthValueOf(x,p)› by (rule "∃I")
AOT_hence ‹TruthValue(x)› by (metis "≡⇩d⇩fI" "T-value")
AOT_hence ‹Situation(x)› using "T-sit"[THEN "→E"] by blast
AOT_thus ‹∃x Situation(x)› by (rule "∃I")
}
next
AOT_modally_strict {
AOT_show ‹Situation(κ) → κ↓› for κ
proof (rule "→I")
AOT_assume ‹Situation(κ)›
AOT_hence ‹A!κ› by (metis "≡⇩d⇩fE" "&E"(1) situations)
AOT_thus ‹κ↓› by (metis "russell-axiom[exe,1].ψ_denotes_asm")
qed
}
next
AOT_modally_strict {
AOT_show ‹∀α(Situation(α) → □Situation(α))›
using "possit-sit:1"[THEN "conventions:3"[THEN "≡⇩d⇩fE"],
THEN "&E"(1)] GEN by fast
}
qed

AOT_register_variable_names
Situation: s

AOT_define TruthInSituation :: ‹τ ⇒ φ ⇒ φ› ("(_ ⊨/ _)" [100, 40] 100)
"true-in-s": ‹s ⊨ p ≡⇩d⇩f s❙Σp›

begin
(* Verify precedence. *)
fix x p q
have ‹«x ⊨ p → q» = «(x ⊨ p) → q»›
by simp
have ‹«x ⊨ p & q» = «(x ⊨ p) & q»›
by simp
have ‹«x ⊨ ¬p» = «x ⊨ (¬p)»›
by simp
have ‹«x ⊨ □p» = «x ⊨ (□p)»›
by simp
have ‹«x ⊨ ❙𝒜p» = «x ⊨ (❙𝒜p)»›
by simp
have ‹«□x ⊨ p» = «□(x ⊨ p)»›
by simp
have ‹«¬x ⊨ p» = «¬(x ⊨ p)»›
by simp
end

AOT_theorem lem1: ‹Situation(x) → (x ⊨ p ≡ x[λy p])›
proof (rule "→I"; rule "≡I"; rule "→I")
AOT_assume ‹Situation(x)›
AOT_assume ‹x ⊨ p›
AOT_hence ‹x❙Σp›
using "true-in-s"[THEN "≡⇩d⇩fE"] "&E" by blast
AOT_thus ‹x[λy p]› using "prop-enc"[THEN "≡⇩d⇩fE"] "&E" by blast
next
AOT_assume 1: ‹Situation(x)›
AOT_assume ‹x[λy p]›
AOT_hence ‹x❙Σp›
using "prop-enc"[THEN "≡⇩d⇩fI", OF "&I", OF "cqt:2"(1)] by blast
AOT_thus ‹x ⊨ p›
using "true-in-s"[THEN "≡⇩d⇩fI"] 1 "&I" by blast
qed

AOT_theorem "lem2:1": ‹s ⊨ p ≡ □s ⊨ p›
proof -
AOT_have sit: ‹Situation(s)›
AOT_have ‹s ⊨ p ≡ s[λy p]›
using lem1[THEN "→E", OF sit] by blast
also AOT_have ‹… ≡ □s[λy p]›
by (rule "en-eq:2"[unvarify F]) "cqt:2[lambda]"
also AOT_have ‹… ≡ □s ⊨ p›
using lem1[THEN RM, THEN "→E", OF "possit-sit:1"[THEN "≡E"(1), OF sit]]
by (metis "KBasic:6" "≡E"(2) "Commutativity of ≡" "→E")
finally show ?thesis.
qed

AOT_theorem "lem2:2": ‹◇s ⊨ p ≡ s ⊨ p›
proof -
AOT_have ‹□(s ⊨ p → □s ⊨ p)›
using "possit-sit:1"[THEN "≡E"(1), OF Situation.ψ]
"lem2:1"[THEN "conventions:3"[THEN "≡⇩d⇩fE", THEN "&E"(1)]]
RM[OF "→I", THEN "→E"] by blast
thus ?thesis by (metis "B◇" "S5Basic:13" "T◇" "≡I" "≡E"(1) "→E")
qed

AOT_theorem "lem2:3": ‹◇s ⊨ p ≡ □s ⊨ p›
using "lem2:1" "lem2:2" by (metis "≡E"(5))

AOT_theorem "lem2:4": ‹❙𝒜(s ⊨ p) ≡ s ⊨ p›
proof -
AOT_have ‹□(s ⊨ p → □s ⊨ p)›
using "possit-sit:1"[THEN "≡E"(1), OF Situation.ψ]
"lem2:1"[THEN "conventions:3"[THEN "≡⇩d⇩fE", THEN "&E"(1)]]
RM[OF "→I", THEN "→E"] by blast
thus ?thesis
using "sc-eq-fur:2"[THEN "→E"] by blast
qed

AOT_theorem "lem2:5": ‹¬s ⊨ p ≡ □¬s ⊨ p›
by (metis "KBasic2:1" "contraposition:1" "→I" "≡I" "≡E"(3) "≡E"(4) "lem2:2")

AOT_theorem "sit-identity": ‹s = s' ≡ ∀p(s ⊨ p ≡ s' ⊨ p)›
proof(rule "≡I"; rule "→I")
AOT_assume ‹s = s'›
moreover AOT_have ‹∀p(s ⊨ p ≡ s ⊨ p)›
ultimately AOT_show ‹∀p(s ⊨ p ≡ s' ⊨ p)›
using "rule=E" by fast
next
AOT_assume a: ‹∀p (s ⊨ p ≡ s' ⊨ p)›
AOT_show ‹s = s'›
proof(safe intro!: "ab-obey:1"[THEN "→E", THEN "→E"] "&I" GEN "≡I" "→I")
AOT_show ‹A!s› using Situation.ψ "≡⇩d⇩fE" "&E"(1) situations by blast
next
AOT_show ‹A!s'› using Situation.ψ "≡⇩d⇩fE" "&E"(1) situations by blast
next
fix F
AOT_assume 0: ‹s[F]›
AOT_hence ‹∃p (F = [λy p])›
using Situation.ψ[THEN situations[THEN "≡⇩d⇩fE"], THEN "&E"(2),
THEN "∀E"(2)[where β=F], THEN "→E"]
"prop-prop1"[THEN "≡⇩d⇩fE"] by blast
then AOT_obtain p where F_def: ‹F = [λy p]›
using "∃E" by metis
AOT_hence ‹s[λy p]›
using 0 "rule=E" by blast
AOT_hence ‹s ⊨ p›
using lem1[THEN "→E", OF Situation.ψ, THEN "≡E"(2)] by blast
AOT_hence ‹s' ⊨ p›
using a[THEN "∀E"(2)[where β=p], THEN "≡E"(1)] by blast
AOT_hence ‹s'[λy p]›
using lem1[THEN "→E", OF Situation.ψ, THEN "≡E"(1)] by blast
AOT_thus ‹s'[F]›
using F_def[symmetric] "rule=E" by blast
next
fix F
AOT_assume 0: ‹s'[F]›
AOT_hence ‹∃p (F = [λy p])›
using Situation.ψ[THEN situations[THEN "≡⇩d⇩fE"], THEN "&E"(2),
THEN "∀E"(2)[where β=F], THEN "→E"]
"prop-prop1"[THEN "≡⇩d⇩fE"] by blast
then AOT_obtain p where F_def: ‹F = [λy p]›
using "∃E" by metis
AOT_hence ‹s'[λy p]›
using 0 "rule=E" by blast
AOT_hence ‹s' ⊨ p›
using lem1[THEN "→E", OF Situation.ψ, THEN "≡E"(2)] by blast
AOT_hence ‹s ⊨ p›
using a[THEN "∀E"(2)[where β=p], THEN "≡E"(2)] by blast
AOT_hence ‹s[λy p]›
using lem1[THEN "→E", OF Situation.ψ, THEN "≡E"(1)] by blast
AOT_thus ‹s[F]›
using F_def[symmetric] "rule=E" by blast
qed
qed

AOT_define PartOfSituation :: ‹τ ⇒ τ ⇒ φ› (infixl ‹⊴› 80)
"sit-part-whole": ‹s ⊴ s' ≡⇩d⇩f ∀p (s ⊨ p → s' ⊨ p)›

AOT_theorem "part:1": ‹s ⊴ s›
by (rule "sit-part-whole"[THEN "≡⇩d⇩fI"])
(safe intro!: "&I" Situation.ψ GEN "→I")

AOT_theorem "part:2": ‹s ⊴ s' & s ≠ s' → ¬(s' ⊴ s)›
proof(rule "→I"; frule "&E"(1); drule "&E"(2); rule "raa-cor:2")
AOT_assume 0: ‹s ⊴ s'›
AOT_hence a: ‹s ⊨ p → s' ⊨ p› for p
using "∀E"(2) "sit-part-whole"[THEN "≡⇩d⇩fE"] "&E" by blast
AOT_assume ‹s' ⊴ s›
AOT_hence b: ‹s' ⊨ p → s ⊨ p› for p
using "∀E"(2) "sit-part-whole"[THEN "≡⇩d⇩fE"] "&E" by blast
AOT_have ‹∀p (s ⊨ p ≡ s' ⊨ p)›
using a b by (simp add: "≡I" "universal-cor")
AOT_hence 1: ‹s = s'›
using "sit-identity"[THEN "≡E"(2)] by metis
AOT_assume ‹s ≠ s'›
AOT_hence ‹¬(s = s')›
by (metis "≡⇩d⇩fE" "=-infix")
AOT_thus ‹s = s' & ¬(s = s')›
using 1 "&I" by blast
qed

AOT_theorem "part:3": ‹s ⊴ s' & s' ⊴ s'' → s ⊴ s''›
proof(rule "→I"; frule "&E"(1); drule "&E"(2);
safe intro!: "&I" GEN "→I" "sit-part-whole"[THEN "≡⇩d⇩fI"] Situation.ψ)
fix p
AOT_assume ‹s ⊨ p›
moreover AOT_assume ‹s ⊴ s'›
ultimately AOT_have ‹s' ⊨ p›
using "sit-part-whole"[THEN "≡⇩d⇩fE", THEN "&E"(2),
THEN "∀E"(2)[where β=p], THEN "→E"] by blast
moreover AOT_assume ‹s' ⊴ s''›
ultimately AOT_show ‹s'' ⊨ p›
using "sit-part-whole"[THEN "≡⇩d⇩fE", THEN "&E"(2),
THEN "∀E"(2)[where β=p], THEN "→E"] by blast
qed

AOT_theorem "sit-identity2:1": ‹s = s' ≡ s ⊴ s' & s' ⊴ s›
proof (safe intro!: "≡I" "&I" "→I")
AOT_show ‹s ⊴ s'› if ‹s = s'›
using "rule=E" "part:1" that by blast
next
AOT_show ‹s' ⊴ s› if ‹s = s'›
using "rule=E" "part:1" that[symmetric] by blast
next
AOT_assume ‹s ⊴ s' & s' ⊴ s›
AOT_thus ‹s = s'› using "part:2"[THEN "→E", OF "&I"]
by (metis "≡⇩d⇩fI" "&E"(1) "&E"(2) "=-infix" "raa-cor:3")
qed

AOT_theorem "sit-identity2:2": ‹s = s' ≡ ∀s'' (s'' ⊴ s ≡ s'' ⊴ s')›
proof(safe intro!: "≡I" "→I" Situation.GEN "sit-identity"[THEN "≡E"(2)]
GEN[where 'a=𝗈])
AOT_show ‹s'' ⊴ s'› if ‹s'' ⊴ s› and ‹s = s'› for s''
using "rule=E" that by blast
next
AOT_show ‹s'' ⊴ s› if ‹s'' ⊴ s'› and ‹s = s'› for s''
using "rule=E" id_sym that by blast
next
AOT_show ‹s' ⊨ p› if ‹s ⊨ p› and ‹∀s'' (s'' ⊴ s ≡ s'' ⊴ s')› for p
using "sit-part-whole"[THEN "≡⇩d⇩fE", THEN "&E"(2),
OF that(2)[THEN "Situation.∀E", THEN "≡E"(1), OF "part:1"],
THEN "∀E"(2), THEN "→E", OF that(1)].
next
AOT_show ‹s ⊨ p› if ‹s' ⊨ p› and ‹∀s'' (s'' ⊴ s ≡ s'' ⊴ s')› for p
using "sit-part-whole"[THEN "≡⇩d⇩fE", THEN "&E"(2),
OF that(2)[THEN "Situation.∀E", THEN "≡E"(2), OF "part:1"],
THEN "∀E"(2), THEN "→E", OF that(1)].
qed

AOT_define Persistent :: ‹φ ⇒ φ› (‹Persistent'(_')›)
persistent: ‹Persistent(p) ≡⇩d⇩f ∀s (s ⊨ p → ∀s' (s ⊴ s' → s' ⊨ p))›

AOT_theorem "pers-prop": ‹∀p Persistent(p)›
by (safe intro!: GEN[where 'a=𝗈] Situation.GEN persistent[THEN "≡⇩d⇩fI"] "→I")
(simp add: "sit-part-whole"[THEN "≡⇩d⇩fE", THEN "&E"(2), THEN "∀E"(2), THEN "→E"])

AOT_define NullSituation :: ‹τ ⇒ φ› (‹NullSituation'(_')›)
"df-null-trivial:1": ‹NullSituation(s) ≡⇩d⇩f ¬∃p s ⊨ p›

AOT_define TrivialSituation :: ‹τ ⇒ φ› (‹TrivialSituation'(_')›)
"df-null-trivial:2": ‹TrivialSituation(s) ≡⇩d⇩f ∀p s ⊨ p›

AOT_theorem "thm-null-trivial:1": ‹∃!x NullSituation(x)›
proof (AOT_subst ‹NullSituation(x)› ‹A!x & ∀F (x[F] ≡ F ≠ F)› for: x)
AOT_modally_strict {
AOT_show ‹NullSituation(x) ≡ A!x & ∀F (x[F] ≡ F ≠ F)› for x
proof (safe intro!: "≡I" "→I" "df-null-trivial:1"[THEN "≡⇩d⇩fI"]
dest!: "df-null-trivial:1"[THEN "≡⇩d⇩fE"])
AOT_assume 0: ‹Situation(x) & ¬∃p x ⊨ p›
AOT_have 1: ‹A!x›
using 0[THEN "&E"(1), THEN situations[THEN "≡⇩d⇩fE"], THEN "&E"(1)].
AOT_have 2: ‹x[F] → ∃p F = [λy p]› for F
using 0[THEN "&E"(1), THEN situations[THEN "≡⇩d⇩fE"],
THEN "&E"(2), THEN "∀E"(2)]
by (metis "≡⇩d⇩fE" "→I" "prop-prop1" "→E")
AOT_show ‹A!x & ∀F (x[F] ≡ F ≠ F)›
proof (safe intro!: "&I" 1 GEN "≡I" "→I")
fix F
AOT_assume ‹x[F]›
moreover AOT_obtain p where ‹F = [λy p]›
using calculation 2[THEN "→E"] "∃E"[rotated] by blast
ultimately AOT_have ‹x[λy p]›
by (metis "rule=E")
AOT_hence ‹x ⊨ p›
using lem1[THEN "→E", OF 0[THEN "&E"(1)], THEN "≡E"(2)] by blast
AOT_hence ‹∃p (x ⊨ p)›
by (rule "∃I")
AOT_thus ‹F ≠ F›
using 0[THEN "&E"(2)] "raa-cor:1" "&I" by blast
next
fix F :: ‹<κ> AOT_var›
AOT_assume ‹F ≠ F›
AOT_hence ‹¬(F = F)› by (metis "≡⇩d⇩fE" "=-infix")
moreover AOT_have ‹F = F›
ultimately AOT_show ‹x[F]› using "&I" "raa-cor:1" by blast
qed
next
AOT_assume 0: ‹A!x & ∀F (x[F] ≡ F ≠ F)›
AOT_hence ‹x[F] ≡ F ≠ F› for F
using "∀E" "&E" by blast
AOT_hence 1: ‹¬x[F]› for F
using "≡⇩d⇩fE" "id-eq:1" "=-infix" "reductio-aa:1" "≡E"(1) by blast
AOT_show ‹Situation(x) & ¬∃p x ⊨ p›
proof (safe intro!: "&I" situations[THEN "≡⇩d⇩fI"] 0[THEN "&E"(1)] GEN "→I")
AOT_show ‹Propositional([F])› if ‹x[F]› for F
using that 1 "&I" "raa-cor:1" by fast
next
AOT_show ‹¬∃p x ⊨ p›
proof(rule "raa-cor:2")
AOT_assume ‹∃p x ⊨ p›
then AOT_obtain p where ‹x ⊨ p› using "∃E"[rotated] by blast
AOT_hence ‹x[λy p]›
using "≡⇩d⇩fE" "&E"(1) "≡E"(1) lem1 "modus-tollens:1"
"raa-cor:3" "true-in-s" by fast
moreover AOT_have ‹¬x[λy p]›
by (rule 1[unvarify F]) "cqt:2[lambda]"
ultimately AOT_show ‹p & ¬p› for p using "&I" "raa-cor:1" by blast
qed
qed
qed
}
next
AOT_show ‹∃!x ([A!]x & ∀F (x[F] ≡ F ≠ F))›
qed

AOT_theorem "thm-null-trivial:2": ‹∃!x TrivialSituation(x)›
proof (AOT_subst ‹TrivialSituation(x)› ‹A!x & ∀F (x[F] ≡ ∃p F = [λy p])› for: x)
AOT_modally_strict {
AOT_show ‹TrivialSituation(x) ≡ A!x & ∀F (x[F] ≡ ∃p F = [λy p])› for x
proof (safe intro!: "≡I" "→I" "df-null-trivial:2"[THEN "≡⇩d⇩fI"]
dest!: "df-null-trivial:2"[THEN "≡⇩d⇩fE"])
AOT_assume 0: ‹Situation(x) & ∀p x ⊨ p›
AOT_have 1: ‹A!x›
using 0[THEN "&E"(1), THEN situations[THEN "≡⇩d⇩fE"], THEN "&E"(1)].
AOT_have 2: ‹x[F] → ∃p F = [λy p]› for F
using 0[THEN "&E"(1), THEN situations[THEN "≡⇩d⇩fE"],
THEN "&E"(2), THEN "∀E"(2)]
by (metis "≡⇩d⇩fE" "deduction-theorem" "prop-prop1" "→E")
AOT_show ‹A!x & ∀F (x[F] ≡ ∃p F = [λy p])›
proof (safe intro!: "&I" 1 GEN "≡I" "→I" 2)
fix F
AOT_assume ‹∃p F = [λy p]›
then AOT_obtain p where ‹F = [λy p]›
using "∃E"[rotated] by blast
moreover AOT_have ‹x ⊨ p›
using 0[THEN "&E"(2)] "∀E" by blast
ultimately AOT_show ‹x[F]›
by (metis 0 "rule=E" "&E"(1) id_sym "≡E"(2) lem1
"Commutativity of ≡" "→E")
qed
next
AOT_assume 0: ‹A!x & ∀F (x[F] ≡ ∃p F = [λy p])›
AOT_hence 1: ‹x[F] ≡ ∃p F = [λy p]› for F
using "∀E" "&E" by blast
AOT_have 2: ‹Situation(x)›
proof (safe intro!: "&I" situations[THEN "≡⇩d⇩fI"] 0[THEN "&E"(1)] GEN "→I")
AOT_show ‹Propositional([F])› if ‹x[F]› for F
using 1[THEN "≡E"(1), OF that]
by (metis "≡⇩d⇩fI" "prop-prop1")
qed
AOT_show ‹Situation(x) & ∀p (x ⊨ p)›
proof (safe intro!: "&I" 2 0[THEN "&E"(1)] GEN "→I")
AOT_have ‹x[λy p] ≡ ∃q [λy p] = [λy q]› for p
by (rule 1[unvarify F, where τ="«[λy p]»"]) "cqt:2[lambda]"
moreover AOT_have ‹∃q [λy p] = [λy q]› for p
by (rule "∃I"(2)[where β=p])
ultimately AOT_have ‹x[λy p]› for p by (metis "≡E"(2))
AOT_thus ‹x ⊨ p› for p
by (metis "2" "≡E"(2) lem1 "→E")
qed
qed
}
next
AOT_show ‹∃!x ([A!]x & ∀F (x[F] ≡ ∃p F = [λy p]))›
qed

AOT_theorem "thm-null-trivial:3": ‹❙ιx NullSituation(x)↓›
by (meson "A-Exists:2" "RA" "≡E"(2) "thm-null-trivial:1")

AOT_theorem "thm-null-trivial:4": ‹❙ιx TrivialSituation(x)↓›
using "A-Exists:2" "RA" "≡E"(2) "thm-null-trivial:2" by blast

AOT_define TheNullSituation :: ‹κ⇩s› (‹❙s⇩∅›)
"df-the-null-sit:1": ‹❙s⇩∅ =⇩d⇩f ❙ιx NullSituation(x)›

AOT_define TheTrivialSituation :: ‹κ⇩s› (‹❙s⇩V›)
"df-the-null-sit:2": ‹❙s⇩V =⇩d⇩f ❙ιx TrivialSituation(x)›

AOT_theorem "null-triv-sc:1": ‹NullSituation(x) → □NullSituation(x)›
proof(safe intro!: "→I" dest!: "df-null-trivial:1"[THEN "≡⇩d⇩fE"];
frule "&E"(1); drule "&E"(2))
AOT_assume 1: ‹¬∃p (x ⊨ p)›
AOT_assume 0: ‹Situation(x)›
AOT_hence ‹□Situation(x)› by (metis "≡E"(1) "possit-sit:1")
moreover AOT_have ‹□¬∃p (x ⊨ p)›
proof(rule "raa-cor:1")
AOT_assume ‹¬□¬∃p (x ⊨ p)›
AOT_hence ‹◇∃p (x ⊨ p)›
by (metis "≡⇩d⇩fI" "conventions:5")
AOT_hence ‹∃p ◇(x ⊨ p)› by (metis "BF◇" "→E")
then AOT_obtain p where ‹◇(x ⊨ p)› using "∃E"[rotated] by blast
AOT_hence ‹x ⊨ p›
by (metis "≡E"(1) "lem2:2"[unconstrain s, THEN "→E", OF 0])
AOT_hence ‹∃p x ⊨ p› using "∃I" by fast
AOT_thus ‹∃p x ⊨ p & ¬∃p x ⊨ p› using 1 "&I" by blast
qed
ultimately AOT_have 2: ‹□(Situation(x) & ¬∃p x ⊨ p)›
by (metis "KBasic:3" "&I" "≡E"(2))
AOT_show ‹□NullSituation(x)›
by (AOT_subst ‹NullSituation(x)› ‹Situation(x) & ¬∃p x ⊨ p›)
(auto simp: "df-null-trivial:1" "≡Df" 2)
qed

AOT_theorem "null-triv-sc:2": ‹TrivialSituation(x) → □TrivialSituation(x)›
proof(safe intro!: "→I" dest!: "df-null-trivial:2"[THEN "≡⇩d⇩fE"];
frule "&E"(1); drule "&E"(2))
AOT_assume 0: ‹Situation(x)›
AOT_hence 1: ‹□Situation(x)› by (metis "≡E"(1) "possit-sit:1")
AOT_assume ‹∀p x ⊨ p›
AOT_hence ‹x ⊨ p› for p
using "∀E" by blast
AOT_hence ‹□x ⊨ p› for p
using  0 "≡E"(1) "lem2:1"[unconstrain s, THEN "→E"] by blast
AOT_hence ‹∀p □x ⊨ p›
by (rule GEN)
AOT_hence ‹□∀p x ⊨ p›
by (rule BF[THEN "→E"])
AOT_hence 2: ‹□(Situation(x) & ∀p x ⊨ p)›
using 1 by (metis "KBasic:3" "&I" "≡E"(2))
AOT_show ‹□TrivialSituation(x)›
by (AOT_subst ‹TrivialSituation(x)› ‹Situation(x) & ∀p x ⊨ p›)
(auto simp: "df-null-trivial:2" "≡Df" 2)
qed

AOT_theorem "null-triv-sc:3": ‹NullSituation(❙s⇩∅)›
by (safe intro!: "df-the-null-sit:1"[THEN "=⇩d⇩fI"(2)] "thm-null-trivial:3"
"rule=I:1"[OF "thm-null-trivial:3"]
"!box-desc:2"[THEN "→E", THEN "→E", rotated, OF "thm-null-trivial:1",
OF "∀I", OF "null-triv-sc:1", THEN "∀E"(1), THEN "→E"])

AOT_theorem "null-triv-sc:4": ‹TrivialSituation(❙s⇩V)›
by (safe intro!: "df-the-null-sit:2"[THEN "=⇩d⇩fI"(2)] "thm-null-trivial:4"
"rule=I:1"[OF "thm-null-trivial:4"]
"!box-desc:2"[THEN "→E", THEN "→E", rotated, OF "thm-null-trivial:2",
OF "∀I", OF "null-triv-sc:2", THEN "∀E"(1), THEN "→E"])

AOT_theorem "null-triv-facts:1": ‹NullSituation(x) ≡ Null(x)›
proof (safe intro!: "≡I" "→I" "df-null-uni:1"[THEN "≡⇩d⇩fI"]
"df-null-trivial:1"[THEN "≡⇩d⇩fI"]
dest!: "df-null-uni:1"[THEN "≡⇩d⇩fE"] "df-null-trivial:1"[THEN "≡⇩d⇩fE"])
AOT_assume 0: ‹Situation(x) & ¬∃p x ⊨ p›
AOT_have 1: ‹x[F] → ∃p F = [λy p]› for F
using 0[THEN "&E"(1), THEN situations[THEN "≡⇩d⇩fE"], THEN "&E"(2), THEN "∀E"(2)]
by (metis "≡⇩d⇩fE" "deduction-theorem" "prop-prop1" "→E")
AOT_show ‹A!x & ¬∃F x[F]›
proof (safe intro!: "&I" 0[THEN "&E"(1), THEN situations[THEN "≡⇩d⇩fE"],
THEN "&E"(1)];
rule "raa-cor:2")
AOT_assume ‹∃F x[F]›
then AOT_obtain F where F_prop: ‹x[F]›
using "∃E"[rotated] by blast
AOT_hence ‹∃p F = [λy p]›
using 1[THEN "→E"] by blast
then AOT_obtain p where ‹F = [λy p]›
using "∃E"[rotated] by blast
AOT_hence ‹x[λy p]›
by (metis "rule=E" F_prop)
AOT_hence ‹x ⊨ p›
using lem1[THEN "→E", OF 0[THEN "&E"(1)], THEN "≡E"(2)] by blast
AOT_hence ‹∃p x ⊨ p›
by (rule "∃I")
AOT_thus ‹∃p x ⊨ p & ¬∃p x ⊨ p›
using 0[THEN "&E"(2)] "&I" by blast
qed
next
AOT_assume 0: ‹A!x & ¬∃F x[F]›
AOT_have ‹Situation(x)›
apply (rule situations[THEN "≡⇩d⇩fI", OF "&I", OF 0[THEN "&E"(1)]]; rule GEN)
using 0[THEN "&E"(2)] by (metis "→I" "existential:2[const_var]" "raa-cor:3")
moreover AOT_have ‹¬∃p x ⊨ p›
proof (rule "raa-cor:2")
AOT_assume ‹∃p x ⊨ p›
then AOT_obtain p where ‹x ⊨ p› by (metis "instantiation")
AOT_hence ‹x[λy p]› by (metis "≡⇩d⇩fE" "&E"(2) "prop-enc" "true-in-s")
AOT_hence ‹∃F x[F]› by (rule "∃I") "cqt:2[lambda]"
AOT_thus ‹∃F x[F] & ¬∃F x[F]› using 0[THEN "&E"(2)] "&I" by blast
qed
ultimately AOT_show ‹Situation(x) & ¬∃p x ⊨ p› using "&I" by blast
qed

AOT_theorem "null-triv-facts:2": ‹❙s⇩∅ = a⇩∅›
apply (rule "=⇩d⇩fI"(2)[OF "df-the-null-sit:1"])
apply (fact "thm-null-trivial:3")
apply (rule "=⇩d⇩fI"(2)[OF "df-null-uni-terms:1"])
apply (fact "null-uni-uniq:3")
apply (rule "equiv-desc-eq:3"[THEN "→E"])
apply (rule "&I")
apply (fact "thm-null-trivial:3")
by (rule RN; rule GEN; rule "null-triv-facts:1")

AOT_theorem "null-triv-facts:3": ‹❙s⇩V ≠ a⇩V›
proof(rule "=-infix"[THEN "≡⇩d⇩fI"])
AOT_have ‹Universal(a⇩V)›
AOT_hence 0: ‹a⇩V[A!]›
using "df-null-uni:2"[THEN "≡⇩d⇩fE"] "&E" "∀E"(1)
by (metis "cqt:5:a" "vdash-properties:10" "vdash-properties:1")
moreover AOT_have 1: ‹¬❙s⇩V[A!]›
proof(rule "raa-cor:2")
AOT_have ‹Situation(❙s⇩V)›
using "≡⇩d⇩fE" "&E"(1) "df-null-trivial:2" "null-triv-sc:4" by blast
AOT_hence ‹∀F (❙s⇩V[F] → Propositional([F]))›
by (metis "≡⇩d⇩fE" "&E"(2) situations)
moreover AOT_assume ‹❙s⇩V[A!]›
ultimately AOT_have ‹Propositional(A!)›
using "∀E"(1)[rotated, OF "oa-exist:2"] "→E" by blast
AOT_thus ‹Propositional(A!) & ¬Propositional(A!)›
using "prop-in-f:4:d" "&I" by blast
qed
AOT_show ‹¬(❙s⇩V = a⇩V)›
proof (rule "raa-cor:2")
AOT_assume ‹❙s⇩V = a⇩V›
AOT_hence ‹❙s⇩V[A!]› using 0 "rule=E" id_sym by fast
AOT_thus ‹❙s⇩V[A!] & ¬❙s⇩V[A!]› using 1 "&I" by blast
qed
qed

definition ConditionOnPropositionalProperties :: ‹(<κ> ⇒ 𝗈) ⇒ bool› where
"cond-prop": ‹ConditionOnPropositionalProperties ≡ λ φ . ∀ v .
[v ⊨ ∀F (φ{F} → Propositional([F]))]›

syntax ConditionOnPropositionalProperties :: ‹id_position ⇒ AOT_prop›
("CONDITION'_ON'_PROPOSITIONAL'_PROPERTIES'(_')")

AOT_theorem "cond-prop[E]":
assumes ‹CONDITION_ON_PROPOSITIONAL_PROPERTIES(φ)›
shows ‹∀F (φ{F} → Propositional([F]))›
using assms[unfolded "cond-prop"] by auto

AOT_theorem "cond-prop[I]":
assumes ‹❙⊢⇩□ ∀F (φ{F} → Propositional([F]))›
shows ‹CONDITION_ON_PROPOSITIONAL_PROPERTIES(φ)›
using assms "cond-prop" by metis

AOT_theorem "pre-comp-sit":
assumes ‹CONDITION_ON_PROPOSITIONAL_PROPERTIES(φ)›
shows ‹(Situation(x) & ∀F (x[F] ≡ φ{F})) ≡ (A!x & ∀F (x[F] ≡ φ{F}))›
proof(rule "≡I"; rule "→I")
AOT_assume ‹Situation(x) & ∀F (x[F] ≡ φ{F})›
AOT_thus ‹A!x & ∀F (x[F] ≡ φ{F})›
using "&E" situations[THEN "≡⇩d⇩fE"] "&I" by blast
next
AOT_assume 0: ‹A!x & ∀F (x[F] ≡ φ{F})›
AOT_show ‹Situation(x) & ∀F (x[F] ≡ φ{F})›
proof (safe intro!: situations[THEN "≡⇩d⇩fI"] "&I")
AOT_show ‹A!x› using 0[THEN "&E"(1)].
next
AOT_show ‹∀F (x[F] → Propositional([F]))›
proof(rule GEN; rule "→I")
fix F
AOT_assume ‹x[F]›
AOT_hence ‹φ{F}›
using 0[THEN "&E"(2)] "∀E" "≡E" by blast
AOT_thus ‹Propositional([F])›
using "cond-prop[E]"[OF assms] "∀E" "→E" by blast
qed
next
AOT_show ‹∀F (x[F] ≡ φ{F})› using 0 "&E" by blast
qed
qed

AOT_theorem "comp-sit:1":
assumes ‹CONDITION_ON_PROPOSITIONAL_PROPERTIES(φ)›
shows ‹∃s ∀F(s[F] ≡ φ{F})›
by (AOT_subst ‹Situation(x) & ∀F(x[F] ≡ φ{F})› ‹A!x & ∀F (x[F] ≡ φ{F})› for: x)
(auto simp: "pre-comp-sit"[OF assms] "A-objects"[where φ=φ, axiom_inst])

AOT_theorem "comp-sit:2":
assumes ‹CONDITION_ON_PROPOSITIONAL_PROPERTIES(φ)›
shows ‹∃!s ∀F(s[F] ≡ φ{F})›
by (AOT_subst ‹Situation(x) & ∀F(x[F] ≡ φ{F})› ‹A!x & ∀F (x[F] ≡ φ{F})› for: x)
(auto simp: assms "pre-comp-sit"  "pre-comp-sit"[OF assms] "A-objects!")

AOT_theorem "can-sit-desc:1":
assumes ‹CONDITION_ON_PROPOSITIONAL_PROPERTIES(φ)›
shows ‹❙ιs(∀F (s[F] ≡ φ{F}))↓›
using "comp-sit:2"[OF assms] "A-Exists:2" "RA" "≡E"(2) by blast

AOT_theorem "can-sit-desc:2":
assumes ‹CONDITION_ON_PROPOSITIONAL_PROPERTIES(φ)›
shows ‹❙ιs(∀F (s[F] ≡ φ{F})) = ❙ιx(A!x & ∀F (x[F] ≡ φ{F}))›
by (auto intro!: "equiv-desc-eq:2"[THEN "→E", OF "&I",
OF "can-sit-desc:1"[OF assms]]
"RA" GEN "pre-comp-sit"[OF assms])

AOT_theorem "strict-sit":
assumes ‹RIGID_CONDITION(φ)›
and ‹CONDITION_ON_PROPOSITIONAL_PROPERTIES(φ)›
shows ‹y = ❙ιs(∀F (s[F] ≡ φ{F})) → ∀F (y[F] ≡ φ{F})›
using "rule=E"[rotated, OF "can-sit-desc:2"[OF assms(2), symmetric]]
"box-phi-a:2"[OF assms(1)] "→E" "→I" "&E" by fast

(* TODO: exercise (479) sit-lit *)

AOT_define actual :: ‹τ ⇒ φ› (‹Actual'(_')›)
‹Actual(s) ≡⇩d⇩f ∀p (s ⊨ p → p)›

AOT_theorem "act-and-not-pos": ‹∃s (Actual(s) & ◇¬Actual(s))›
proof -
AOT_obtain q⇩1 where q⇩1_prop: ‹q⇩1 & ◇¬q⇩1›
by (metis "≡⇩d⇩fE" "instantiation" "cont-tf:1" "cont-tf-thm:1")
AOT_have ‹∃s (∀F (s[F] ≡ F = [λy q⇩1]))›
proof (safe intro!: "comp-sit:1" "cond-prop[I]" GEN "→I")
AOT_modally_strict {
AOT_show ‹Propositional([F])› if ‹F = [λy q⇩1]› for F
using "≡⇩d⇩fI" "existential:2[const_var]" "prop-prop1" that by fastforce
}
qed
then AOT_obtain s⇩1 where s_prop: ‹∀F (s⇩1[F] ≡ F = [λy q⇩1])›
using "Situation.∃E"[rotated] by meson
AOT_have ‹Actual(s⇩1)›
proof(safe intro!: actual[THEN "≡⇩d⇩fI"] "&I" GEN "→I" s_prop Situation.ψ)
fix p
AOT_assume ‹s⇩1 ⊨ p›
AOT_hence ‹s⇩1[λy p]›
by (metis "≡⇩d⇩fE" "&E"(2) "prop-enc" "true-in-s")
AOT_hence ‹[λy p] = [λy q⇩1]›
by (rule s_prop[THEN "∀E"(1), THEN "≡E"(1), rotated]) "cqt:2[lambda]"
AOT_hence ‹p = q⇩1› by (metis "≡E"(2) "p-identity-thm2:3")
AOT_thus ‹p› using q⇩1_prop[THEN "&E"(1)] "rule=E" id_sym by fast
qed
moreover AOT_have ‹◇¬Actual(s⇩1)›
proof(rule "raa-cor:1"; drule "KBasic:12"[THEN "≡E"(2)])
AOT_assume ‹□Actual(s⇩1)›
AOT_hence ‹□(Situation(s⇩1) & ∀p (s⇩1 ⊨ p → p))›
using actual[THEN "≡Df", THEN "conventions:3"[THEN "≡⇩d⇩fE"],
THEN "&E"(1), THEN RM, THEN "→E"] by blast
AOT_hence ‹□∀p (s⇩1 ⊨ p → p)›
by (metis "RM:1" "Conjunction Simplification"(2) "→E")
AOT_hence ‹∀p □(s⇩1 ⊨ p → p)›
by (metis "CBF" "vdash-properties:10")
AOT_hence ‹□(s⇩1 ⊨ q⇩1 → q⇩1)›
using "∀E" by blast
AOT_hence ‹□s⇩1 ⊨ q⇩1 → □q⇩1›
by (metis "→E" "qml:1" "vdash-properties:1")
moreover AOT_have ‹s⇩1 ⊨ q⇩1›
using s_prop[THEN "∀E"(1), THEN "≡E"(2),
THEN lem1[THEN "→E", OF Situation.ψ, THEN "≡E"(2)]]
"rule=I:1" "prop-prop2:2" by blast
ultimately AOT_have ‹□q⇩1›
using "≡⇩d⇩fE" "&E"(1) "≡E"(1) "lem2:1" "true-in-s" "→E" by fast
AOT_thus ‹◇¬q⇩1 & ¬◇¬q⇩1›
using "KBasic:12"[THEN "≡E"(1)] q⇩1_prop[THEN "&E"(2)] "&I" by blast
qed
ultimately AOT_have ‹(Actual(s⇩1) & ◇¬Actual(s⇩1))›
using s_prop "&I" by blast
thus ?thesis
by (rule "Situation.∃I")
qed

AOT_theorem "actual-s:1": ‹∃s Actual(s)›
proof -
AOT_obtain s where ‹(Actual(s) & ◇¬Actual(s))›
using "act-and-not-pos" "Situation.∃E"[rotated] by meson
AOT_hence ‹Actual(s)› using "&E" "&I" by metis
thus ?thesis by (rule "Situation.∃I")
qed

AOT_theorem "actual-s:2": ‹∃s ¬Actual(s)›
proof(rule "∃I"(1)[where τ=‹«❙s⇩V»›]; (rule "&I")?)
AOT_show ‹Situation(❙s⇩V)›
using "≡⇩d⇩fE" "&E"(1) "df-null-trivial:2" "null-triv-sc:4" by blast
next
AOT_show ‹¬Actual(❙s⇩V)›
proof(rule "raa-cor:2")
AOT_assume 0: ‹Actual(❙s⇩V)›
AOT_obtain p⇩1 where notp⇩1: ‹¬p⇩1›
by (metis "∃E" "∃I"(1) "log-prop-prop:2" "non-contradiction")
AOT_have ‹❙s⇩V ⊨ p⇩1›
using "null-triv-sc:4"[THEN "≡⇩d⇩fE"[OF "df-null-trivial:2"], THEN "&E"(2)]
"∀E" by blast
AOT_hence ‹p⇩1›
using 0[THEN actual[THEN "≡⇩d⇩fE"], THEN "&E"(2), THEN "∀E"(2), THEN "→E"]
by blast
AOT_thus ‹p & ¬p› for p using notp⇩1 by (metis "raa-cor:3")
qed
next
AOT_show ‹❙s⇩V↓›
using "df-the-null-sit:2" "rule-id-df:2:b[zero]" "thm-null-trivial:4" by blast
qed

AOT_theorem "actual-s:3": ‹∃p∀s(Actual(s) → ¬s ⊨ p)›
proof -
AOT_obtain p⇩1 where notp⇩1: ‹¬p⇩1›
by (metis "∃E" "∃I"(1) "log-prop-prop:2" "non-contradiction")
AOT_have ‹∀s (Actual(s) → ¬(s ⊨ p⇩1))›
proof (rule Situation.GEN; rule "→I"; rule "raa-cor:2")
fix s
AOT_assume ‹Actual(s)›
moreover AOT_assume ‹s ⊨ p⇩1›
ultimately AOT_have ‹p⇩1›
using actual[THEN "≡⇩d⇩fE", THEN "&E"(2), THEN "∀E"(2), THEN "→E"] by blast
AOT_thus ‹p⇩1 & ¬p⇩1›
using notp⇩1 "&I" by simp
qed
thus ?thesis by (rule "∃I")
qed

AOT_theorem comp:
‹∃s (s' ⊴ s & s'' ⊴ s & ∀s''' (s' ⊴ s''' & s'' ⊴ s''' → s ⊴ s'''))›
proof -
have cond_prop: ‹ConditionOnPropositionalProperties (λ Π . «s'[Π] ∨ s''[Π]»)›
proof(safe intro!: "cond-prop[I]" GEN "oth-class-taut:8:c"[THEN "→E", THEN "→E"];
rule "→I")
AOT_modally_strict {
fix F
AOT_have ‹Situation(s')›
AOT_hence ‹s'[F] → Propositional([F])›
using "situations"[THEN "≡⇩d⇩fE", THEN "&E"(2), THEN "∀E"(2)] by blast
moreover AOT_assume ‹s'[F]›
ultimately AOT_show ‹Propositional([F])›
using "→E" by blast
}
next
AOT_modally_strict {
fix F
AOT_have ‹Situation(s'')›
AOT_hence ‹s''[F] → Propositional([F])›
using "situations"[THEN "≡⇩d⇩fE", THEN "&E"(2), THEN "∀E"(2)] by blast
moreover AOT_assume ‹s''[F]›
ultimately AOT_show ‹Propositional([F])›
using "→E" by blast
}
qed
AOT_obtain s⇩3 where θ: ‹∀F (s⇩3[F] ≡ s'[F] ∨ s''[F])›
using "comp-sit:1"[OF cond_prop] "Situation.∃E"[rotated] by meson
AOT_have ‹s' ⊴ s⇩3 & s'' ⊴ s⇩3 & ∀s''' (s' ⊴ s''' & s'' ⊴ s''' → s⇩3 ⊴ s''')›
proof(safe intro!: "&I" "≡⇩d⇩fI"[OF "true-in-s"] "≡⇩d⇩fI"[OF "prop-enc"]
"Situation.GEN" "GEN"[where 'a=𝗈] "→I"
"sit-part-whole"[THEN "≡⇩d⇩fI"]
Situation.ψ "cqt:2[const_var]"[axiom_inst])
fix p
AOT_assume ‹s' ⊨ p›
AOT_hence ‹s'[λx p]›
by (metis "&E"(2) "prop-enc" "≡⇩d⇩fE" "true-in-s")
AOT_thus ‹s⇩3[λx p]›
using θ[THEN "∀E"(1),OF "prop-prop2:2", THEN "≡E"(2), OF "∨I"(1)] by blast
next
fix p
AOT_assume ‹s'' ⊨ p›
AOT_hence ‹s''[λx p]›
by (metis "&E"(2) "prop-enc" "≡⇩d⇩fE" "true-in-s")
AOT_thus ‹s⇩3[λx p]›
using θ[THEN "∀E"(1),OF "prop-prop2:2", THEN "≡E"(2), OF "∨I"(2)] by blast
next
fix s p
AOT_assume 0: ‹s' ⊴ s & s'' ⊴ s›
AOT_assume ‹s⇩3 ⊨ p›
AOT_hence ‹s⇩3[λx p]›
by (metis "&E"(2) "prop-enc" "≡⇩d⇩fE" "true-in-s")
AOT_hence ‹s'[λx p] ∨ s''[λx p]›
using θ[THEN "∀E"(1),OF "prop-prop2:2", THEN "≡E"(1)] by blast
moreover {
AOT_assume ‹s'[λx p]›
AOT_hence ‹s' ⊨ p›
by (safe intro!: "prop-enc"[THEN "≡⇩d⇩fI"] "true-in-s"[THEN "≡⇩d⇩fI"] "&I"
Situation.ψ "cqt:2[const_var]"[axiom_inst])
moreover AOT_have ‹s' ⊨ p → s ⊨ p›
using "sit-part-whole"[THEN "≡⇩d⇩fE", THEN "&E"(2)] 0[THEN "&E"(1)]
"∀E"(2) by blast
ultimately AOT_have ‹s ⊨ p›
using "→E" by blast
AOT_hence ‹s[λx p]›
using "true-in-s"[THEN "≡⇩d⇩fE"] "prop-enc"[THEN "≡⇩d⇩fE"] "&E" by blast
}
moreover {
AOT_assume ‹s''[λx p]›
AOT_hence ‹s'' ⊨ p›
by (safe intro!: "prop-enc"[THEN "≡⇩d⇩fI"] "true-in-s"[THEN "≡⇩d⇩fI"] "&I"
Situation.ψ "cqt:2[const_var]"[axiom_inst])
moreover AOT_have ‹s'' ⊨ p → s ⊨ p›
using "sit-part-whole"[THEN "≡⇩d⇩fE", THEN "&E"(2)] 0[THEN "&E"(2)]
"∀E"(2) by blast
ultimately AOT_have ‹s ⊨ p›
using "→E" by blast
AOT_hence ‹s[λx p]›
using "true-in-s"[THEN "≡⇩d⇩fE"] "prop-enc"[THEN "≡⇩d⇩fE"] "&E" by blast
}
ultimately AOT_show ‹s[λx p]›
by (metis "∨E"(1) "→I")
qed
thus ?thesis
using "Situation.∃I" by fast
qed

AOT_theorem "act-sit:1": ‹Actual(s) → (s ⊨ p → [λy p]s)›
proof (safe intro!: "→I")
AOT_assume ‹Actual(s)›
AOT_hence p if ‹s ⊨ p›
using actual[THEN "≡⇩d⇩fE", THEN "&E"(2), THEN "∀E"(2), THEN "→E"] that by blast
moreover AOT_assume ‹s ⊨ p›
ultimately AOT_have p by blast
AOT_thus ‹[λy p]s›
by (safe intro!: "β←C"(1) "cqt:2")
qed

AOT_theorem "act-sit:2":
‹(Actual(s') & Actual(s'')) → ∃x (Actual(x) & s' ⊴ x & s'' ⊴ x)›
proof(rule "→I"; frule "&E"(1); drule "&E"(2))
AOT_assume act_s': ‹Actual(s')›
AOT_assume act_s'': ‹Actual(s'')›
have "cond-prop": ‹ConditionOnPropositionalProperties
(λ Π . «∃p (Π = [λy p] & (s' ⊨ p ∨ s'' ⊨ p))»)›
proof (safe intro!: "cond-prop[I]"  "∀I" "→I" "prop-prop1"[THEN "≡⇩d⇩fI"])
AOT_modally_strict {
fix β
AOT_assume ‹∃p (β = [λy p] & (s' ⊨ p ∨ s'' ⊨ p))›
then AOT_obtain p where ‹β = [λy p]› using "∃E"[rotated] "&E" by blast
AOT_thus ‹∃p β = [λy p]› by (rule "∃I")
}
qed
have rigid: ‹rigid_condition (λ Π . «∃p (Π = [λy p] & (s' ⊨ p ∨ s'' ⊨ p))»)›
proof(safe intro!: "strict-can:1[I]" "→I" GEN)
AOT_modally_strict {
fix F
AOT_assume ‹∃p (F = [λy p] & (s' ⊨ p ∨ s'' ⊨ p))›
then AOT_obtain p⇩1 where p⇩1_prop: ‹F = [λy p⇩1] & (s' ⊨ p⇩1 ∨ s'' ⊨ p⇩1)›
using "∃E"[rotated] by blast
AOT_hence ‹□(F = [λy p⇩1])›
using "&E"(1) "id-nec:2" "vdash-properties:10" by blast
moreover AOT_have ‹□(s' ⊨ p⇩1 ∨ s'' ⊨ p⇩1)›
proof(rule "∨E"; (rule "→I"; rule "KBasic:15"[THEN "→E"])?)
AOT_show ‹s' ⊨ p⇩1 ∨ s'' ⊨ p⇩1› using p⇩1_prop "&E" by blast
next
AOT_show ‹□s' ⊨ p⇩1 ∨ □s'' ⊨ p⇩1› if ‹s' ⊨ p⇩1›
apply (rule "∨I"(1))
using "≡⇩d⇩fE" "&E"(1) "≡E"(1) "lem2:1" that "true-in-s" by blast
next
AOT_show ‹□s' ⊨ p⇩1 ∨ □s'' ⊨ p⇩1› if ‹s'' ⊨ p⇩1›
apply (rule "∨I"(2))
using "≡⇩d⇩fE" "&E"(1) "≡E"(1) "lem2:1" that "true-in-s" by blast
qed
ultimately AOT_have ‹□(F = [λy p⇩1] & (s' ⊨ p⇩1 ∨ s'' ⊨ p⇩1))›
by (metis "KBasic:3" "&I" "≡E"(2))
AOT_hence ‹∃p □(F = [λy p] & (s' ⊨ p ∨ s'' ⊨ p))› by (rule "∃I")
AOT_thus ‹□∃p (F = [λy p] & (s' ⊨ p ∨ s'' ⊨ p))›
using Buridan[THEN "→E"] by fast
}
qed

AOT_have desc_den: ‹❙ιs(∀F (s[F] ≡ ∃p (F = [λy p] & (s' ⊨ p ∨ s'' ⊨ p))))↓›
by (rule "can-sit-desc:1"[OF "cond-prop"])
AOT_obtain x⇩0
where x⇩0_prop1: ‹x⇩0 = ❙ιs(∀F (s[F] ≡ ∃p (F = [λy p] & (s' ⊨ p ∨ s'' ⊨ p))))›
by (metis (no_types, lifting) "∃E" "rule=I:1" desc_den "∃I"(1) id_sym)
AOT_hence x⇩0_sit: ‹Situation(x⇩0)›
using "actual-desc:3"[THEN "→E"] "Act-Basic:2" "&E"(1) "≡E"(1)
"possit-sit:4" by blast

AOT_have 1: ‹∀F (x⇩0[F] ≡ ∃p (F = [λy p] & (s' ⊨ p ∨ s'' ⊨ p)))›
using "strict-sit"[OF rigid, OF "cond-prop", THEN "→E", OF x⇩0_prop1].
AOT_have 2: ‹(x⇩0 ⊨ p) ≡ (s' ⊨ p ∨ s'' ⊨ p)› for p
proof (rule "≡I"; rule "→I")
AOT_assume ‹x⇩0 ⊨ p›
AOT_hence ‹x⇩0[λy p]› using lem1[THEN "→E", OF x⇩0_sit, THEN "≡E"(1)] by blast
then AOT_obtain q where ‹[λy p] = [λy q] & (s' ⊨ q ∨ s'' ⊨ q)›
using 1[THEN "∀E"(1)[where τ="«[λy p]»"], OF "prop-prop2:2", THEN "≡E"(1)]
"∃E"[rotated] by blast
AOT_thus ‹s' ⊨ p ∨ s'' ⊨ p›
by (metis "rule=E" "&E"(1) "&E"(2) "∨I"(1) "∨I"(2)
"∨E"(1) "deduction-theorem" id_sym "≡E"(2) "p-identity-thm2:3")
next
AOT_assume ‹s' ⊨ p ∨ s'' ⊨ p›
AOT_hence ‹[λy p] = [λy p] & (s' ⊨ p ∨ s'' ⊨ p)›
by (metis "rule=I:1" "&I" "prop-prop2:2")
AOT_hence ‹∃q ([λy p] = [λy q] & (s' ⊨ q ∨ s'' ⊨ q))›
by (rule "∃I")
AOT_hence ‹x⇩0[λy p]›
using 1[THEN "∀E"(1), OF "prop-prop2:2", THEN "≡E"(2)] by blast
AOT_thus ‹x⇩0 ⊨ p›
by (metis "≡⇩d⇩fI" "&I" "ex:1:a" "prop-enc" "rule-ui:2[const_var]"
x⇩0_sit "true-in-s")
qed

AOT_have ‹Actual(x⇩0) & s' ⊴ x⇩0 & s'' ⊴ x⇩0›
proof(safe intro!: "→I" "&I" "∃I"(1) actual[THEN "≡⇩d⇩fI"] x⇩0_sit GEN
"sit-part-whole"[THEN "≡⇩d⇩fI"])
fix p
AOT_assume ‹x⇩0 ⊨ p›
AOT_hence ‹s' ⊨ p ∨ s'' ⊨ p›
using 2 "≡E"(1) by metis
AOT_thus ‹p›
using act_s' act_s''
actual[THEN "≡⇩d⇩fE", THEN "&E"(2), THEN "∀E"(2), THEN "→E"]
by (metis "∨E"(3) "reductio-aa:1")
next
AOT_show ‹x⇩0 ⊨ p› if ‹s' ⊨ p› for p
using 2[THEN "≡E"(2), OF "∨I"(1), OF that].
next
AOT_show ‹x⇩0 ⊨ p› if ‹s'' ⊨ p› for p
using 2[THEN "≡E"(2), OF "∨I"(2), OF that].
next
AOT_show ‹Situation(s')›
using act_s'[THEN actual[THEN "≡⇩d⇩fE"]] "&E" by blast
next
AOT_show ‹Situation(s'')›
using act_s''[THEN actual[THEN "≡⇩d⇩fE"]] "&E" by blast
qed
AOT_thus ‹∃x (Actual(x) & s' ⊴ x & s'' ⊴ x)›
by (rule "∃I")
qed

AOT_define Consistent :: ‹τ ⇒ φ› (‹Consistent'(_')›)
cons: ‹Consistent(s) ≡⇩d⇩f ¬∃p (s ⊨ p & s ⊨ ¬p)›

AOT_theorem "sit-cons": ‹Actual(s) → Consistent(s)›
proof(safe intro!: "→I" cons[THEN "≡⇩d⇩fI"] "&I" Situation.ψ
dest!: actual[THEN "≡⇩d⇩fE"]; frule "&E"(1); drule "&E"(2))
AOT_assume 0: ‹∀p (s ⊨ p → p)›
AOT_show ‹¬∃p (s ⊨ p & s ⊨ ¬p)›
proof (rule "raa-cor:2")
AOT_assume ‹∃p (s ⊨ p & s ⊨ ¬p)›
then AOT_obtain p where ‹s ⊨ p & s ⊨ ¬p›
using "∃E"[rotated] by blast
AOT_hence ‹p & ¬p›
using 0[THEN "∀E"(1)[where τ=‹«¬p»›, THEN "→E"], OF "log-prop-prop:2"]
0[THEN "∀E"(2)[where β=p], THEN "→E"] "&E" "&I" by blast
AOT_thus ‹p & ¬p› for p by (metis "raa-cor:1")
qed
qed

AOT_theorem "cons-rigid:1": ‹¬Consistent(s) ≡ □¬Consistent(s)›
proof (rule "≡I"; rule "→I")
AOT_assume ‹¬Consistent(s)›
AOT_hence ‹∃p (s ⊨ p & s ⊨ ¬p)›
using cons[THEN "≡⇩d⇩fI", OF "&I", OF Situation.ψ]
by (metis "raa-cor:3")
then AOT_obtain p where p_prop: ‹s ⊨ p & s ⊨ ¬p›
using "∃E"[rotated] by blast
AOT_hence ‹□s ⊨ p›
using "&E"(1) "≡E"(1) "lem2:1" by blast
moreover AOT_have ‹□s ⊨ ¬p›
using p_prop "T◇" "&E" "≡E"(1)
"modus-tollens:1" "raa-cor:3" "lem2:3"[unvarify p]
"log-prop-prop:2" by metis
ultimately AOT_have ‹□(s ⊨ p & s ⊨ ¬p)›
by (metis "KBasic:3" "&I" "≡E"(2))
AOT_hence ‹∃p □(s ⊨ p & s ⊨ ¬p)›
by (rule "∃I")
AOT_hence ‹□∃p(s ⊨ p & s ⊨ ¬p)›
by (metis Buridan "vdash-properties:10")
AOT_thus ‹□¬Consistent(s)›
apply (rule "qml:1"[axiom_inst, THEN "→E", THEN "→E", rotated])
apply (rule RN)
using "≡⇩d⇩fE" "&E"(2) cons "deduction-theorem" "raa-cor:3" by blast
next
AOT_assume ‹□¬Consistent(s)›
AOT_thus ‹¬Consistent(s)› using "qml:2"[axiom_inst, THEN "→E"] by auto
qed

AOT_theorem "cons-rigid:2": ‹◇Consistent(x) ≡ Consistent(x)›
proof(rule "≡I"; rule "→I")
AOT_assume 0: ‹◇Consistent(x)›
AOT_have ‹◇(Situation(x) & ¬∃p (x ⊨ p & x ⊨ ¬p))›
apply (AOT_subst ‹Situation(x) & ¬∃p (x ⊨ p & x ⊨ ¬p)› ‹Consistent(x)›)
using cons "≡E"(2) "Commutativity of ≡" "≡Df" apply blast
AOT_hence ‹◇Situation(x)› and 1: ‹◇¬∃p (x ⊨ p & x ⊨ ¬p)›
using "RM◇" "Conjunction Simplification"(1) "Conjunction Simplification"(2)
"modus-tollens:1" "raa-cor:3" by blast+
AOT_hence 2: ‹Situation(x)› by (metis "≡E"(1) "possit-sit:2")
AOT_have 3: ‹¬□∃p (x ⊨ p & x ⊨ ¬p)›
using 2 using 1 "KBasic:11" "≡E"(2) by blast
AOT_show ‹Consistent(x)›
proof (rule "raa-cor:1")
AOT_assume ‹¬Consistent(x)›
AOT_hence ‹∃p (x ⊨ p & x ⊨ ¬p)›
using 0 "≡⇩d⇩fE" "conventions:5" 2 "cons-rigid:1"[unconstrain s, THEN "→E"]
"modus-tollens:1" "raa-cor:3" "≡E"(4) by meson
then AOT_obtain p where ‹x ⊨ p› and 4: ‹x ⊨ ¬p›
using "∃E"[rotated] "&E" by blast
AOT_hence ‹□x ⊨ p›
by (metis "2" "≡E"(1) "lem2:1"[unconstrain s, THEN "→E"])
moreover AOT_have ‹□x ⊨ ¬p›
using 4 "lem2:1"[unconstrain s, unvarify p, THEN "→E"]
by (metis 2 "≡E"(1) "log-prop-prop:2")
ultimately AOT_have ‹□(x ⊨ p & x ⊨ ¬p)›
by (metis "KBasic:3" "&I" "≡E"(3) "raa-cor:3")
AOT_hence ‹∃p □(x ⊨ p & x ⊨ ¬p)›
by (metis "existential:1" "log-prop-prop:2")
AOT_hence ‹□∃p (x ⊨ p & x ⊨ ¬p)›
by (metis Buridan "vdash-properties:10")
AOT_thus ‹p & ¬p› for p
using 3 "&I"  by (metis "raa-cor:3")
qed
next
AOT_show ‹◇Consistent(x)› if ‹Consistent(x)›
using "T◇" that "vdash-properties:10" by blast
qed

AOT_define possible :: ‹τ ⇒ φ› (‹Possible'(_')›)
pos: ‹Possible(s) ≡⇩d⇩f ◇Actual(s)›

AOT_theorem "sit-pos:1": ‹Actual(s) → Possible(s)›
apply(rule "→I"; rule pos[THEN "≡⇩d⇩fI"]; rule "&I")
apply (meson "≡⇩d⇩fE" actual "&E"(1))
using "T◇" "vdash-properties:10" by blast

AOT_theorem "sit-pos:2": ‹∃p ((s ⊨ p) & ¬◇p) → ¬Possible(s)›
proof(rule "→I")
AOT_assume ‹∃p ((s ⊨ p) & ¬◇p)›
then AOT_obtain p where a: ‹(s ⊨ p) & ¬◇p›
using "∃E"[rotated] by blast
AOT_hence ‹□(s ⊨ p)›
using "&E" by (metis "T◇" "≡E"(1) "lem2:3" "vdash-properties:10")
moreover AOT_have ‹□¬p›
using a[THEN "&E"(2)] by (metis "KBasic2:1" "≡E"(2))
ultimately AOT_have ‹□(s ⊨ p & ¬p)›
by (metis "KBasic:3" "&I" "≡E"(3) "raa-cor:3")
AOT_hence ‹∃p □(s ⊨ p & ¬p)›
by (rule "∃I")
AOT_hence 1: ‹□∃q (s ⊨ q & ¬q)›
by (metis Buridan "vdash-properties:10")
AOT_have ‹□¬∀q (s ⊨ q → q)›
apply (AOT_subst ‹s ⊨ q → q› ‹¬(s ⊨ q & ¬q)› for: q)
apply (AOT_subst ‹¬∀q ¬(s ⊨ q & ¬q)› ‹∃q (s ⊨ q & ¬q)›)
by (auto simp: "conventions:4" "df-rules-formulas" "df-rules-formulas" "≡I" 1)
AOT_hence 0: ‹¬◇∀q (s ⊨ q → q)›
by (metis "≡⇩d⇩fE" "conventions:5" "raa-cor:3")
AOT_show ‹¬Possible(s)›
apply (AOT_subst ‹Possible(s)› ‹Situation(s) & ◇Actual(s)›)
apply (AOT_subst ‹Actual(s)› ‹Situation(s) & ∀q (s ⊨ q → q)›)
using actual "≡Df" apply presburger
by (metis "0" "KBasic2:3" "&E"(2) "raa-cor:3" "vdash-properties:10")
qed

AOT_theorem "pos-cons-sit:1": ‹Possible(s) → Consistent(s)›
by (auto simp: "sit-cons"[THEN "RM◇", THEN "→E",
THEN "cons-rigid:2"[THEN "≡E"(1)]]
intro!: "→I" dest!: pos[THEN "≡⇩d⇩fE"] "&E"(2))

AOT_theorem "pos-cons-sit:2": ‹∃s (Consistent(s) & ¬Possible(s))›
proof -
AOT_obtain q⇩1 where ‹q⇩1 & ◇¬q⇩1›
using "≡⇩d⇩fE" "instantiation" "cont-tf:1" "cont-tf-thm:1" by blast
have "cond-prop": ‹ConditionOnPropositionalProperties
(λ Π . «Π = [λy q⇩1 & ¬q⇩1]»)›
by (auto intro!: "cond-prop[I]" GEN "→I" "prop-prop1"[THEN "≡⇩d⇩fI"]
"∃I"(1)[where τ=‹«q⇩1 & ¬q⇩1»›, rotated, OF "log-prop-prop:2"])
have rigid: ‹rigid_condition (λ Π . «Π = [λy q⇩1 & ¬q⇩1]»)›
by (auto intro!: "strict-can:1[I]" GEN "→I" simp: "id-nec:2"[THEN "→E"])

AOT_obtain x where x_prop: ‹x = ❙ιs (∀F (s[F] ≡ F = [λy q⇩1 & ¬q⇩1]))›
using "ex:1:b"[THEN "∀E"(1), OF "can-sit-desc:1", OF "cond-prop"]
"∃E"[rotated] by blast
AOT_hence 0: ‹❙𝒜(Situation(x) & ∀F (x[F] ≡ F = [λy q⇩1 & ¬q⇩1]))›
using "→E" "actual-desc:2" by blast
AOT_hence ‹❙𝒜(Situation(x))› by (metis "Act-Basic:2" "&E"(1) "≡E"(1))
AOT_hence s_sit: ‹Situation(x)› by (metis "≡E"(1) "possit-sit:4")
AOT_have s_enc_prop: ‹∀F (x[F] ≡ F = [λy q⇩1 & ¬q⇩1])›
using "strict-sit"[OF rigid, OF "cond-prop", THEN "→E", OF x_prop].
AOT_hence ‹x[λy q⇩1 & ¬q⇩1]›
using "∀E"(1)[rotated, OF "prop-prop2:2"]
"rule=I:1"[OF "prop-prop2:2"] "≡E" by blast
AOT_hence ‹x ⊨ (q⇩1 & ¬q⇩1)›
using lem1[THEN "→E", OF s_sit, unvarify p, THEN "≡E"(2), OF "log-prop-prop:2"]
by blast
AOT_hence ‹□(x ⊨ (q⇩1 & ¬q⇩1))›
using "lem2:1"[unconstrain s, THEN "→E", OF s_sit, unvarify p,
OF "log-prop-prop:2", THEN "≡E"(1)] by blast
moreover AOT_have ‹□(x ⊨ (q⇩1 & ¬q⇩1) → ¬Actual(x))›
proof(rule RN; rule "→I"; rule "raa-cor:2")
AOT_modally_strict {
AOT_assume ‹Actual(x)›
AOT_hence ‹∀p (x ⊨ p → p)›
using actual[THEN "≡⇩d⇩fE", THEN "&E"(2)] by blast
moreover AOT_assume ‹x ⊨ (q⇩1 & ¬q⇩1)›
ultimately AOT_show ‹q⇩1 & ¬q⇩1›
using "∀E"(1)[rotated, OF "log-prop-prop:2"] "→E" by metis
}
qed
ultimately AOT_have nec_not_actual_s: ‹□¬Actual(x)›
using "qml:1"[axiom_inst, THEN "→E", THEN "→E"] by blast
AOT_have 1: ‹¬∃p (x ⊨ p & x ⊨ ¬p)›
proof (rule "raa-cor:2")
AOT_assume ‹∃p (x ⊨ p & x ⊨ ¬p)›
then AOT_obtain p where ‹x ⊨ p & x ⊨ ¬p›
using "∃E"[rotated] by blast
AOT_hence ‹x[λy p] & x[λy ¬p]›
using lem1[unvarify p, THEN "→E", OF "log-prop-prop:2",
OF s_sit, THEN "≡E"(1)] "&I" "&E" by metis
AOT_hence ‹[λy p] = [λy q⇩1 & ¬q⇩1]› and ‹[λy ¬p] = [λy q⇩1 & ¬q⇩1]›
by (auto intro!: "prop-prop2:2" s_enc_prop[THEN "∀E"(1), THEN "≡E"(1)]
elim: "&E")
AOT_hence i: ‹[λy p] = [λy ¬p]› by (metis "rule=E" id_sym)
{
AOT_assume 0: ‹p›
AOT_have ‹[λy p]x› for x
by (auto intro!: "β←C"(1) "cqt:2" 0)
AOT_hence ‹[λy ¬p]x› for x using i "rule=E" by fast
AOT_hence ‹¬p›
using "β→C"(1) by auto
}
moreover {
AOT_assume 0: ‹¬p›
AOT_have ‹[λy ¬p]x› for x
by (auto intro!: "β←C"(1) "cqt:2" 0)
AOT_hence ‹[λy p]x› for x using i[symmetric] "rule=E" by fast
AOT_hence ‹p›
using "β→C"(1) by auto
}
ultimately AOT_show ‹p & ¬p› for p by (metis "raa-cor:1" "raa-cor:3")
qed
AOT_have 2: ‹¬Possible(x)›
proof(rule "raa-cor:2")
AOT_assume ‹Possible(x)›
AOT_hence ‹◇Actual(x)›
by (metis "≡⇩d⇩fE" "&E"(2) pos)
moreover AOT_have ‹¬◇Actual(x)› using nec_not_actual_s
using "≡⇩d⇩fE" "conventions:5" "reductio-aa:2" by blast
ultimately AOT_show ‹◇Actual(x) & ¬◇Actual(x)› by (rule "&I")
qed
show ?thesis
by(rule "∃I"(2)[where β=x]; safe intro!: "&I" 2 s_sit cons[THEN "≡⇩d⇩fI"] 1)
qed

AOT_theorem "sit-classical:1": ‹∀p (s ⊨ p ≡ p) → ∀q(s ⊨ ¬q ≡ ¬s ⊨ q)›
proof(rule "→I"; rule GEN)
fix q
AOT_assume ‹∀p (s ⊨ p ≡ p)›
AOT_hence ‹s ⊨ q ≡ q› and ‹s ⊨ ¬q ≡ ¬q›
using "∀E"(1)[rotated, OF "log-prop-prop:2"] by blast+
AOT_thus ‹s ⊨ ¬q ≡ ¬s ⊨ q›
by (metis "deduction-theorem" "≡I" "≡E"(1) "≡E"(2) "≡E"(4))
qed

AOT_theorem "sit-classical:2":
‹∀p (s ⊨ p ≡ p) → ∀q∀r((s ⊨ (q → r)) ≡ (s ⊨ q → s ⊨ r))›
proof(rule "→I"; rule GEN; rule GEN)
fix q r
AOT_assume ‹∀p (s ⊨ p ≡ p)›
AOT_hence θ: ‹s ⊨ q ≡ q› and ξ: ‹s ⊨ r ≡ r› and ζ: ‹(s ⊨ (q → r)) ≡ (q → r)›
using "∀E"(1)[rotated, OF "log-prop-prop:2"] by blast+
AOT_show ‹(s ⊨ (q → r)) ≡ (s ⊨ q → s ⊨ r)›
proof (safe intro!: "≡I" "→I")
AOT_assume ‹s ⊨ (q → r)›
moreover AOT_assume ‹s ⊨ q›
ultimately AOT_show ‹s ⊨ r›
using θ ξ ζ by (metis "≡E"(1) "≡E"(2) "vdash-properties:10")
next
AOT_assume ‹s ⊨ q → s ⊨ r›
AOT_thus ‹s ⊨ (q → r)›
using θ ξ ζ by (metis "deduction-theorem" "≡E"(1) "≡E"(2) "→E")
qed
qed

AOT_theorem "sit-classical:3":
‹∀p (s ⊨ p ≡ p) → ((s ⊨ ∀α φ{α}) ≡ ∀α s ⊨ φ{α})›
proof (rule "→I")
AOT_assume ‹∀p (s ⊨ p ≡ p)›
AOT_hence θ: ‹s ⊨ φ{α} ≡ φ{α}› and ξ: ‹s ⊨ ∀α φ{α} ≡ ∀α φ{α}› for α
using "∀E"(1)[rotated, OF "log-prop-prop:2"] by blast+
AOT_show ‹s ⊨ ∀α φ{α} ≡ ∀α s ⊨ φ{α}›
proof (safe intro!: "≡I" "→I" GEN)
fix α
AOT_assume ‹s ⊨ ∀α φ{α}›
AOT_hence ‹φ{α}› using ξ "∀E"(2) "≡E"(1) by blast
AOT_thus ‹s ⊨ φ{α}› using θ "≡E"(2) by blast
next
AOT_assume ‹∀α s ⊨ φ{α}›
AOT_hence ‹s ⊨ φ{α}› for α using "∀E"(2) by blast
AOT_hence ‹φ{α}› for α using θ "≡E"(1) by blast
AOT_hence ‹∀α φ{α}› by (rule GEN)
AOT_thus ‹s ⊨ ∀α φ{α}› using ξ "≡E"(2) by blast
qed
qed

AOT_theorem "sit-classical:4": ‹∀p (s ⊨ p ≡ p) → ∀q (s ⊨ □q → □s ⊨ q)›
proof(rule "→I"; rule GEN; rule "→I")
fix q
AOT_assume ‹∀p (s ⊨ p ≡ p)›
AOT_hence θ: ‹s ⊨ q ≡ q› and ξ: ‹s ⊨ □q ≡ □q›
using "∀E"(1)[rotated, OF "log-prop-prop:2"] by blast+
AOT_assume ‹s ⊨ □q›
AOT_hence ‹□q› using ξ "≡E"(1) by blast
AOT_hence ‹q› using "qml:2"[axiom_inst, THEN "→E"] by blast
AOT_hence ‹s ⊨ q› using θ "≡E"(2) by blast
AOT_thus ‹□s ⊨ q› using "≡⇩d⇩fE" "&E"(1) "≡E"(1) "lem2:1" "true-in-s" by blast
qed

AOT_theorem "sit-classical:5":
‹∀p (s ⊨ p ≡ p) → ∃q(□(s ⊨ q) & ¬(s ⊨ □ q))›
proof (rule "→I")
AOT_obtain r where A: ‹r› and ‹◇¬r›
by (metis "&E"(1) "&E"(2) "≡⇩d⇩fE" "instantiation" "cont-tf:1" "cont-tf-thm:1")
AOT_hence B: ‹¬□r›
using "KBasic:11" "≡E"(2) by blast
moreover AOT_assume asm: ‹∀ p (s ⊨ p ≡ p)›
AOT_hence ‹s ⊨ r›
using "∀E"(2) A "≡E"(2) by blast
AOT_hence 1: ‹□s ⊨ r›
using "≡⇩d⇩fE" "&E"(1) "≡E"(1) "lem2:1" "true-in-s" by blast
AOT_have ‹s ⊨ ¬□r›
using asm[THEN "∀E"(1)[rotated, OF "log-prop-prop:2"], THEN "≡E"(2)] B by blast
AOT_hence ‹¬s ⊨ □r›
using "sit-classical:1"[THEN "→E", OF asm,
THEN "∀E"(1)[rotated, OF "log-prop-prop:2"], THEN "≡E"(1)] by blast
AOT_hence ‹□s ⊨ r & ¬s ⊨ □r›
using 1 "&I" by blast
AOT_thus ‹∃r (□s ⊨ r & ¬s ⊨ □r)›
by (rule "∃I")
qed

AOT_theorem "sit-classical:6":
‹∃s ∀p (s ⊨ p ≡ p)›
proof -
have "cond-prop": ‹ConditionOnPropositionalProperties
(λ Π . «∃q (q & Π = [λy q])»)›
proof (safe intro!: "cond-prop[I]" GEN "→I")
fix F
AOT_modally_strict {
AOT_assume ‹∃q (q & F = [λy q])›
then AOT_obtain q where ‹q & F = [λy q]›
using "∃E"[rotated] by blast
AOT_hence ‹F = [λy q]›
using "&E" by blast
AOT_hence ‹∃q F = [λy q]›
by (rule "∃I")
AOT_thus ‹Propositional([F])›
by (metis "≡⇩d⇩fI" "prop-prop1")
}
qed
AOT_have ‹∃s ∀F (s[F] ≡ ∃q (q & F = [λy q]))›
using "comp-sit:1"[OF "cond-prop"].
then AOT_obtain s⇩0 where s⇩0_prop: ‹∀F (s⇩0[F] ≡ ∃q (q & F = [λy q]))›
using "Situation.∃E"[rotated] by meson
AOT_have ‹∀p (s⇩0 ⊨ p ≡ p)›
proof(safe intro!: GEN "≡I" "→I")
fix p
AOT_assume ‹s⇩0 ⊨ p›
AOT_hence ‹s⇩0[λy p]›
using lem1[THEN "→E", OF Situation.ψ, THEN "≡E"(1)] by blast
AOT_hence ‹∃q (q & [λy p] = [λy q])›
using s⇩0_prop[THEN "∀E"(1)[rotated, OF "prop-prop2:2"], THEN "≡E"(1)] by blast
then AOT_obtain q⇩1 where q⇩1_prop: ‹q⇩1 & [λy p] = [λy q⇩1]›
using "∃E"[rotated] by blast
AOT_hence ‹p = q⇩1›
by (metis "&E"(2) "≡E"(2) "p-identity-thm2:3")
AOT_thus ‹p›
using q⇩1_prop[THEN "&E"(1)] "rule=E" id_sym by fast
next
fix p
AOT_assume ‹p›
moreover AOT_have ‹[λy p] = [λy p]›