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[2]" "≡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[2]",
THEN "act-cond"[THEN "→E"], THEN "→E"]
by blast
AOT_hence ‹❙𝒜Situation(⊤)›
using "T-sit"[unvarify x, OF true_den, THEN "RA[2]",
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[2]",
THEN "act-cond"[THEN "→E"], THEN "→E"]
by blast
AOT_hence ‹❙𝒜Situation(⊥)›
using "T-sit"[unvarify x, OF true_den, THEN "RA[2]",
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›
notepad
begin
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)›
by (simp add: Situation.ψ)
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[1]"[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[2]" "→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)›
by (simp add: "oth-class-taut:3:a" "universal-cor")
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›
by (simp add: "id-eq:1")
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))›
by (simp add: "A-objects!")
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])
(simp add: "rule=I:1" "prop-prop2:2")
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]))›
by (simp add: "A-objects!")
qed
AOT_theorem "thm-null-trivial:3": ‹❙ιx NullSituation(x)↓›
by (meson "A-Exists:2" "RA[2]" "≡E"(2) "thm-null-trivial:1")
AOT_theorem "thm-null-trivial:4": ‹❙ιx TrivialSituation(x)↓›
using "A-Exists:2" "RA[2]" "≡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)›
by (simp add: "null-uni-facts:4")
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[2]")
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[2]" "≡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[2]" 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
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[2]")
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')›
by (simp add: Situation.restricted_var_condition)
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'')›
by (simp add: Situation.restricted_var_condition)
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
by (simp add: 0)
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 (simp add: "oth-class-taut:1:a")
apply (AOT_subst ‹¬∀q ¬(s ⊨ q & ¬q)› ‹∃q (s ⊨ q & ¬q)›)
by (auto simp: "conventions:4" "df-rules-formulas[3]" "df-rules-formulas[4]" "≡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 (simp add: pos "≡Df")
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]›
by (simp add: "rule=I:1"[OF "prop-prop2:2"])
ultimately AOT_have ‹p & [λy p] = [λy p]›
using "&I" by blast
AOT_hence ‹∃q (q & [λy p] = [λy q])›
by (rule "∃I")
AOT_hence ‹s⇩0[λy p]›
using s⇩0_prop[THEN "∀E"(1)[rotated, OF "prop-prop2:2"], THEN "≡E"(2)] by blast
AOT_thus ‹s⇩0 ⊨ p›
using lem1[THEN "→E", OF Situation.ψ, THEN "≡E"(2)] by blast
qed
AOT_hence ‹∀p (s⇩0 ⊨ p ≡ p)›
using "&I" by blast
AOT_thus ‹∃s ∀p (s ⊨ p ≡ p)›
by (rule "Situation.∃I")
qed
AOT_define PossibleWorld :: ‹τ ⇒ φ› (‹PossibleWorld'(_')›)
"world:1": ‹PossibleWorld(x) ≡⇩d⇩f Situation(x) & ◇∀p(x ⊨ p ≡ p)›
AOT_theorem "world:2": ‹∃x PossibleWorld(x)›
proof -
AOT_obtain s where s_prop: ‹∀p (s ⊨ p ≡ p)›
using "sit-classical:6" "Situation.∃E"[rotated] by meson
AOT_have ‹∀p (s ⊨ p ≡ p)›
proof(safe intro!: GEN "≡I" "→I")
fix p
AOT_assume ‹s ⊨ p›
AOT_thus ‹p›
using s_prop[THEN "∀E"(2), THEN "≡E"(1)] by blast
next
fix p
AOT_assume ‹p›
AOT_thus ‹s ⊨ p›
using s_prop[THEN "∀E"(2), THEN "≡E"(2)] by blast
qed
AOT_hence ‹◇∀p (s ⊨ p ≡ p)›
by (metis "T◇"[THEN "→E"])
AOT_hence ‹◇∀p (s ⊨ p ≡ p)›
using s_prop "&I" by blast
AOT_hence ‹PossibleWorld(s)›
using "world:1"[THEN "≡⇩d⇩fI"] Situation.ψ "&I" by blast
AOT_thus ‹∃x PossibleWorld(x)›
by (rule "∃I")
qed
AOT_theorem "world:3": ‹PossibleWorld(κ) → κ↓›
proof (rule "→I")
AOT_assume ‹PossibleWorld(κ)›
AOT_hence ‹Situation(κ)›
using "world:1"[THEN "≡⇩d⇩fE"] "&E" by blast
AOT_hence ‹A!κ›
by (metis "≡⇩d⇩fE" "&E"(1) situations)
AOT_thus ‹κ↓›
by (metis "russell-axiom[exe,1].ψ_denotes_asm")
qed
AOT_theorem "rigid-pw:1": ‹PossibleWorld(x) ≡ □PossibleWorld(x)›
proof(safe intro!: "≡I" "→I")
AOT_assume ‹PossibleWorld(x)›
AOT_hence ‹Situation(x) & ◇∀p(x ⊨ p ≡ p)›
using "world:1"[THEN "≡⇩d⇩fE"] by blast
AOT_hence ‹□Situation(x) & □◇∀p(x ⊨ p ≡ p)›
by (metis "S5Basic:1" "&I" "&E"(1) "&E"(2) "≡E"(1) "possit-sit:1")
AOT_hence 0: ‹□(Situation(x) & ◇∀p(x ⊨ p ≡ p))›
by (metis "KBasic:3" "≡E"(2))
AOT_show ‹□PossibleWorld(x)›
by (AOT_subst ‹PossibleWorld(x)› ‹Situation(x) & ◇∀p(x ⊨ p ≡ p)›)
(auto simp: "≡Df" "world:1" 0)
next
AOT_show ‹PossibleWorld(x)› if ‹□PossibleWorld(x)›
using that "qml:2"[axiom_inst, THEN "→E"] by blast
qed
AOT_theorem "rigid-pw:2": ‹◇PossibleWorld(x) ≡ PossibleWorld(x)›
using "rigid-pw:1"
by (meson "RE◇" "S5Basic:2" "≡E"(2) "≡E"(6) "Commutativity of ≡")
AOT_theorem "rigid-pw:3": ‹◇PossibleWorld(x) ≡ □PossibleWorld(x)›
using "rigid-pw:1" "rigid-pw:2" by (meson "≡E"(5))
AOT_theorem "rigid-pw:4": ‹❙𝒜PossibleWorld(x) ≡ PossibleWorld(x)›
by (metis "Act-Sub:3" "→I" "≡I" "≡E"(6) "nec-imp-act" "rigid-pw:1" "rigid-pw:2")
AOT_register_rigid_restricted_type
PossibleWorld: ‹PossibleWorld(κ)›
proof
AOT_modally_strict {
AOT_show ‹∃x PossibleWorld(x)› using "world:2".
}
next
AOT_modally_strict {
AOT_show ‹PossibleWorld(κ) → κ↓› for κ using "world:3".
}
next
AOT_modally_strict {
AOT_show ‹∀α(PossibleWorld(α) → □PossibleWorld(α))›
by (meson GEN "→I" "≡E"(1) "rigid-pw:1")
}
qed
AOT_register_variable_names
PossibleWorld: w
AOT_theorem "world-pos": ‹Possible(w)›
proof (safe intro!: "≡⇩d⇩fE"[OF "world:1", OF PossibleWorld.ψ, THEN "&E"(1)]
pos[THEN "≡⇩d⇩fI"] "&I" )
AOT_have ‹◇∀p (w ⊨ p ≡ p)›
using "world:1"[THEN "≡⇩d⇩fE", OF PossibleWorld.ψ, THEN "&E"(2)].
AOT_hence ‹◇∀p (w ⊨ p → p)›
proof (rule "RM◇"[THEN "→E", rotated]; safe intro!: "→I" GEN)
AOT_modally_strict {
fix p
AOT_assume ‹∀p (w ⊨ p ≡ p)›
AOT_hence ‹w ⊨ p ≡ p› using "∀E"(2) by blast
moreover AOT_assume ‹w ⊨ p›
ultimately AOT_show p using "≡E"(1) by blast
}
qed
AOT_hence 0: ‹◇(Situation(w) & ∀p (w ⊨ p → p))›
using "world:1"[THEN "≡⇩d⇩fE", OF PossibleWorld.ψ, THEN "&E"(1),
THEN "possit-sit:1"[THEN "≡E"(1)]]
by (metis "KBasic:16" "&I" "vdash-properties:10")
AOT_show ‹◇Actual(w)›
by (AOT_subst ‹Actual(w)› ‹Situation(w) & ∀p (w ⊨ p → p)›)
(auto simp: actual "≡Df" 0)
qed
AOT_theorem "world-cons:1": ‹Consistent(w)›
using "world-pos"
using "pos-cons-sit:1"[unconstrain s, THEN "→E", THEN "→E"]
by (meson "≡⇩d⇩fE" "&E"(1) pos)
AOT_theorem "world-cons:2": ‹¬TrivialSituation(w)›
proof(rule "raa-cor:2")
AOT_assume ‹TrivialSituation(w)›
AOT_hence ‹Situation(w) & ∀p w ⊨ p›
using "df-null-trivial:2"[THEN "≡⇩d⇩fE"] by blast
AOT_hence 0: ‹□w ⊨ (∃p (p & ¬p))›
using "&E"
by (metis "Buridan◇" "T◇" "&E"(2) "≡E"(1) "lem2:3"[unconstrain s, THEN "→E"]
"log-prop-prop:2" "rule-ui:1" "universal-cor" "→E")
AOT_have ‹◇∀p (w ⊨ p ≡ p)›
using PossibleWorld.ψ "world:1"[THEN "≡⇩d⇩fE", THEN "&E"(2)] by metis
AOT_hence ‹∀p ◇(w ⊨ p ≡ p)›
using "Buridan◇"[THEN "→E"] by blast
AOT_hence ‹◇(w ⊨ (∃p (p & ¬p)) ≡ (∃p (p & ¬p)))›
by (metis "log-prop-prop:2" "rule-ui:1")
AOT_hence ‹◇(w ⊨ (∃p (p & ¬p)) → (∃p (p & ¬p)))›
using "RM◇"[THEN "→E"] "→I" "≡E"(1) by meson
AOT_hence ‹◇(∃p (p & ¬p))› using 0
by (metis "KBasic2:4" "≡E"(1) "→E")
moreover AOT_have ‹¬◇(∃p (p & ¬p))›
by (metis "instantiation" "KBasic2:1" RN "≡E"(1) "raa-cor:2")
ultimately AOT_show ‹◇(∃p (p & ¬p)) & ¬◇(∃p (p & ¬p))›
using "&I" by blast
qed
AOT_theorem "rigid-truth-at:1": ‹w ⊨ p ≡ □w ⊨ p›
using "lem2:1"[unconstrain s, THEN "→E",
OF PossibleWorld.ψ[THEN "world:1"[THEN "≡⇩d⇩fE"], THEN "&E"(1)]].
AOT_theorem "rigid-truth-at:2": ‹◇w ⊨ p ≡ w ⊨ p›
using "lem2:2"[unconstrain s, THEN "→E",
OF PossibleWorld.ψ[THEN "world:1"[THEN "≡⇩d⇩fE"], THEN "&E"(1)]].
AOT_theorem "rigid-truth-at:3": ‹◇w ⊨ p ≡ □w ⊨ p›
using "lem2:3"[unconstrain s, THEN "→E",
OF PossibleWorld.ψ[THEN "world:1"[THEN "≡⇩d⇩fE"], THEN "&E"(1)]].
AOT_theorem "rigid-truth-at:4": ‹❙𝒜w ⊨ p ≡ w ⊨ p›
using "lem2:4"[unconstrain s, THEN "→E",
OF PossibleWorld.ψ[THEN "world:1"[THEN "≡⇩d⇩fE"], THEN "&E"(1)]].
AOT_theorem "rigid-truth-at:5": ‹¬w ⊨ p ≡ □¬w ⊨ p›
using "lem2:5"[unconstrain s, THEN "→E",
OF PossibleWorld.ψ[THEN "world:1"[THEN "≡⇩d⇩fE"], THEN "&E"(1)]].
AOT_define Maximal :: ‹τ ⇒ φ› (‹Maximal'(_')›)
max: ‹Maximal(s) ≡⇩d⇩f ∀p (s ⊨ p ∨ s ⊨ ¬p)›
AOT_theorem "world-max": ‹Maximal(w)›
proof(safe intro!: PossibleWorld.ψ[THEN "≡⇩d⇩fE"[OF "world:1"], THEN "&E"(1)]
GEN "≡⇩d⇩fI"[OF max] "&I" )
fix q
AOT_have ‹◇(w ⊨ q ∨ w ⊨ ¬q)›
proof(rule "RM◇"[THEN "→E"]; (rule "→I")?)
AOT_modally_strict {
AOT_assume ‹∀p (w ⊨ p ≡ p)›
AOT_hence ‹w ⊨ q ≡ q› and ‹w ⊨ ¬q ≡ ¬q›
using "∀E"(1)[rotated, OF "log-prop-prop:2"] by blast+
AOT_thus ‹w ⊨ q ∨ w ⊨ ¬q›
by (metis "∨I"(1) "∨I"(2) "≡E"(3) "reductio-aa:1")
}
next
AOT_show ‹◇∀p (w ⊨ p ≡ p)›
using PossibleWorld.ψ[THEN "≡⇩d⇩fE"[OF "world:1"], THEN "&E"(2)].
qed
AOT_hence ‹◇w ⊨ q ∨ ◇w ⊨ ¬q›
using "KBasic2:2"[THEN "≡E"(1)] by blast
AOT_thus ‹w ⊨ q ∨ w ⊨ ¬q›
using "lem2:2"[unconstrain s, THEN "→E", unvarify p,
OF PossibleWorld.ψ[THEN "≡⇩d⇩fE"[OF "world:1"], THEN "&E"(1)],
THEN "≡E"(1), OF "log-prop-prop:2"]
by (metis "∨I"(1) "∨I"(2) "∨E"(3) "raa-cor:2")
qed
AOT_theorem "world=maxpos:1": ‹Maximal(x) → □Maximal(x)›
proof (AOT_subst ‹Maximal(x)› ‹Situation(x) & ∀p (x ⊨ p ∨ x ⊨ ¬p)›;
safe intro!: max "≡Df" "→I"; frule "&E"(1); drule "&E"(2))
AOT_assume sit_x: ‹Situation(x)›
AOT_hence nec_sit_x: ‹□Situation(x)›
by (metis "≡E"(1) "possit-sit:1")
AOT_assume ‹∀p (x ⊨ p ∨ x ⊨ ¬p)›
AOT_hence ‹x ⊨ p ∨ x ⊨ ¬p› for p
using "∀E"(1)[rotated, OF "log-prop-prop:2"] by blast
AOT_hence ‹□x ⊨ p ∨ □x ⊨ ¬p› for p
using "lem2:1"[unconstrain s, THEN "→E", OF sit_x, unvarify p,
OF "log-prop-prop:2", THEN "≡E"(1)]
by (metis "∨I"(1) "∨I"(2) "∨E"(2) "raa-cor:1")
AOT_hence ‹□(x ⊨ p ∨ x ⊨ ¬p)› for p
by (metis "KBasic:15" "→E")
AOT_hence ‹∀p □(x ⊨ p ∨ x ⊨ ¬p)›
by (rule GEN)
AOT_hence ‹□∀p (x ⊨ p ∨ x ⊨ ¬p)›
by (rule BF[THEN "→E"])
AOT_thus ‹□(Situation(x) & ∀p (x ⊨ p ∨ x ⊨ ¬p))›
using nec_sit_x by (metis "KBasic:3" "&I" "≡E"(2))
qed
AOT_theorem "world=maxpos:2": ‹PossibleWorld(x) ≡ Maximal(x) & Possible(x)›
proof(safe intro!: "≡I" "→I" "&I" "world-pos"[unconstrain w, THEN "→E"]
"world-max"[unconstrain w, THEN "→E"];
frule "&E"(2); drule "&E"(1))
AOT_assume pos_x: ‹Possible(x)›
AOT_have ‹◇(Situation(x) & ∀p(x ⊨ p → p))›
apply (AOT_subst (reverse) ‹Situation(x) & ∀p(x ⊨ p → p)› ‹Actual(x)›)
using actual "≡Df" apply presburger
using "≡⇩d⇩fE" "&E"(2) pos pos_x by blast
AOT_hence 0: ‹◇∀p(x ⊨ p → p)›
by (metis "KBasic2:3" "&E"(2) "vdash-properties:6")
AOT_assume max_x: ‹Maximal(x)›
AOT_hence sit_x: ‹Situation(x)› by (metis "≡⇩d⇩fE" max_x "&E"(1) max)
AOT_have ‹□Maximal(x)› using "world=maxpos:1"[THEN "→E", OF max_x] by simp
moreover AOT_have ‹□Maximal(x) → □(∀p(x ⊨ p → p) → ∀p (x ⊨ p ≡ p))›
proof(safe intro!: "→I" RM GEN)
AOT_modally_strict {
fix p
AOT_assume 0: ‹Maximal(x)›
AOT_assume 1: ‹∀p (x ⊨ p → p)›
AOT_show ‹x ⊨ p ≡ p›
proof(safe intro!: "≡I" "→I" 1[THEN "∀E"(2), THEN "→E"]; rule "raa-cor:1")
AOT_assume ‹¬x ⊨ p›
AOT_hence ‹x ⊨ ¬p›
using 0[THEN "≡⇩d⇩fE"[OF max], THEN "&E"(2), THEN "∀E"(2)]
1 by (metis "∨E"(2))
AOT_hence ‹¬p›
using 1[THEN "∀E"(1), OF "log-prop-prop:2", THEN "→E"] by blast
moreover AOT_assume p
ultimately AOT_show ‹p & ¬p› using "&I" by blast
qed
}
qed
ultimately AOT_have ‹□(∀p(x ⊨ p → p) → ∀p (x ⊨ p ≡ p))›
using "→E" by blast
AOT_hence ‹◇∀p(x ⊨ p → p) → ◇∀p(x ⊨ p ≡ p)›
by (metis "KBasic:13"[THEN "→E"])
AOT_hence ‹◇∀p(x ⊨ p ≡ p)›
using 0 "→E" by blast
AOT_thus ‹PossibleWorld(x)›
using "≡⇩d⇩fI"[OF "world:1", OF "&I", OF sit_x] by blast
qed
AOT_define NecImpl :: ‹φ ⇒ φ ⇒ φ› (infixl ‹⇒› 26)
"nec-impl-p:1": ‹p ⇒ q ≡⇩d⇩f □(p → q)›
AOT_define NecEquiv :: ‹φ ⇒ φ ⇒ φ› (infixl ‹⇔› 21)
"nec-impl-p:2": ‹p ⇔ q ≡⇩d⇩f (p ⇒ q) & (q ⇒ p)›
AOT_theorem "nec-equiv-nec-im": ‹p ⇔ q ≡ □(p ≡ q)›
proof(safe intro!: "≡I" "→I")
AOT_assume ‹p ⇔ q›
AOT_hence ‹(p ⇒ q)› and ‹(q ⇒ p)›
using "nec-impl-p:2"[THEN "≡⇩d⇩fE"] "&E" by blast+
AOT_hence ‹□(p → q)› and ‹□(q → p)›
using "nec-impl-p:1"[THEN "≡⇩d⇩fE"] by blast+
AOT_thus ‹□(p ≡ q)› by (metis "KBasic:4" "&I" "≡E"(2))
next
AOT_assume ‹□(p ≡ q)›
AOT_hence ‹□(p → q)› and ‹□(q → p)›
using "KBasic:4" "&E" "≡E"(1) by blast+
AOT_hence ‹(p ⇒ q)› and ‹(q ⇒ p)›
using "nec-impl-p:1"[THEN "≡⇩d⇩fI"] by blast+
AOT_thus ‹p ⇔ q›
using "nec-impl-p:2"[THEN "≡⇩d⇩fI"] "&I" by blast
qed
AOT_theorem world_closed_lem_1_a:
‹(s ⊨ (φ & ψ)) → (∀p (s ⊨ p ≡ p) → (s ⊨ φ & s ⊨ ψ))›
proof(safe intro!: "→I")
AOT_assume ‹∀ p (s ⊨ p ≡ p)›
AOT_hence ‹s ⊨ (φ & ψ) ≡ (φ & ψ)› and ‹s ⊨ φ ≡ φ› and ‹s ⊨ ψ ≡ ψ›
using "∀E"(1)[rotated, OF "log-prop-prop:2"] by blast+
moreover AOT_assume ‹s ⊨ (φ & ψ)›
ultimately AOT_show ‹s ⊨ φ & s ⊨ ψ›
by (metis "&I" "&E"(1) "&E"(2) "≡E"(1) "≡E"(2))
qed
AOT_theorem world_closed_lem_1_b:
‹(s ⊨ φ & (φ → q)) → (∀p (s ⊨ p ≡ p) → s ⊨ q)›
proof(safe intro!: "→I")
AOT_assume ‹∀ p (s ⊨ p ≡ p)›
AOT_hence ‹s ⊨ φ ≡ φ› for φ
using "∀E"(1)[rotated, OF "log-prop-prop:2"] by blast
moreover AOT_assume ‹s ⊨ φ & (φ → q)›
ultimately AOT_show ‹s ⊨ q›
by (metis "&E"(1) "&E"(2) "≡E"(1) "≡E"(2) "→E")
qed
AOT_theorem world_closed_lem_1_c:
‹(s ⊨ φ & s ⊨ (φ → ψ)) → (∀p (s ⊨ p ≡ p) → s ⊨ ψ)›
proof(safe intro!: "→I")
AOT_assume ‹∀ p (s ⊨ p ≡ p)›
AOT_hence ‹s ⊨ φ ≡ φ› for φ
using "∀E"(1)[rotated, OF "log-prop-prop:2"] by blast
moreover AOT_assume ‹s ⊨ φ & s ⊨ (φ → ψ)›
ultimately AOT_show ‹s ⊨ ψ›
by (metis "&E"(1) "&E"(2) "≡E"(1) "≡E"(2) "→E")
qed
AOT_theorem "world-closed-lem:1[0]":
‹q → (∀p (s ⊨ p ≡ p) → s ⊨ q)›
by (meson "→I" "≡E"(2) "log-prop-prop:2" "rule-ui:1")
AOT_theorem "world-closed-lem:1[1]":
‹s ⊨ p⇩1 & (p⇩1 → q) → (∀p (s ⊨ p ≡ p) → s ⊨ q)›
using world_closed_lem_1_b.
AOT_theorem "world-closed-lem:1[2]":
‹s ⊨ p⇩1 & s ⊨ p⇩2 & ((p⇩1 & p⇩2) → q) → (∀p (s ⊨ p ≡ p) → s ⊨ q)›
using world_closed_lem_1_b world_closed_lem_1_a
by (metis (full_types) "&I" "&E" "→I" "→E")
AOT_theorem "world-closed-lem:1[3]":
‹s ⊨ p⇩1 & s ⊨ p⇩2 & s ⊨ p⇩3 & ((p⇩1 & p⇩2 & p⇩3) → q) → (∀p (s ⊨ p ≡ p) → s ⊨ q)›
using world_closed_lem_1_b world_closed_lem_1_a
by (metis (full_types) "&I" "&E" "→I" "→E")
AOT_theorem "world-closed-lem:1[4]":
‹s ⊨ p⇩1 & s ⊨ p⇩2 & s ⊨ p⇩3 & s ⊨ p⇩4 & ((p⇩1 & p⇩2 & p⇩3 & p⇩4) → q) →
(∀p (s ⊨ p ≡ p) → s ⊨ q)›
using world_closed_lem_1_b world_closed_lem_1_a
by (metis (full_types) "&I" "&E" "→I" "→E")
AOT_theorem "coherent:1": ‹w ⊨ ¬p ≡ ¬w ⊨ p›
proof(safe intro!: "≡I" "→I")
AOT_assume 1: ‹w ⊨ ¬p›
AOT_show ‹¬w ⊨ p›
proof(rule "raa-cor:2")
AOT_assume ‹w ⊨ p›
AOT_hence ‹w ⊨ p & w ⊨ ¬p› using 1 "&I" by blast
AOT_hence ‹∃q (w ⊨ q & w ⊨ ¬q)› by (rule "∃I")
moreover AOT_have ‹¬∃q (w ⊨ q & w ⊨ ¬q)›
using "world-cons:1"[THEN "≡⇩d⇩fE"[OF cons], THEN "&E"(2)].
ultimately AOT_show ‹∃q (w ⊨ q & w ⊨ ¬q) & ¬∃q (w ⊨ q & w ⊨ ¬q)›
using "&I" by blast
qed
next
AOT_assume ‹¬w ⊨ p›
AOT_thus ‹w ⊨ ¬p›
using "world-max"[THEN "≡⇩d⇩fE"[OF max], THEN "&E"(2)]
by (metis "∨E"(2) "log-prop-prop:2" "rule-ui:1")
qed
AOT_theorem "coherent:2": ‹w ⊨ p ≡ ¬w ⊨ ¬p›
by (metis "coherent:1" "deduction-theorem" "≡I" "≡E"(1) "≡E"(2) "raa-cor:3")
AOT_theorem "act-world:1": ‹∃w ∀p (w ⊨ p ≡ p)›
proof -
AOT_obtain s where s_prop: ‹∀p (s ⊨ p ≡ p)›
using "sit-classical:6" "Situation.∃E"[rotated] by meson
AOT_hence ‹◇∀p (s ⊨ p ≡ p)›
by (metis "T◇" "vdash-properties:10")
AOT_hence ‹PossibleWorld(s)›
using "world:1"[THEN "≡⇩d⇩fI"] Situation.ψ "&I" by blast
AOT_hence ‹PossibleWorld(s) & ∀p (s ⊨ p ≡ p)›
using "&I" s_prop by blast
thus ?thesis by (rule "∃I")
qed
AOT_theorem "act-world:2": ‹∃!w Actual(w)›
proof -
AOT_obtain w where w_prop: ‹∀p (w ⊨ p ≡ p)›
using "act-world:1" "PossibleWorld.∃E"[rotated] by meson
AOT_have sit_s: ‹Situation(w)›
using PossibleWorld.ψ "world:1"[THEN "≡⇩d⇩fE", THEN "&E"(1)] by blast
show ?thesis
proof (safe intro!: "uniqueness:1"[THEN "≡⇩d⇩fI"] "∃I"(2) "&I" GEN "→I"
PossibleWorld.ψ actual[THEN "≡⇩d⇩fI"] sit_s
"sit-identity"[unconstrain s, unconstrain s', THEN "→E",
THEN "→E", THEN "≡E"(2)] "≡I"
w_prop[THEN "∀E"(2), THEN "≡E"(1)])
AOT_show ‹PossibleWorld(w)› using PossibleWorld.ψ.
next
AOT_show ‹Situation(w)›
by (simp add: sit_s)
next
fix y p
AOT_assume w_asm: ‹PossibleWorld(y) & Actual(y)›
AOT_assume ‹w ⊨ p›
AOT_hence p: ‹p›
using w_prop[THEN "∀E"(2), THEN "≡E"(1)] by blast
AOT_show ‹y ⊨ p›
proof(rule "raa-cor:1")
AOT_assume ‹¬y ⊨ p›
AOT_hence ‹y ⊨ ¬p›
by (metis "coherent:1"[unconstrain w, THEN "→E"] "&E"(1) "≡E"(2) w_asm)
AOT_hence ‹¬p›
using w_asm[THEN "&E"(2), THEN actual[THEN "≡⇩d⇩fE"], THEN "&E"(2),
THEN "∀E"(1), rotated, OF "log-prop-prop:2"]
"→E" by blast
AOT_thus ‹p & ¬p› using p "&I" by blast
qed
next
AOT_show ‹w ⊨ p› if ‹y ⊨ p› and ‹PossibleWorld(y) & Actual(y)› for p y
using that(2)[THEN "&E"(2), THEN actual[THEN "≡⇩d⇩fE"], THEN "&E"(2),
THEN "∀E"(2), THEN "→E", OF that(1)]
w_prop[THEN "∀E"(2), THEN "≡E"(2)] by blast
next
AOT_show ‹Situation(y)› if ‹PossibleWorld(y) & Actual(y)› for y
using that[THEN "&E"(1)] "world:1"[THEN "≡⇩d⇩fE", THEN "&E"(1)] by blast
next
AOT_show ‹Situation(w)›
using sit_s by blast
qed(simp)
qed
AOT_theorem "pre-walpha": ‹❙ιw Actual(w)↓›
using "A-Exists:2" "RA[2]" "act-world:2" "≡E"(2) by blast
AOT_define TheActualWorld :: ‹κ⇩s› (‹❙w⇩α›)
"w-alpha": ‹❙w⇩α =⇩d⇩f ❙ιw Actual(w)›
AOT_theorem true_in_truth_act_true: ‹⊤ ⊨ p ≡ ❙𝒜p›
proof(safe intro!: "≡I" "→I")
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_assume ‹⊤ ⊨ p›
AOT_hence ‹⊤[λy p]›
by (metis "≡⇩d⇩fE" "con-dis-i-e:2:b" "prop-enc" "true-in-s")
AOT_hence ‹❙ιx(A!x & ∀F (x[F] ≡ ∃q (q & F = [λy q])))[λy p]›
using "rule=E" true_def true_den by fast
AOT_hence ‹❙𝒜∃q (q & [λy p] = [λy q])›
using "≡E"(1) "desc-nec-encode:1"[unvarify F] "prop-prop2:2" by fast
AOT_hence ‹∃q ❙𝒜(q & [λy p] = [λy q])›
by (metis "Act-Basic:10" "≡E"(1))
then AOT_obtain q where ‹❙𝒜(q & [λy p] = [λy q])›
using "∃E"[rotated] by blast
AOT_hence actq: ‹❙𝒜q› and ‹❙𝒜[λy p] = [λy q]›
using "Act-Basic:2" "intro-elim:3:a" "&E" by blast+
AOT_hence ‹[λy p] = [λy q]›
using "id-act:1"[unvarify α β, THEN "≡E"(2)] "prop-prop2:2" by blast
AOT_hence ‹p = q›
by (metis "intro-elim:3:b" "p-identity-thm2:3")
AOT_thus ‹❙𝒜p›
using actq "rule=E" id_sym by blast
}
{
AOT_assume ‹❙𝒜p›
AOT_hence ‹❙𝒜(p & [λy p] = [λy p])›
by (auto intro!: "Act-Basic:2"[THEN "≡E"(2)] "&I"
intro: "RA[2]" "=I"(1)[OF "prop-prop2:2"])
AOT_hence ‹∃q ❙𝒜(q & [λy p] = [λy q])›
using "∃I" by fast
AOT_hence ‹❙𝒜∃q (q & [λy p] = [λy q])›
by (metis "Act-Basic:10" "≡E"(2))
AOT_hence ‹❙ιx(A!x & ∀F (x[F] ≡ ∃q (q & F = [λy q])))[λy p]›
using "≡E"(2) "desc-nec-encode:1"[unvarify F] "prop-prop2:2" by fast
AOT_hence ‹⊤[λy p]›
using "rule=E" true_def true_den id_sym by fast
AOT_thus ‹⊤ ⊨ p›
by (safe intro!: "true-in-s"[THEN "≡⇩d⇩fI"] "&I" "possit-sit:6"
"prop-enc"[THEN "≡⇩d⇩fI"] true_den)
}
qed
AOT_theorem "T-world": ‹⊤ = ❙w⇩α›
proof -
AOT_have true_den: ‹❙⊢⇩□ ⊤↓›
using "Situation.res-var:3" "possit-sit:6" "→E" by blast
AOT_have ‹❙𝒜∀p (⊤ ⊨ p → p)›
proof (safe intro!: "logic-actual-nec:3"[axiom_inst, THEN "≡E"(2)] GEN
"logic-actual-nec:2"[axiom_inst, THEN "≡E"(2)] "→I")
fix p
AOT_assume ‹❙𝒜⊤ ⊨ p›
AOT_hence ‹⊤ ⊨ p›
using "lem2:4"[unconstrain s, unvarify β, OF true_den,
THEN "→E", OF "possit-sit:6"] "≡E"(1) by blast
AOT_thus ‹❙𝒜p› using true_in_truth_act_true "≡E"(1) by blast
qed
moreover AOT_have ‹❙𝒜(Situation(κ) & ∀p (κ ⊨ p → p)) → ❙𝒜Actual(κ)› for κ
using actual[THEN "≡Df", THEN "conventions:3"[THEN "≡⇩d⇩fE", THEN "&E"(2)],
THEN "RA[2]", THEN "act-cond"[THEN "→E"]].
ultimately AOT_have act_act_true: ‹❙𝒜Actual(⊤)›
using "possit-sit:4"[unvarify x, OF true_den, THEN "≡E"(2), OF "possit-sit:6"]
"Act-Basic:2"[THEN "≡E"(2), OF "&I"] "→E" by blast
AOT_hence ‹◇Actual(⊤)› by (metis "Act-Sub:3" "vdash-properties:10")
AOT_hence ‹Possible(⊤)›
by (safe intro!: pos[THEN "≡⇩d⇩fI"] "&I" "possit-sit:6")
moreover AOT_have ‹Maximal(⊤)›
proof (safe intro!: max[THEN "≡⇩d⇩fI"] "&I" "possit-sit:6" GEN)
fix p
AOT_have ‹❙𝒜p ∨ ❙𝒜¬p›
by (simp add: "Act-Basic:1")
moreover AOT_have ‹⊤ ⊨ p› if ‹❙𝒜p›
using that true_in_truth_act_true[THEN "≡E"(2)] by blast
moreover AOT_have ‹⊤ ⊨ ¬p› if ‹❙𝒜¬p›
using that true_in_truth_act_true[unvarify p, THEN "≡E"(2)]
"log-prop-prop:2" by blast
ultimately AOT_show ‹⊤ ⊨ p ∨ ⊤ ⊨ ¬p›
using "∨I"(3) "→I" by blast
qed
ultimately AOT_have ‹PossibleWorld(⊤)›
by (safe intro!: "world=maxpos:2"[unvarify x, OF true_den, THEN "≡E"(2)] "&I")
AOT_hence ‹❙𝒜PossibleWorld(⊤)›
using "rigid-pw:4"[unvarify x, OF true_den, THEN "≡E"(2)] by blast
AOT_hence 1: ‹❙𝒜(PossibleWorld(⊤) & Actual(⊤))›
using act_act_true "Act-Basic:2" "df-simplify:2" "intro-elim:3:b" by blast
AOT_have ‹❙w⇩α = ❙ιw(Actual(w))›
using "rule-id-df:1[zero]"[OF "w-alpha", OF "pre-walpha"] by simp
moreover AOT_have w_act_den: ‹❙w⇩α↓›
using calculation "t=t-proper:1" "→E" by blast
ultimately AOT_have ‹∀z (❙𝒜(PossibleWorld(z) & Actual(z)) → z = ❙w⇩α)›
using "nec-hintikka-scheme"[unvarify x] "≡E"(1) "&E" by blast
AOT_thus ‹⊤ = ❙w⇩α›
using "∀E"(1)[rotated, OF true_den] 1 "→E" by blast
qed
AOT_act_theorem "truth-at-alpha:1": ‹p ≡ ❙w⇩α = ❙ιx (ExtensionOf(x, p))›
by (metis "rule=E" "T-world" "deduction-theorem" "ext-p-tv:3" id_sym "≡I"
"≡E"(1) "≡E"(2) "q-True:1")
AOT_act_theorem "truth-at-alpha:2": ‹p ≡ ❙w⇩α ⊨ p›
proof -
AOT_have ‹PossibleWorld(❙w⇩α)›
using "&E"(1) "pre-walpha" "rule-id-df:2:b[zero]" "→E"
"w-alpha" "y-in:3" by blast
AOT_hence sit_w_alpha: ‹Situation(❙w⇩α)›
by (metis "≡⇩d⇩fE" "&E"(1) "world:1")
AOT_have w_alpha_den: ‹❙w⇩α↓›
using "pre-walpha" "rule-id-df:2:b[zero]" "w-alpha" by blast
AOT_have ‹p ≡ ⊤❙Σp›
using "q-True:3" by force
moreover AOT_have ‹⊤ = ❙w⇩α›
using "T-world" by auto
ultimately AOT_have ‹p ≡ ❙w⇩α❙Σp›
using "rule=E" by fast
moreover AOT_have ‹❙w⇩α ❙Σ p ≡ ❙w⇩α ⊨ p›
using lem1[unvarify x, OF w_alpha_den, THEN "→E", OF sit_w_alpha]
using "≡S"(1) "≡E"(1) "Commutativity of ≡" "≡Df" sit_w_alpha "true-in-s" by blast
ultimately AOT_show ‹p ≡ ❙w⇩α ⊨ p›
by (metis "≡E"(5))
qed
AOT_theorem "alpha-world:1": ‹PossibleWorld(❙w⇩α)›
proof -
AOT_have 0: ‹❙w⇩α = ❙ιw Actual(w)›
using "pre-walpha" "rule-id-df:1[zero]" "w-alpha" by blast
AOT_hence walpha_den: ‹❙w⇩α↓›
by (metis "t=t-proper:1" "vdash-properties:6")
AOT_have ‹❙𝒜(PossibleWorld(❙w⇩α) & Actual(❙w⇩α))›
by (rule "actual-desc:2"[unvarify x, OF walpha_den, THEN "→E"]) (fact 0)
AOT_hence ‹❙𝒜PossibleWorld(❙w⇩α)›
by (metis "Act-Basic:2" "&E"(1) "≡E"(1))
AOT_thus ‹PossibleWorld(❙w⇩α)›
using "rigid-pw:4"[unvarify x, OF walpha_den, THEN "≡E"(1)]
by blast
qed
AOT_theorem "alpha-world:2": ‹Maximal(❙w⇩α)›
proof -
AOT_have ‹❙w⇩α↓›
using "pre-walpha" "rule-id-df:2:b[zero]" "w-alpha" by blast
then AOT_obtain x where x_def: ‹x = ❙w⇩α›
by (metis "instantiation" "rule=I:1" "existential:1" id_sym)
AOT_hence ‹PossibleWorld(x)› using "alpha-world:1" "rule=E" id_sym by fast
AOT_hence ‹Maximal(x)› by (metis "world-max"[unconstrain w, THEN "→E"])
AOT_thus ‹Maximal(❙w⇩α)› using x_def "rule=E" by blast
qed
AOT_theorem "t-at-alpha-strict": ‹❙w⇩α ⊨ p ≡ ❙𝒜p›
proof -
AOT_have 0: ‹❙w⇩α = ❙ιw Actual(w)›
using "pre-walpha" "rule-id-df:1[zero]" "w-alpha" by blast
AOT_hence walpha_den: ‹❙w⇩α↓›
by (metis "t=t-proper:1" "vdash-properties:6")
AOT_have 1: ‹❙𝒜(PossibleWorld(❙w⇩α) & Actual(❙w⇩α))›
by (rule "actual-desc:2"[unvarify x, OF walpha_den, THEN "→E"]) (fact 0)
AOT_have walpha_sit: ‹Situation(❙w⇩α)›
by (meson "≡⇩d⇩fE" "alpha-world:2" "&E"(1) max)
{
fix p
AOT_have 2: ‹Situation(x) → (❙𝒜x ⊨ p ≡ x ⊨ p)› for x
using "lem2:4"[unconstrain s] by blast
AOT_assume ‹❙w⇩α ⊨ p›
AOT_hence θ: ‹❙𝒜❙w⇩α ⊨ p›
using 2[unvarify x, OF walpha_den, THEN "→E", OF walpha_sit, THEN "≡E"(2)]
by argo
AOT_have 3: ‹❙𝒜Actual(❙w⇩α)›
using "1" "Act-Basic:2" "&E"(2) "≡E"(1) by blast
AOT_have ‹❙𝒜(Situation(❙w⇩α) & ∀q(❙w⇩α ⊨ q → q))›
apply (AOT_subst (reverse) ‹Situation(❙w⇩α) & ∀q(❙w⇩α ⊨ q → q)› ‹Actual(❙w⇩α)›)
using actual "≡Df" apply blast
by (fact 3)
AOT_hence ‹❙𝒜∀q(❙w⇩α ⊨ q → q)› by (metis "Act-Basic:2" "&E"(2) "≡E"(1))
AOT_hence ‹∀q ❙𝒜(❙w⇩α ⊨ q → q)›
using "logic-actual-nec:3"[axiom_inst, THEN "≡E"(1)] by blast
AOT_hence ‹❙𝒜(❙w⇩α ⊨ p → p)› using "∀E"(2) by blast
AOT_hence ‹❙𝒜(❙w⇩α ⊨ p) → ❙𝒜p› by (metis "act-cond" "vdash-properties:10")
AOT_hence ‹❙𝒜p› using θ "→E" by blast
}
AOT_hence 2: ‹❙w⇩α ⊨ p → ❙𝒜p› for p by (rule "→I")
AOT_have walpha_sit: ‹Situation(❙w⇩α)›
using "≡⇩d⇩fE" "alpha-world:2" "&E"(1) max by blast
show ?thesis
proof(safe intro!: "≡I" "→I" 2)
AOT_assume actp: ‹❙𝒜p›
AOT_show ‹❙w⇩α ⊨ p›
proof(rule "raa-cor:1")
AOT_assume ‹¬❙w⇩α ⊨ p›
AOT_hence ‹❙w⇩α ⊨ ¬p›
using "alpha-world:2"[THEN max[THEN "≡⇩d⇩fE"], THEN "&E"(2),
THEN "∀E"(1), OF "log-prop-prop:2"]
by (metis "∨E"(2))
AOT_hence ‹❙𝒜¬p›
using 2[unvarify p, OF "log-prop-prop:2", THEN "→E"] by blast
AOT_hence ‹¬❙𝒜p› by (metis "¬¬I" "Act-Sub:1" "≡E"(4))
AOT_thus ‹❙𝒜p & ¬❙𝒜p› using actp "&I" by blast
qed
qed
qed
AOT_act_theorem "not-act": ‹w ≠ ❙w⇩α → ¬Actual(w)›
proof (rule "→I"; rule "raa-cor:2")
AOT_assume ‹w ≠ ❙w⇩α›
AOT_hence 0: ‹¬(w = ❙w⇩α)› by (metis "≡⇩d⇩fE" "=-infix")
AOT_have walpha_den: ‹❙w⇩α↓›
using "pre-walpha" "rule-id-df:2:b[zero]" "w-alpha" by blast
AOT_have walpha_sit: ‹Situation(❙w⇩α)›
using "≡⇩d⇩fE" "alpha-world:2" "&E"(1) max by blast
AOT_assume act_w: ‹Actual(w)›
AOT_hence w_sit: ‹Situation(w)› by (metis "≡⇩d⇩fE" actual "&E"(1))
AOT_have sid: ‹Situation(x') → (w = x' ≡ ∀p (w ⊨ p ≡ x' ⊨ p))› for x'
using "sit-identity"[unconstrain s', unconstrain s, THEN "→E", OF w_sit]
by blast
AOT_have ‹w = ❙w⇩α›
proof(safe intro!: GEN sid[unvarify x', OF walpha_den, THEN "→E",
OF walpha_sit, THEN "≡E"(2)] "≡I" "→I")
fix p
AOT_assume ‹w ⊨ p›
AOT_hence ‹p›
using actual[THEN "≡⇩d⇩fE", OF act_w, THEN "&E"(2), THEN "∀E"(2), THEN "→E"]
by blast
AOT_hence ‹❙𝒜p›
by (metis "RA[1]")
AOT_thus ‹❙w⇩α ⊨ p›
using "t-at-alpha-strict"[THEN "≡E"(2)] by blast
next
fix p
AOT_assume ‹❙w⇩α ⊨ p›
AOT_hence ‹❙𝒜p›
using "t-at-alpha-strict"[THEN "≡E"(1)] by blast
AOT_hence p: ‹p›
using "logic-actual"[act_axiom_inst, THEN "→E"] by blast
AOT_show ‹w ⊨ p›
proof(rule "raa-cor:1")
AOT_assume ‹¬w ⊨ p›
AOT_hence ‹w ⊨ ¬p›
by (metis "coherent:1" "≡E"(2))
AOT_hence ‹¬p›
using actual[THEN "≡⇩d⇩fE", OF act_w, THEN "&E"(2), THEN "∀E"(1),
OF "log-prop-prop:2", THEN "→E"] by blast
AOT_thus ‹p & ¬p› using p "&I" by blast
qed
qed
AOT_thus ‹w = ❙w⇩α & ¬(w = ❙w⇩α)› using 0 "&I" by blast
qed
AOT_act_theorem "w-alpha-part": ‹Actual(s) ≡ s ⊴ ❙w⇩α›
proof(safe intro!: "≡I" "→I" "sit-part-whole"[THEN "≡⇩d⇩fI"] "&I" GEN
dest!: "sit-part-whole"[THEN "≡⇩d⇩fE"])
AOT_show ‹Situation(s)› if ‹Actual(s)›
using "≡⇩d⇩fE" actual "&E"(1) that by blast
next
AOT_show ‹Situation(❙w⇩α)›
using "≡⇩d⇩fE" "alpha-world:2" "&E"(1) max by blast
next
fix p
AOT_assume ‹Actual(s)›
moreover AOT_assume ‹s ⊨ p›
ultimately AOT_have ‹p›
using actual[THEN "≡⇩d⇩fE", THEN "&E"(2), THEN "∀E"(2), THEN "→E"] by blast
AOT_thus ‹❙w⇩α ⊨ p›
by (metis "≡E"(1) "truth-at-alpha:2")
next
AOT_assume 0: ‹Situation(s) & Situation(❙w⇩α) & ∀p (s ⊨ p → ❙w⇩α ⊨ p)›
AOT_hence ‹s ⊨ p → ❙w⇩α ⊨ p› for p
using "&E" "∀E"(2) by blast
AOT_hence ‹s ⊨ p → p› for p
by (metis "→I" "≡E"(2) "truth-at-alpha:2" "→E")
AOT_hence ‹∀p (s ⊨ p → p)› by (rule GEN)
AOT_thus ‹Actual(s)›
using actual[THEN "≡⇩d⇩fI", OF "&I", OF 0[THEN "&E"(1), THEN "&E"(1)]] by blast
qed
AOT_act_theorem "act-world2:1": ‹❙w⇩α ⊨ p ≡ [λy p]❙w⇩α›
apply (AOT_subst ‹[λy p]❙w⇩α› p)
apply (rule "beta-C-meta"[THEN "→E", OF "prop-prop2:2", unvarify ν⇩1ν⇩n])
using "pre-walpha" "rule-id-df:2:b[zero]" "w-alpha" apply blast
using "≡E"(2) "Commutativity of ≡" "truth-at-alpha:2" by blast
AOT_act_theorem "act-world2:2": ‹p ≡ ❙w⇩α ⊨ [λy p]❙w⇩α›
proof -
AOT_have ‹p ≡ [λy p]❙w⇩α›
apply (rule "beta-C-meta"[THEN "→E", OF "prop-prop2:2",
unvarify ν⇩1ν⇩n, symmetric])
using "pre-walpha" "rule-id-df:2:b[zero]" "w-alpha" by blast
also AOT_have ‹… ≡ ❙w⇩α ⊨ [λy p]❙w⇩α›
by (meson "log-prop-prop:2" "rule-ui:1" "truth-at-alpha:2" "universal-cor")
finally show ?thesis.
qed
AOT_theorem "fund-lem:1": ‹◇p → ◇∃w (w ⊨ p)›
proof (rule "RM◇"; rule "→I"; rule "raa-cor:1")
AOT_modally_strict {
AOT_obtain w where w_prop: ‹∀q (w ⊨ q ≡ q)›
using "act-world:1" "PossibleWorld.∃E"[rotated] by meson
AOT_assume p: ‹p›
AOT_assume 0: ‹¬∃w (w ⊨ p)›
AOT_have ‹∀w ¬(w ⊨ p)›
apply (AOT_subst ‹PossibleWorld(x) → ¬x ⊨ p›
‹¬(PossibleWorld(x) & x ⊨ p)› for: x)
apply (metis "&I" "&E"(1) "&E"(2) "→I" "≡I" "modus-tollens:2")
using "0" "cqt-further:4" "vdash-properties:10" by blast
AOT_hence ‹¬(w ⊨ p)›
using PossibleWorld.ψ "rule-ui:3" "→E" by blast
AOT_hence ‹¬p›
using w_prop[THEN "∀E"(2), THEN "≡E"(2)]
by (metis "raa-cor:3")
AOT_thus ‹p & ¬p›
using p "&I" by blast
}
qed
AOT_theorem "fund-lem:2": ‹◇∃w (w ⊨ p) → ∃w (w ⊨ p)›
proof (rule "→I")
AOT_assume ‹◇∃w (w ⊨ p)›
AOT_hence ‹∃w ◇(w ⊨ p)›
using "PossibleWorld.res-var-bound-reas[BF◇]"[THEN "→E"] by auto
then AOT_obtain w where ‹◇(w ⊨ p)›
using "PossibleWorld.∃E"[rotated] by meson
moreover AOT_have ‹Situation(w)›
by (metis "≡⇩d⇩fE" "&E"(1) pos "world-pos")
ultimately AOT_have ‹w ⊨ p›
using "lem2:2"[unconstrain s, THEN "→E"] "≡E" by blast
AOT_thus ‹∃w w ⊨ p›
by (rule "PossibleWorld.∃I")
qed
AOT_theorem "fund-lem:3": ‹p → ∀s(∀q (s ⊨ q ≡ q) → s ⊨ p)›
proof(safe intro!: "→I" Situation.GEN)
fix s
AOT_assume ‹p›
moreover AOT_assume ‹∀q (s ⊨ q ≡ q)›
ultimately AOT_show ‹s ⊨ p›
using "∀E"(2) "≡E"(2) by blast
qed
AOT_theorem "fund-lem:4": ‹□p → □∀s(∀q (s ⊨ q ≡ q) → s ⊨ p)›
using "fund-lem:3" by (rule RM)
AOT_theorem "fund-lem:5": ‹□∀s φ{s} → ∀s □φ{s}›
proof(safe intro!: "→I" Situation.GEN)
fix s
AOT_assume ‹□∀s φ{s}›
AOT_hence ‹∀s □φ{s}›
using "Situation.res-var-bound-reas[CBF]"[THEN "→E"] by blast
AOT_thus ‹□φ{s}›
using "Situation.∀E" by fast
qed
text‹Note: not explicit in PLM.›
AOT_theorem "fund-lem:5[world]": ‹□∀w φ{w} → ∀w □φ{w}›
proof(safe intro!: "→I" PossibleWorld.GEN)
fix w
AOT_assume ‹□∀w φ{w}›
AOT_hence ‹∀w □φ{w}›
using "PossibleWorld.res-var-bound-reas[CBF]"[THEN "→E"] by blast
AOT_thus ‹□φ{w}›
using "PossibleWorld.∀E" by fast
qed
AOT_theorem "fund-lem:6": ‹∀w w ⊨ p → □∀w w ⊨ p›
proof(rule "→I")
AOT_assume ‹∀w (w ⊨ p)›
AOT_hence 1: ‹PossibleWorld(w) → (w ⊨ p)› for w
using "∀E"(2) by blast
AOT_show ‹□∀w w ⊨ p›
proof(rule "raa-cor:1")
AOT_assume ‹¬□∀w w ⊨ p›
AOT_hence ‹◇¬∀w w ⊨ p›
by (metis "KBasic:11" "≡E"(1))
AOT_hence ‹◇∃x (¬(PossibleWorld(x) → x ⊨ p))›
apply (rule "RM◇"[THEN "→E", rotated])
by (simp add: "cqt-further:2")
AOT_hence ‹∃x ◇(¬(PossibleWorld(x) → x ⊨ p))›
by (metis "BF◇" "vdash-properties:10")
then AOT_obtain x where x_prop: ‹◇¬(PossibleWorld(x) → x ⊨ p)›
using "∃E"[rotated] by blast
AOT_have ‹◇(PossibleWorld(x) & ¬x ⊨ p)›
apply (AOT_subst ‹PossibleWorld(x) & ¬x ⊨ p›
‹¬(PossibleWorld(x) → x ⊨ p)›)
apply (meson "≡E"(6) "oth-class-taut:1:b" "oth-class-taut:3:a")
by(fact x_prop)
AOT_hence 2: ‹◇PossibleWorld(x) & ◇¬x ⊨ p›
by (metis "KBasic2:3" "vdash-properties:10")
AOT_hence ‹PossibleWorld(x)›
using "&E"(1) "≡E"(1) "rigid-pw:2" by blast
AOT_hence ‹□(x ⊨ p)›
using 2[THEN "&E"(2)] 1[unconstrain w, THEN "→E"] "→E"
"rigid-truth-at:1"[unconstrain w, THEN "→E"]
by (metis "≡E"(1))
moreover AOT_have ‹¬□(x ⊨ p)›
using 2[THEN "&E"(2)] by (metis "¬¬I" "KBasic:12" "≡E"(4))
ultimately AOT_show ‹p & ¬p› for p
by (metis "raa-cor:3")
qed
qed
AOT_theorem "fund-lem:7": ‹□∀w(w ⊨ p) → □p›
proof(rule RM; rule "→I")
AOT_modally_strict {
AOT_obtain w where w_prop: ‹∀p (w ⊨ p ≡ p)›
using "act-world:1" "PossibleWorld.∃E"[rotated] by meson
AOT_assume ‹∀w (w ⊨ p)›
AOT_hence ‹w ⊨ p›
using "PossibleWorld.∀E" by fast
AOT_thus ‹p›
using w_prop[THEN "∀E"(2), THEN "≡E"(1)] by blast
}
qed
AOT_theorem "fund:1": ‹◇p ≡ ∃w w ⊨ p›
proof (rule "≡I"; rule "→I")
AOT_assume ‹◇p›
AOT_thus ‹∃w w ⊨ p›
by (metis "fund-lem:1" "fund-lem:2" "→E")
next
AOT_assume ‹∃w w ⊨ p›
then AOT_obtain w where w_prop: ‹w ⊨ p›
using "PossibleWorld.∃E"[rotated] by meson
AOT_hence ‹◇∀p (w ⊨ p ≡ p)›
using "world:1"[THEN "≡⇩d⇩fE", THEN "&E"(2)] PossibleWorld.ψ "&E" by blast
AOT_hence ‹∀p ◇(w ⊨ p ≡ p)›
by (metis "Buridan◇" "→E")
AOT_hence 1: ‹◇(w ⊨ p ≡ p)›
by (metis "log-prop-prop:2" "rule-ui:1")
AOT_have ‹◇((w ⊨ p → p) & (p → w ⊨ p))›
apply (AOT_subst ‹(w ⊨ p → p) & (p → w ⊨ p)› ‹w ⊨ p ≡ p›)
apply (meson "conventions:3" "≡E"(6) "oth-class-taut:3:a" "≡Df")
by (fact 1)
AOT_hence ‹◇(w ⊨ p → p)›
by (metis "RM◇" "Conjunction Simplification"(1) "→E")
moreover AOT_have ‹□(w ⊨ p)›
using w_prop by (metis "≡E"(1) "rigid-truth-at:1")
ultimately AOT_show ‹◇p›
by (metis "KBasic2:4" "≡E"(1) "→E")
qed
AOT_theorem "fund:2": ‹□p ≡ ∀w (w ⊨ p)›
proof -
AOT_have 0: ‹∀w (w ⊨ ¬p ≡ ¬w ⊨ p)›
apply (rule PossibleWorld.GEN)
using "coherent:1" by blast
AOT_have ‹◇¬p ≡ ∃w (w ⊨ ¬p)›
using "fund:1"[unvarify p, OF "log-prop-prop:2"] by blast
also AOT_have ‹… ≡ ∃w ¬(w ⊨ p)›
proof(safe intro!: "≡I" "→I")
AOT_assume ‹∃w w ⊨ ¬p›
then AOT_obtain w where w_prop: ‹w ⊨ ¬p›
using "PossibleWorld.∃E"[rotated] by meson
AOT_hence ‹¬w ⊨ p›
using 0[THEN "PossibleWorld.∀E", THEN "≡E"(1)] "&E" by blast
AOT_thus ‹∃w ¬w ⊨ p›
by (rule "PossibleWorld.∃I")
next
AOT_assume ‹∃w ¬w ⊨ p›
then AOT_obtain w where w_prop: ‹¬w ⊨ p›
using "PossibleWorld.∃E"[rotated] by meson
AOT_hence ‹w ⊨ ¬p›
using 0[THEN "∀E"(2), THEN "→E", THEN "≡E"(1)] "&E"
by (metis "coherent:1" "≡E"(2))
AOT_thus ‹∃w w ⊨ ¬p›
by (rule "PossibleWorld.∃I")
qed
finally AOT_have ‹¬◇¬p ≡ ¬∃w ¬w ⊨ p›
by (meson "≡E"(1) "oth-class-taut:4:b")
AOT_hence ‹□p ≡ ¬∃w ¬w ⊨ p›
by (metis "KBasic:12" "≡E"(5))
also AOT_have ‹… ≡ ∀w w ⊨ p›
proof(safe intro!: "≡I" "→I")
AOT_assume ‹¬∃w ¬w ⊨ p›
AOT_hence 0: ‹∀x (¬(PossibleWorld(x) & ¬x ⊨ p))›
by (metis "cqt-further:4" "→E")
AOT_show ‹∀w w ⊨ p›
apply (AOT_subst ‹PossibleWorld(x) → x ⊨ p›
‹¬(PossibleWorld(x) & ¬x ⊨ p)› for: x)
using "oth-class-taut:1:a" apply presburger
by (fact 0)
next
AOT_assume 0: ‹∀w w ⊨ p›
AOT_have ‹∀x (¬(PossibleWorld(x) & ¬x ⊨ p))›
by (AOT_subst (reverse) ‹¬(PossibleWorld(x) & ¬x ⊨ p)›
‹PossibleWorld(x) → x ⊨ p› for: x)
(auto simp: "oth-class-taut:1:a" 0)
AOT_thus ‹¬∃w ¬w ⊨ p›
by (metis "∃E" "raa-cor:3" "rule-ui:3")
qed
finally AOT_show ‹□p ≡ ∀w w ⊨ p›.
qed
AOT_theorem "fund:3": ‹¬◇p ≡ ¬∃w w ⊨ p›
by (metis (full_types) "contraposition:1[1]" "→I" "fund:1" "≡I" "≡E"(1,2))
AOT_theorem "fund:4": ‹¬□p ≡ ∃w ¬w ⊨p›
apply (AOT_subst ‹∃w ¬w ⊨ p› ‹¬ ∀w w ⊨ p›)
apply (AOT_subst ‹PossibleWorld(x) → x ⊨ p›
‹¬(PossibleWorld(x) & ¬x ⊨ p)› for: x)
by (auto simp add: "oth-class-taut:1:a" "conventions:4" "≡Df" RN
"fund:2" "rule-sub-lem:1:a")
AOT_theorem "nec-dia-w:1": ‹□p ≡ ∃w w ⊨ □p›
proof -
AOT_have ‹□p ≡ ◇□p›
using "S5Basic:2" by blast
also AOT_have ‹... ≡ ∃w w ⊨ □p›
using "fund:1"[unvarify p, OF "log-prop-prop:2"] by blast
finally show ?thesis.
qed
AOT_theorem "nec-dia-w:2": ‹□p ≡ ∀w w ⊨ □p›
proof -
AOT_have ‹□p ≡ □□p›
using 4 "qml:2"[axiom_inst] "≡I" by blast
also AOT_have ‹... ≡ ∀w w ⊨ □p›
using "fund:2"[unvarify p, OF "log-prop-prop:2"] by blast
finally show ?thesis.
qed
AOT_theorem "nec-dia-w:3": ‹◇p ≡ ∃w w ⊨ ◇p›
proof -
AOT_have ‹◇p ≡ ◇◇p›
by (simp add: "4◇" "T◇" "≡I")
also AOT_have ‹... ≡ ∃w w ⊨ ◇p›
using "fund:1"[unvarify p, OF "log-prop-prop:2"] by blast
finally show ?thesis.
qed
AOT_theorem "nec-dia-w:4": ‹◇p ≡ ∀w w ⊨ ◇p›
proof -
AOT_have ‹◇p ≡ □◇p›
by (simp add: "S5Basic:1")
also AOT_have ‹... ≡ ∀w w ⊨ ◇p›
using "fund:2"[unvarify p, OF "log-prop-prop:2"] by blast
finally show ?thesis.
qed
AOT_theorem "conj-dist-w:1": ‹w ⊨ (p & q) ≡ ((w ⊨ p) & (w ⊨ q))›
proof(safe intro!: "≡I" "→I")
AOT_assume ‹w ⊨ (p & q)›
AOT_hence 0: ‹□w ⊨ (p & q)›
using "rigid-truth-at:1"[unvarify p, THEN "≡E"(1), OF "log-prop-prop:2"]
by blast
AOT_modally_strict {
AOT_have ‹∀p (w ⊨ p ≡ p) → ((w ⊨ (φ & ψ)) → (w ⊨ φ & w ⊨ ψ))› for w φ ψ
proof(safe intro!: "→I")
AOT_assume ‹∀ p (w ⊨ p ≡ p)›
AOT_hence ‹w ⊨ (φ & ψ) ≡ (φ & ψ)› and ‹w ⊨ φ ≡ φ› and ‹w ⊨ ψ ≡ ψ›
using "∀E"(1)[rotated, OF "log-prop-prop:2"] by blast+
moreover AOT_assume ‹w ⊨ (φ & ψ)›
ultimately AOT_show ‹w ⊨ φ & w ⊨ ψ›
by (metis "&I" "&E"(1) "&E"(2) "≡E"(1) "≡E"(2))
qed
}
AOT_hence ‹◇∀p (w ⊨ p ≡ p) → ◇(w ⊨ (φ & ψ) → w ⊨ φ & w ⊨ ψ)› for w φ ψ
by (rule "RM◇")
moreover AOT_have pos: ‹◇∀p (w ⊨ p ≡ p)›
using "world:1"[THEN "≡⇩d⇩fE", OF PossibleWorld.ψ] "&E" by blast
ultimately AOT_have ‹◇(w ⊨ (p & q) → w ⊨ p & w ⊨ q)› using "→E" by blast
AOT_hence ‹◇(w ⊨ p) & ◇(w ⊨ q)›
by (metis 0 "KBasic2:3" "KBasic2:4" "≡E"(1) "vdash-properties:10")
AOT_thus ‹w ⊨ p & w ⊨ q›
using "rigid-truth-at:2"[unvarify p, THEN "≡E"(1), OF "log-prop-prop:2"]
"&E" "&I" by meson
next
AOT_assume ‹w ⊨ p & w ⊨ q›
AOT_hence ‹□w ⊨ p & □w ⊨ q›
using "rigid-truth-at:1"[unvarify p, THEN "≡E"(1), OF "log-prop-prop:2"]
"&E" "&I" by blast
AOT_hence 0: ‹□(w ⊨ p & w ⊨ q)›
by (metis "KBasic:3" "≡E"(2))
AOT_modally_strict {
AOT_have ‹∀p (w ⊨ p ≡ p) → ((w ⊨ φ & w ⊨ ψ) → (w ⊨ (φ & ψ)))› for w φ ψ
proof(safe intro!: "→I")
AOT_assume ‹∀ p (w ⊨ p ≡ p)›
AOT_hence ‹w ⊨ (φ & ψ) ≡ (φ & ψ)› and ‹w ⊨ φ ≡ φ› and ‹w ⊨ ψ ≡ ψ›
using "∀E"(1)[rotated, OF "log-prop-prop:2"] by blast+
moreover AOT_assume ‹w ⊨ φ & w ⊨ ψ›
ultimately AOT_show ‹w ⊨ (φ & ψ)›
by (metis "&I" "&E"(1) "&E"(2) "≡E"(1) "≡E"(2))
qed
}
AOT_hence ‹◇∀p (w ⊨ p ≡ p) → ◇((w ⊨ φ & w ⊨ ψ) → w ⊨ (φ & ψ))› for w φ ψ
by (rule "RM◇")
moreover AOT_have pos: ‹◇∀p (w ⊨ p ≡ p)›
using "world:1"[THEN "≡⇩d⇩fE", OF PossibleWorld.ψ] "&E" by blast
ultimately AOT_have ‹◇((w ⊨ p & w ⊨ q) → w ⊨ (p & q))›
using "→E" by blast
AOT_hence ‹◇(w ⊨ (p & q))›
by (metis 0 "KBasic2:4" "≡E"(1) "vdash-properties:10")
AOT_thus ‹w ⊨ (p & q)›
using "rigid-truth-at:2"[unvarify p, THEN "≡E"(1), OF "log-prop-prop:2"]
by blast
qed
AOT_theorem "conj-dist-w:2": ‹w ⊨ (p → q) ≡ ((w ⊨ p) → (w ⊨ q))›
proof(safe intro!: "≡I" "→I")
AOT_assume ‹w ⊨ (p → q)›
AOT_hence 0: ‹□w ⊨ (p → q)›
using "rigid-truth-at:1"[unvarify p, THEN "≡E"(1), OF "log-prop-prop:2"]
by blast
AOT_assume ‹w ⊨ p›
AOT_hence 1: ‹□w ⊨ p›
by (metis "T◇" "≡E"(1) "rigid-truth-at:3" "→E")
AOT_modally_strict {
AOT_have ‹∀p (w ⊨ p ≡ p) → ((w ⊨ (φ → ψ)) → (w ⊨ φ → w ⊨ ψ))› for w φ ψ
proof(safe intro!: "→I")
AOT_assume ‹∀ p (w ⊨ p ≡ p)›
AOT_hence ‹w ⊨ (φ → ψ) ≡ (φ → ψ)› and ‹w ⊨ φ ≡ φ› and ‹w ⊨ ψ ≡ ψ›
using "∀E"(1)[rotated, OF "log-prop-prop:2"] by blast+
moreover AOT_assume ‹w ⊨ (φ → ψ)›
moreover AOT_assume ‹w ⊨ φ›
ultimately AOT_show ‹w ⊨ ψ›
by (metis "≡E"(1) "≡E"(2) "→E")
qed
}
AOT_hence ‹◇∀p (w ⊨ p ≡ p) → ◇(w ⊨ (φ → ψ) → (w ⊨ φ → w ⊨ ψ))› for w φ ψ
by (rule "RM◇")
moreover AOT_have pos: ‹◇∀p (w ⊨ p ≡ p)›
using "world:1"[THEN "≡⇩d⇩fE", OF PossibleWorld.ψ] "&E" by blast
ultimately AOT_have ‹◇(w ⊨ (p → q) → (w ⊨ p → w ⊨ q))›
using "→E" by blast
AOT_hence ‹◇(w ⊨ p → w ⊨ q)›
by (metis 0 "KBasic2:4" "≡E"(1) "→E")
AOT_hence ‹◇w ⊨ q›
by (metis 1 "KBasic2:4" "≡E"(1) "→E")
AOT_thus ‹w ⊨ q›
using "rigid-truth-at:2"[unvarify p, THEN "≡E"(1), OF "log-prop-prop:2"]
"&E" "&I" by meson
next
AOT_assume ‹w ⊨ p → w ⊨ q›
AOT_hence ‹¬(w ⊨ p) ∨ w ⊨ q›
by (metis "∨I"(1) "∨I"(2) "reductio-aa:1" "→E")
AOT_hence ‹w ⊨ ¬p ∨ w ⊨ q›
by (metis "coherent:1" "∨I"(1) "∨I"(2) "∨E"(2) "≡E"(2) "reductio-aa:1")
AOT_hence 0: ‹□(w ⊨ ¬p ∨ w ⊨ q)›
using "rigid-truth-at:1"[unvarify p, THEN "≡E"(1), OF "log-prop-prop:2"]
by (metis "KBasic:15" "∨I"(1) "∨I"(2) "∨E"(2) "reductio-aa:1" "→E")
AOT_modally_strict {
AOT_have ‹∀p (w ⊨ p ≡ p) → ((w ⊨ ¬φ ∨ w ⊨ ψ) → (w ⊨ (φ → ψ)))› for w φ ψ
proof(safe intro!: "→I")
AOT_assume ‹∀ p (w ⊨ p ≡ p)›
moreover AOT_assume ‹w ⊨ ¬φ ∨ w ⊨ ψ›
ultimately AOT_show ‹w ⊨ (φ → ψ)›
by (metis "∨E"(2) "→I" "≡E"(1) "≡E"(2) "log-prop-prop:2"
"reductio-aa:1" "rule-ui:1")
qed
}
AOT_hence ‹◇∀p (w ⊨ p ≡ p) → ◇((w ⊨ ¬φ ∨ w ⊨ ψ) → w ⊨ (φ → ψ))› for w φ ψ
by (rule "RM◇")
moreover AOT_have pos: ‹◇∀p (w ⊨ p ≡ p)›
using "world:1"[THEN "≡⇩d⇩fE", OF PossibleWorld.ψ] "&E" by blast
ultimately AOT_have ‹◇((w ⊨ ¬p ∨ w ⊨ q) → w ⊨ (p → q))›
using "→E" by blast
AOT_hence ‹◇(w ⊨ (p → q))›
by (metis 0 "KBasic2:4" "≡E"(1) "→E")
AOT_thus ‹w ⊨ (p → q)›
using "rigid-truth-at:2"[unvarify p, THEN "≡E"(1), OF "log-prop-prop:2"]
by blast
qed
AOT_theorem "conj-dist-w:3": ‹w ⊨ (p ∨ q) ≡ ((w ⊨ p) ∨ (w ⊨ q))›
proof(safe intro!: "≡I" "→I")
AOT_assume ‹w ⊨ (p ∨ q)›
AOT_hence 0: ‹□w ⊨ (p ∨ q)›
using "rigid-truth-at:1"[unvarify p, THEN "≡E"(1), OF "log-prop-prop:2"]
by blast
AOT_modally_strict {
AOT_have ‹∀p (w ⊨ p ≡ p) → ((w ⊨ (φ ∨ ψ)) → (w ⊨ φ ∨ w ⊨ ψ))› for w φ ψ
proof(safe intro!: "→I")
AOT_assume ‹∀ p (w ⊨ p ≡ p)›
AOT_hence ‹w ⊨ (φ ∨ ψ) ≡ (φ ∨ ψ)› and ‹w ⊨ φ ≡ φ› and ‹w ⊨ ψ ≡ ψ›
using "∀E"(1)[rotated, OF "log-prop-prop:2"] by blast+
moreover AOT_assume ‹w ⊨ (φ ∨ ψ)›
ultimately AOT_show ‹w ⊨ φ ∨ w ⊨ ψ›
by (metis "∨I"(1) "∨I"(2) "∨E"(3) "≡E"(1) "≡E"(2) "reductio-aa:1")
qed
}
AOT_hence ‹◇∀p (w ⊨ p ≡ p) → ◇(w ⊨ (φ ∨ ψ) → (w ⊨ φ ∨ w ⊨ ψ))› for w φ ψ
by (rule "RM◇")
moreover AOT_have pos: ‹◇∀p (w ⊨ p ≡ p)›
using "world:1"[THEN "≡⇩d⇩fE", OF PossibleWorld.ψ] "&E" by blast
ultimately AOT_have ‹◇(w ⊨ (p ∨ q) → (w ⊨ p ∨ w ⊨ q))› using "→E" by blast
AOT_hence ‹◇(w ⊨ p ∨ w ⊨ q)›
by (metis 0 "KBasic2:4" "≡E"(1) "vdash-properties:10")
AOT_hence ‹◇w ⊨ p ∨ ◇w ⊨ q›
using "KBasic2:2"[THEN "≡E"(1)] by blast
AOT_thus ‹w ⊨ p ∨ w ⊨ q›
using "rigid-truth-at:2"[unvarify p, THEN "≡E"(1), OF "log-prop-prop:2"]
by (metis "∨I"(1) "∨I"(2) "∨E"(2) "reductio-aa:1")
next
AOT_assume ‹w ⊨ p ∨ w ⊨ q›
AOT_hence 0: ‹□(w ⊨ p ∨ w ⊨ q)›
using "rigid-truth-at:1"[unvarify p, THEN "≡E"(1), OF "log-prop-prop:2"]
by (metis "KBasic:15" "∨I"(1) "∨I"(2) "∨E"(2) "reductio-aa:1" "→E")
AOT_modally_strict {
AOT_have ‹∀p (w ⊨ p ≡ p) → ((w ⊨ φ ∨ w ⊨ ψ) → (w ⊨ (φ ∨ ψ)))› for w φ ψ
proof(safe intro!: "→I")
AOT_assume ‹∀ p (w ⊨ p ≡ p)›
moreover AOT_assume ‹w ⊨ φ ∨ w ⊨ ψ›
ultimately AOT_show ‹w ⊨ (φ ∨ ψ)›
by (metis "∨I"(1) "∨I"(2) "∨E"(2) "≡E"(1) "≡E"(2)
"log-prop-prop:2" "reductio-aa:1" "rule-ui:1")
qed
}
AOT_hence ‹◇∀p (w ⊨ p ≡ p) → ◇((w ⊨ φ ∨ w ⊨ ψ) → w ⊨ (φ ∨ ψ))› for w φ ψ
by (rule "RM◇")
moreover AOT_have pos: ‹◇∀p (w ⊨ p ≡ p)›
using "world:1"[THEN "≡⇩d⇩fE", OF PossibleWorld.ψ] "&E" by blast
ultimately AOT_have ‹◇((w ⊨ p ∨ w ⊨ q) → w ⊨ (p ∨ q))›
using "→E" by blast
AOT_hence ‹◇(w ⊨ (p ∨ q))›
by (metis 0 "KBasic2:4" "≡E"(1) "→E")
AOT_thus ‹w ⊨ (p ∨ q)›
using "rigid-truth-at:2"[unvarify p, THEN "≡E"(1), OF "log-prop-prop:2"]
by blast
qed
AOT_theorem "conj-dist-w:4": ‹w ⊨ (p ≡ q) ≡ ((w ⊨ p) ≡ (w ⊨ q))›
proof(rule "≡I"; rule "→I")
AOT_assume ‹w ⊨ (p ≡ q)›
AOT_hence 0: ‹□w ⊨ (p ≡ q)›
using "rigid-truth-at:1"[unvarify p, THEN "≡E"(1), OF "log-prop-prop:2"]
by blast
AOT_modally_strict {
AOT_have ‹∀p (w ⊨ p ≡ p) → ((w ⊨ (φ ≡ ψ)) → (w ⊨ φ ≡ w ⊨ ψ))› for w φ ψ
proof(safe intro!: "→I")
AOT_assume ‹∀ p (w ⊨ p ≡ p)›
AOT_hence ‹w ⊨ (φ ≡ ψ) ≡ (φ ≡ ψ)› and ‹w ⊨ φ ≡ φ› and ‹w ⊨ ψ ≡ ψ›
using "∀E"(1)[rotated, OF "log-prop-prop:2"] by blast+
moreover AOT_assume ‹w ⊨ (φ ≡ ψ)›
ultimately AOT_show ‹w ⊨ φ ≡ w ⊨ ψ›
by (metis "≡E"(2) "≡E"(5) "Commutativity of ≡")
qed
}
AOT_hence ‹◇∀p (w ⊨ p ≡ p) → ◇(w ⊨ (φ ≡ ψ) → (w ⊨ φ ≡ w ⊨ ψ))› for w φ ψ
by (rule "RM◇")
moreover AOT_have pos: ‹◇∀p (w ⊨ p ≡ p)›
using "world:1"[THEN "≡⇩d⇩fE", OF PossibleWorld.ψ] "&E" by blast
ultimately AOT_have ‹◇(w ⊨ (p ≡ q) → (w ⊨ p ≡ w ⊨ q))›
using "→E" by blast
AOT_hence 1: ‹◇(w ⊨ p ≡ w ⊨ q)›
by (metis 0 "KBasic2:4" "≡E"(1) "vdash-properties:10")
AOT_have ‹◇((w ⊨ p → w ⊨ q) & (w ⊨ q → w ⊨ p))›
apply (AOT_subst ‹(w ⊨ p → w ⊨ q) & (w ⊨ q → w ⊨ p)› ‹w ⊨ p ≡ w ⊨ q›)
apply (meson "≡⇩d⇩fE" "conventions:3" "→I" "df-rules-formulas[4]" "≡I")
by (fact 1)
AOT_hence 2: ‹◇(w ⊨ p → w ⊨ q) & ◇(w ⊨ q → w ⊨ p)›
by (metis "KBasic2:3" "vdash-properties:10")
AOT_have ‹◇(¬w ⊨ p ∨ w ⊨ q)› and ‹◇(¬w ⊨ q ∨ w ⊨ p)›
apply (AOT_subst (reverse) ‹¬w ⊨ p ∨ w ⊨ q› ‹w ⊨ p → w ⊨ q›)
apply (simp add: "oth-class-taut:1:c")
apply (fact 2[THEN "&E"(1)])
apply (AOT_subst (reverse) ‹¬w ⊨ q ∨ w ⊨ p› ‹w ⊨ q → w ⊨ p›)
apply (simp add: "oth-class-taut:1:c")
by (fact 2[THEN "&E"(2)])
AOT_hence ‹◇(¬w ⊨ p) ∨ ◇w ⊨ q› and ‹◇¬w ⊨ q ∨ ◇w ⊨ p›
using "KBasic2:2" "≡E"(1) by blast+
AOT_hence ‹¬□w ⊨ p ∨ ◇w ⊨ q› and ‹¬□w ⊨ q ∨ ◇w ⊨ p›
by (metis "KBasic:11" "∨I"(1) "∨I"(2) "∨E"(2) "≡E"(2) "raa-cor:1")+
AOT_thus ‹w ⊨ p ≡ w ⊨ q›
using "rigid-truth-at:2"[unvarify p, THEN "≡E"(1), OF "log-prop-prop:2"]
by (metis "¬¬I" "T◇" "∨E"(2) "→I" "≡I" "≡E"(1) "rigid-truth-at:3")
next
AOT_have ‹□PossibleWorld(w)›
using "≡E"(1) "rigid-pw:1" PossibleWorld.ψ by blast
moreover {
fix p
AOT_modally_strict {
AOT_have ‹PossibleWorld(w) → (w ⊨ p → □w ⊨ p)›
using "rigid-truth-at:1" "→I"
by (metis "≡E"(1))
}
AOT_hence ‹□PossibleWorld(w) → □(w ⊨ p → □w ⊨ p)›
by (rule RM)
}
ultimately AOT_have 1: ‹□(w ⊨ p → □w ⊨ p)› for p
by (metis "→E")
AOT_assume ‹w ⊨ p ≡ w ⊨ q›
AOT_hence 0: ‹□(w ⊨ p ≡ w ⊨ q)›
using "sc-eq-box-box:5"[THEN "→E", THEN "qml:2"[axiom_inst, THEN "→E"],
THEN "→E", OF "&I"]
by (metis "1")
AOT_modally_strict {
AOT_have ‹∀p (w ⊨ p ≡ p) → ((w ⊨ φ ≡ w ⊨ ψ) → (w ⊨ (φ ≡ ψ)))› for w φ ψ
proof(safe intro!: "→I")
AOT_assume ‹∀ p (w ⊨ p ≡ p)›
moreover AOT_assume ‹w ⊨ φ ≡ w ⊨ ψ›
ultimately AOT_show ‹w ⊨ (φ ≡ ψ)›
by (metis "≡E"(2) "≡E"(6) "log-prop-prop:2" "rule-ui:1")
qed
}
AOT_hence ‹◇∀p (w ⊨ p ≡ p) → ◇((w ⊨ φ ≡ w ⊨ ψ) → w ⊨ (φ ≡ ψ))› for w φ ψ
by (rule "RM◇")
moreover AOT_have pos: ‹◇∀p (w ⊨ p ≡ p)›
using "world:1"[THEN "≡⇩d⇩fE", OF PossibleWorld.ψ] "&E" by blast
ultimately AOT_have ‹◇((w ⊨ p ≡ w ⊨ q) → w ⊨ (p ≡ q))›
using "→E" by blast
AOT_hence ‹◇(w ⊨ (p ≡ q))›
by (metis 0 "KBasic2:4" "≡E"(1) "→E")
AOT_thus ‹w ⊨ (p ≡ q)›
using "rigid-truth-at:2"[unvarify p, THEN "≡E"(1), OF "log-prop-prop:2"]
by blast
qed
AOT_theorem "conj-dist-w:5": ‹w ⊨ (∀α φ{α}) ≡ (∀ α (w ⊨ φ{α}))›
proof(safe intro!: "≡I" "→I" GEN)
AOT_assume ‹w ⊨ (∀α φ{α})›
AOT_hence 0: ‹□w ⊨ (∀α φ{α})›
using "rigid-truth-at:1"[unvarify p, THEN "≡E"(1), OF "log-prop-prop:2"]
by blast
AOT_modally_strict {
AOT_have ‹∀p (w ⊨ p ≡ p) → ((w ⊨ (∀α φ{α})) → (∀α w ⊨ φ{α}))› for w
proof(safe intro!: "→I" GEN)
AOT_assume ‹∀p (w ⊨ p ≡ p)›
moreover AOT_assume ‹w ⊨ (∀α φ{α})›
ultimately AOT_show ‹w ⊨ φ{α}› for α
by (metis "≡E"(1) "≡E"(2) "log-prop-prop:2" "rule-ui:1" "rule-ui:3")
qed
}
AOT_hence ‹◇∀p (w ⊨ p ≡ p) → ◇(w ⊨ (∀α φ{α}) → (∀α w ⊨ φ{α}))› for w
by (rule "RM◇")
moreover AOT_have pos: ‹◇∀p (w ⊨ p ≡ p)›
using "world:1"[THEN "≡⇩d⇩fE", OF PossibleWorld.ψ] "&E" by blast
ultimately AOT_have ‹◇(w ⊨ (∀α φ{α}) → (∀α w ⊨ φ{α}))› using "→E" by blast
AOT_hence ‹◇(∀α w ⊨ φ{α})›
by (metis 0 "KBasic2:4" "≡E"(1) "→E")
AOT_hence ‹∀α ◇w ⊨ φ{α}›
by (metis "Buridan◇" "→E")
AOT_thus ‹w ⊨ φ{α}› for α
using "rigid-truth-at:2"[unvarify p, THEN "≡E"(1), OF "log-prop-prop:2"]
"∀E"(2) by blast
next
AOT_assume ‹∀α w ⊨ φ{α}›
AOT_hence ‹w ⊨ φ{α}› for α using "∀E"(2) by blast
AOT_hence ‹□w ⊨ φ{α}› for α
using "rigid-truth-at:1"[unvarify p, THEN "≡E"(1), OF "log-prop-prop:2"]
"&E" "&I" by blast
AOT_hence ‹∀α □w ⊨ φ{α}› by (rule GEN)
AOT_hence 0: ‹□∀α w ⊨ φ{α}› by (rule BF[THEN "→E"])
AOT_modally_strict {
AOT_have ‹∀p (w ⊨ p ≡ p) → ((∀α w ⊨ φ{α}) → (w ⊨ (∀α φ{α})))› for w
proof(safe intro!: "→I")
AOT_assume ‹∀ p (w ⊨ p ≡ p)›
moreover AOT_assume ‹∀α w ⊨ φ{α}›
ultimately AOT_show ‹w ⊨ (∀α φ{α})›
by (metis "≡E"(1) "≡E"(2) "log-prop-prop:2" "rule-ui:1"
"rule-ui:3" "universal-cor")
qed
}
AOT_hence ‹◇∀p (w ⊨ p ≡ p) → ◇((∀α w ⊨ φ{α}) → w ⊨ (∀α φ{α}))› for w
by (rule "RM◇")
moreover AOT_have pos: ‹◇∀p (w ⊨ p ≡ p)›
using "world:1"[THEN "≡⇩d⇩fE", OF PossibleWorld.ψ] "&E" by blast
ultimately AOT_have ‹◇((∀α w ⊨ φ{α}) → w ⊨ (∀α φ{α}))›
using "→E" by blast
AOT_hence ‹◇(w ⊨ (∀α φ{α}))›
by (metis 0 "KBasic2:4" "≡E"(1) "→E")
AOT_thus ‹w ⊨ (∀α φ{α})›
using "rigid-truth-at:2"[unvarify p, THEN "≡E"(1), OF "log-prop-prop:2"]
by blast
qed
AOT_theorem "conj-dist-w:6": ‹w ⊨ (∃α φ{α}) ≡ (∃ α (w ⊨ φ{α}))›
proof(safe intro!: "≡I" "→I" GEN)
AOT_assume ‹w ⊨ (∃α φ{α})›
AOT_hence 0: ‹□w ⊨ (∃α φ{α})›
using "rigid-truth-at:1"[unvarify p, THEN "≡E"(1), OF "log-prop-prop:2"]
by blast
AOT_modally_strict {
AOT_have ‹∀p (w ⊨ p ≡ p) → ((w ⊨ (∃α φ{α})) → (∃α w ⊨ φ{α}))› for w
proof(safe intro!: "→I" GEN)
AOT_assume ‹∀p (w ⊨ p ≡ p)›
moreover AOT_assume ‹w ⊨ (∃α φ{α})›
ultimately AOT_show ‹∃ α (w ⊨ φ{α})›
by (metis "∃E" "∃I"(2) "≡E"(1,2) "log-prop-prop:2" "rule-ui:1")
qed
}
AOT_hence ‹◇∀p (w ⊨ p ≡ p) → ◇(w ⊨ (∃α φ{α}) → (∃α w ⊨ φ{α}))› for w
by (rule "RM◇")
moreover AOT_have pos: ‹◇∀p (w ⊨ p ≡ p)›
using "world:1"[THEN "≡⇩d⇩fE", OF PossibleWorld.ψ] "&E" by blast
ultimately AOT_have ‹◇(w ⊨ (∃α φ{α}) → (∃α w ⊨ φ{α}))› using "→E" by blast
AOT_hence ‹◇(∃α w ⊨ φ{α})›
by (metis 0 "KBasic2:4" "≡E"(1) "→E")
AOT_hence ‹∃α ◇w ⊨ φ{α}›
by (metis "BF◇" "→E")
then AOT_obtain α where ‹◇w ⊨ φ{α}›
using "∃E"[rotated] by blast
AOT_hence ‹w ⊨ φ{α}›
using "rigid-truth-at:2"[unvarify p, THEN "≡E"(1), OF "log-prop-prop:2"] by blast
AOT_thus ‹∃ α w ⊨ φ{α}› by (rule "∃I")
next
AOT_assume ‹∃α w ⊨ φ{α}›
then AOT_obtain α where ‹w ⊨ φ{α}› using "∃E"[rotated] by blast
AOT_hence ‹□w ⊨ φ{α}›
using "rigid-truth-at:1"[unvarify p, THEN "≡E"(1), OF "log-prop-prop:2"]
"&E" "&I" by blast
AOT_hence ‹∃α □w ⊨ φ{α}›
by (rule "∃I")
AOT_hence 0: ‹□∃α w ⊨ φ{α}›
by (metis Buridan "→E")
AOT_modally_strict {
AOT_have ‹∀p (w ⊨ p ≡ p) → ((∃α w ⊨ φ{α}) → (w ⊨ (∃α φ{α})))› for w
proof(safe intro!: "→I")
AOT_assume ‹∀ p (w ⊨ p ≡ p)›
moreover AOT_assume ‹∃α w ⊨ φ{α}›
then AOT_obtain α where ‹w ⊨ φ{α}›
using "∃E"[rotated] by blast
ultimately AOT_show ‹w ⊨ (∃α φ{α})›
by (metis "∃I"(2) "≡E"(1,2) "log-prop-prop:2" "rule-ui:1")
qed
}
AOT_hence ‹◇∀p (w ⊨ p ≡ p) → ◇((∃α w ⊨ φ{α}) → w ⊨ (∃α φ{α}))› for w
by (rule "RM◇")
moreover AOT_have pos: ‹◇∀p (w ⊨ p ≡ p)›
using "world:1"[THEN "≡⇩d⇩fE", OF PossibleWorld.ψ] "&E" by blast
ultimately AOT_have ‹◇((∃α w ⊨ φ{α}) → w ⊨ (∃α φ{α}))›
using "→E" by blast
AOT_hence ‹◇(w ⊨ (∃α φ{α}))›
by (metis 0 "KBasic2:4" "≡E"(1) "→E")
AOT_thus ‹w ⊨ (∃α φ{α})›
using "rigid-truth-at:2"[unvarify p, THEN "≡E"(1), OF "log-prop-prop:2"]
by blast
qed
AOT_theorem "conj-dist-w:7": ‹(w ⊨ □p) → □w ⊨ p›
proof(rule "→I")
AOT_assume ‹w ⊨ □p›
AOT_hence ‹∃w w ⊨ □p› by (rule "PossibleWorld.∃I")
AOT_hence ‹◇□p› using "fund:1"[unvarify p, OF "log-prop-prop:2", THEN "≡E"(2)]
by blast
AOT_hence ‹□p›
by (metis "5◇" "→E")
AOT_hence 1: ‹□□p›
by (metis "S5Basic:6" "≡E"(1))
AOT_have ‹□∀w w ⊨ p›
by (AOT_subst (reverse) ‹∀w w ⊨ p› ‹□p›)
(auto simp add: "fund:2" 1)
AOT_hence ‹∀w □w ⊨ p›
using "fund-lem:5[world]"[THEN "→E"] by simp
AOT_thus ‹□w ⊨ p›
using "→E" "PossibleWorld.∀E" by fast
qed
AOT_theorem "conj-dist-w:8": ‹∃w∃p((□w ⊨ p) & ¬w ⊨ □p)›
proof -
AOT_obtain r where A: r and ‹◇¬r›
by (metis "&E"(1) "&E"(2) "≡⇩d⇩fE" "∃E" "cont-tf:1" "cont-tf-thm:1")
AOT_hence B: ‹¬□r›
by (metis "KBasic:11" "≡E"(2))
AOT_have ‹◇r›
using A "T◇"[THEN "→E"] by simp
AOT_hence ‹∃w w ⊨ r›
using "fund:1"[THEN "≡E"(1)] by blast
then AOT_obtain w where w: ‹w ⊨ r›
using "PossibleWorld.∃E"[rotated] by meson
AOT_hence ‹□w ⊨ r›
by (metis "T◇" "≡E"(1) "rigid-truth-at:3" "vdash-properties:10")
moreover AOT_have ‹¬w ⊨ □r›
proof(rule "raa-cor:2")
AOT_assume ‹w ⊨ □r›
AOT_hence ‹∃w w ⊨ □r›
by (rule "PossibleWorld.∃I")
AOT_hence ‹□r›
by (metis "≡E"(2) "nec-dia-w:1")
AOT_thus ‹□r & ¬□r›
using B "&I" by blast
qed
ultimately AOT_have ‹□w ⊨ r & ¬w ⊨ □r›
by (rule "&I")
AOT_hence ‹∃p (□w ⊨ p & ¬w ⊨ □p)›
by (rule "∃I")
thus ?thesis
by (rule "PossibleWorld.∃I")
qed
AOT_theorem "conj-dist-w:9": ‹(◇w ⊨ p) → w ⊨ ◇p›
proof(rule "→I"; rule "raa-cor:1")
AOT_assume ‹◇w ⊨ p›
AOT_hence 0: ‹w ⊨ p›
by (metis "≡E"(1) "rigid-truth-at:2")
AOT_assume ‹¬w ⊨ ◇p›
AOT_hence 1: ‹w ⊨ ¬◇p›
using "coherent:1"[unvarify p, THEN "≡E"(2), OF "log-prop-prop:2"] by blast
moreover AOT_have ‹w ⊨ (¬◇p → ¬p)›
using "T◇"[THEN "contraposition:1[1]", THEN RN]
"fund:2"[unvarify p, OF "log-prop-prop:2", THEN "≡E"(1), THEN "∀E"(2),
THEN "→E", rotated, OF PossibleWorld.ψ]
by blast
ultimately AOT_have ‹w ⊨ ¬p›
using "conj-dist-w:2"[unvarify p q, OF "log-prop-prop:2", OF "log-prop-prop:2",
THEN "≡E"(1), THEN "→E"]
by blast
AOT_hence ‹w ⊨ p & w ⊨ ¬p› using 0 "&I" by blast
AOT_thus ‹p & ¬p›
by (metis "coherent:1" "Conjunction Simplification"(1,2) "≡E"(4)
"modus-tollens:1" "raa-cor:3")
qed
AOT_theorem "conj-dist-w:10": ‹∃w∃p((w ⊨ ◇p) & ¬◇w ⊨ p)›
proof -
AOT_obtain w where w: ‹∀p (w ⊨ p ≡ p)›
using "act-world:1" "PossibleWorld.∃E"[rotated] by meson
AOT_obtain r where ‹¬r› and ‹◇r›
using "cont-tf-thm:2" "cont-tf:2"[THEN "≡⇩d⇩fE"] "&E" "∃E"[rotated] by metis
AOT_hence ‹w ⊨ ¬r› and 0: ‹w ⊨ ◇r›
using w[THEN "∀E"(1), OF "log-prop-prop:2", THEN "≡E"(2)] by blast+
AOT_hence ‹¬w ⊨ r› using "coherent:1"[THEN "≡E"(1)] by blast
AOT_hence ‹¬◇w ⊨ r› by (metis "≡E"(4) "rigid-truth-at:2")
AOT_hence ‹w ⊨ ◇r & ¬◇w ⊨ r› using 0 "&I" by blast
AOT_hence ‹∃p (w ⊨ ◇p & ¬◇w ⊨ p)› by (rule "∃I")
thus ?thesis by (rule "PossibleWorld.∃I")
qed
AOT_theorem "two-worlds-exist:1": ‹∃p(ContingentlyTrue(p)) → ∃w (¬Actual(w))›
proof(rule "→I")
AOT_assume ‹∃p ContingentlyTrue(p)›
then AOT_obtain p where ‹ContingentlyTrue(p)›
using "∃E"[rotated] by blast
AOT_hence p: ‹p & ◇¬p›
by (metis "≡⇩d⇩fE" "cont-tf:1")
AOT_hence ‹∃w w ⊨ ¬p›
using "fund:1"[unvarify p, OF "log-prop-prop:2", THEN "≡E"(1)] "&E" by blast
then AOT_obtain w where w: ‹w ⊨ ¬p›
using "PossibleWorld.∃E"[rotated] by meson
AOT_have ‹¬Actual(w)›
proof(rule "raa-cor:2")
AOT_assume ‹Actual(w)›
AOT_hence ‹w ⊨ p›
using p[THEN "&E"(1)] actual[THEN "≡⇩d⇩fE", THEN "&E"(2)]
by (metis "log-prop-prop:2" "raa-cor:3" "rule-ui:1" "→E" w)
moreover AOT_have ‹¬(w ⊨ p)›
by (metis "coherent:1" "≡E"(4) "reductio-aa:2" w)
ultimately AOT_show ‹w ⊨ p & ¬(w ⊨ p)›
using "&I" by blast
qed
AOT_thus ‹∃w ¬Actual(w)›
by (rule "PossibleWorld.∃I")
qed
AOT_theorem "two-worlds-exist:2": ‹∃p(ContingentlyFalse(p)) → ∃w (¬Actual(w))›
proof(rule "→I")
AOT_assume ‹∃p ContingentlyFalse(p)›
then AOT_obtain p where ‹ContingentlyFalse(p)›
using "∃E"[rotated] by blast
AOT_hence p: ‹¬p & ◇p›
by (metis "≡⇩d⇩fE" "cont-tf:2")
AOT_hence ‹∃w w ⊨ p›
using "fund:1"[unvarify p, OF "log-prop-prop:2", THEN "≡E"(1)] "&E" by blast
then AOT_obtain w where w: ‹w ⊨ p›
using "PossibleWorld.∃E"[rotated] by meson
moreover AOT_have ‹¬Actual(w)›
proof(rule "raa-cor:2")
AOT_assume ‹Actual(w)›
AOT_hence ‹w ⊨ ¬p›
using p[THEN "&E"(1)] actual[THEN "≡⇩d⇩fE", THEN "&E"(2)]
by (metis "log-prop-prop:2" "raa-cor:3" "rule-ui:1" "→E" w)
moreover AOT_have ‹¬(w ⊨ p)›
using calculation by (metis "coherent:1" "≡E"(4) "reductio-aa:2")
AOT_thus ‹w ⊨ p & ¬(w ⊨ p)›
using "&I" w by metis
qed
AOT_thus ‹∃w ¬Actual(w)›
by (rule "PossibleWorld.∃I")
qed
AOT_theorem "two-worlds-exist:3": ‹∃w ¬Actual(w)›
using "cont-tf-thm:1" "two-worlds-exist:1" "→E" by blast
AOT_theorem "two-worlds-exist:4": ‹∃w∃w'(w ≠ w')›
proof -
AOT_obtain w where w: ‹Actual(w)›
using "act-world:2"[THEN "uniqueness:1"[THEN "≡⇩d⇩fE"],
THEN "cqt-further:5"[THEN "→E"]]
"PossibleWorld.∃E"[rotated] "&E"
by blast
moreover AOT_obtain w' where w': ‹¬Actual(w')›
using "two-worlds-exist:3" "PossibleWorld.∃E"[rotated] by meson
AOT_have ‹¬(w = w')›
proof(rule "raa-cor:2")
AOT_assume ‹w = w'›
AOT_thus ‹p & ¬p› for p
using w w' "&E" by (metis "rule=E" "raa-cor:3")
qed
AOT_hence ‹w ≠ w'›
by (metis "≡⇩d⇩fI" "=-infix")
AOT_hence ‹∃w' w ≠ w'›
by (rule "PossibleWorld.∃I")
thus ?thesis
by (rule "PossibleWorld.∃I")
qed
AOT_theorem "w-rel:1": ‹[λx φ{x}]↓ → [λx w ⊨ φ{x}]↓›
proof(rule "→I")
AOT_assume ‹[λx φ{x}]↓›
AOT_hence ‹□[λx φ{x}]↓›
by (metis "exist-nec" "→E")
moreover AOT_have
‹□[λx φ{x}]↓ → □∀x∀y(∀F([F]x ≡ [F]y) → ((w ⊨ φ{x}) ≡ ( w ⊨ φ{y})))›
proof (rule RM; rule "→I"; rule GEN; rule GEN; rule "→I")
AOT_modally_strict {
fix x y
AOT_assume ‹[λx φ{x}]↓›
AOT_hence ‹∀x∀y (∀F ([F]x ≡ [F]y) → □(φ{x} ≡ φ{y}))›
using "&E" "kirchner-thm-cor:1"[THEN "→E"] by blast
AOT_hence ‹∀F ([F]x ≡ [F]y) → □(φ{x} ≡ φ{y})›
using "∀E"(2) by blast
moreover AOT_assume ‹∀F ([F]x ≡ [F]y)›
ultimately AOT_have ‹□(φ{x} ≡ φ{y})›
using "→E" by blast
AOT_hence ‹∀w (w ⊨ (φ{x} ≡ φ{y}))›
using "fund:2"[unvarify p, OF "log-prop-prop:2", THEN "≡E"(1)] by blast
AOT_hence ‹w ⊨ (φ{x} ≡ φ{y})›
using "∀E"(2) using PossibleWorld.ψ "→E" by blast
AOT_thus ‹(w ⊨ φ{x}) ≡ (w ⊨ φ{y})›
using "conj-dist-w:4"[unvarify p q, OF "log-prop-prop:2",
OF "log-prop-prop:2", THEN "≡E"(1)] by blast
}
qed
ultimately AOT_have ‹□∀x∀y(∀F([F]x ≡ [F]y) → ((w ⊨ φ{x}) ≡ ( w ⊨ φ{y})))›
using "→E" by blast
AOT_thus ‹[λx w ⊨ φ{x}]↓›
using "kirchner-thm:1"[THEN "≡E"(2)] by fast
qed
AOT_theorem "w-rel:2": ‹[λx⇩1...x⇩n φ{x⇩1...x⇩n}]↓ → [λx⇩1...x⇩n w ⊨ φ{x⇩1...x⇩n}]↓›
proof(rule "→I")
AOT_assume ‹[λx⇩1...x⇩n φ{x⇩1...x⇩n}]↓›
AOT_hence ‹□[λx⇩1...x⇩n φ{x⇩1...x⇩n}]↓›
by (metis "exist-nec" "→E")
moreover AOT_have ‹□[λx⇩1...x⇩n φ{x⇩1...x⇩n}]↓ → □∀x⇩1...∀x⇩n∀y⇩1...∀y⇩n(
∀F([F]x⇩1...x⇩n ≡ [F]y⇩1...y⇩n) → ((w ⊨ φ{x⇩1...x⇩n}) ≡ ( w ⊨ φ{y⇩1...y⇩n})))›
proof (rule RM; rule "→I"; rule GEN; rule GEN; rule "→I")
AOT_modally_strict {
fix x⇩1x⇩n y⇩1y⇩n
AOT_assume ‹[λx⇩1...x⇩n φ{x⇩1...x⇩n}]↓›
AOT_hence ‹∀x⇩1...∀x⇩n∀y⇩1...∀y⇩n (
∀F ([F]x⇩1...x⇩n ≡ [F]y⇩1...y⇩n) → □(φ{x⇩1...x⇩n} ≡ φ{y⇩1...y⇩n}))›
using "&E" "kirchner-thm-cor:2"[THEN "→E"] by blast
AOT_hence ‹∀F ([F]x⇩1...x⇩n ≡ [F]y⇩1...y⇩n) → □(φ{x⇩1...x⇩n} ≡ φ{y⇩1...y⇩n})›
using "∀E"(2) by blast
moreover AOT_assume ‹∀F ([F]x⇩1...x⇩n ≡ [F]y⇩1...y⇩n)›
ultimately AOT_have ‹□(φ{x⇩1...x⇩n} ≡ φ{y⇩1...y⇩n})›
using "→E" by blast
AOT_hence ‹∀w (w ⊨ (φ{x⇩1...x⇩n} ≡ φ{y⇩1...y⇩n}))›
using "fund:2"[unvarify p, OF "log-prop-prop:2", THEN "≡E"(1)] by blast
AOT_hence ‹w ⊨ (φ{x⇩1...x⇩n} ≡ φ{y⇩1...y⇩n})›
using "∀E"(2) using PossibleWorld.ψ "→E" by blast
AOT_thus ‹(w ⊨ φ{x⇩1...x⇩n}) ≡ (w ⊨ φ{y⇩1...y⇩n})›
using "conj-dist-w:4"[unvarify p q, OF "log-prop-prop:2",
OF "log-prop-prop:2", THEN "≡E"(1)] by blast
}
qed
ultimately AOT_have ‹□∀x⇩1...∀x⇩n∀y⇩1...∀y⇩n(
∀F([F]x⇩1...x⇩n ≡ [F]y⇩1...y⇩n) → ((w ⊨ φ{x⇩1...x⇩n}) ≡ ( w ⊨ φ{y⇩1...y⇩n})))›
using "→E" by blast
AOT_thus ‹[λx⇩1...x⇩n w ⊨ φ{x⇩1...x⇩n}]↓›
using "kirchner-thm:2"[THEN "≡E"(2)] by fast
qed
AOT_theorem "w-rel:3": ‹[λx⇩1...x⇩n w ⊨ [F]x⇩1...x⇩n]↓›
by (rule "w-rel:2"[THEN "→E"]) "cqt:2[lambda]"
AOT_define WorldIndexedRelation :: ‹Π ⇒ τ ⇒ Π› (‹_⇩_›)
"w-index": ‹[F]⇩w =⇩d⇩f [λx⇩1...x⇩n w ⊨ [F]x⇩1...x⇩n]›
AOT_define Rigid :: ‹τ ⇒ φ› (‹Rigid'(_')›)
"df-rigid-rel:1":
‹Rigid(F) ≡⇩d⇩f F↓ & □∀x⇩1...∀x⇩n([F]x⇩1...x⇩n → □[F]x⇩1...x⇩n)›
AOT_define Rigidifies :: ‹τ ⇒ τ ⇒ φ› (‹Rigidifies'(_,_')›)
"df-rigid-rel:2":
‹Rigidifies(F, G) ≡⇩d⇩f Rigid(F) & ∀x⇩1...∀x⇩n([F]x⇩1...x⇩n ≡ [G]x⇩1...x⇩n)›
AOT_theorem "rigid-der:1": ‹[[F]⇩w]x⇩1...x⇩n ≡ w ⊨ [F]x⇩1...x⇩n›
apply (rule "rule-id-df:2:b[2]"[where τ="λ (Π, κ). «[Π]⇩κ»" and
σ="λ(Π, κ). «[λx⇩1...x⇩n κ ⊨ [Π]x⇩1...x⇩n]»",
simplified, OF "w-index"])
apply (fact "w-rel:3")
apply (rule "beta-C-meta"[THEN "→E"])
by (fact "w-rel:3")
AOT_theorem "rigid-der:2": ‹Rigid([G]⇩w)›
proof(safe intro!: "≡⇩d⇩fI"[OF "df-rigid-rel:1"] "&I")
AOT_show ‹[G]⇩w↓›
by (rule "rule-id-df:2:b[2]"[where τ="λ (Π, κ). «[Π]⇩κ»" and
σ="λ(Π, κ). «[λx⇩1...x⇩n κ ⊨ [Π]x⇩1...x⇩n]»",
simplified, OF "w-index"])
(fact "w-rel:3")+
next
AOT_have ‹□∀x⇩1...∀x⇩n ([[G]⇩w]x⇩1...x⇩n → □[[G]⇩w]x⇩1...x⇩n)›
proof(rule RN; safe intro!: "→I" GEN)
AOT_modally_strict {
AOT_have assms: ‹PossibleWorld(w)› using PossibleWorld.ψ.
AOT_hence nec_pw_w: ‹□PossibleWorld(w)›
using "≡E"(1) "rigid-pw:1" by blast
fix x⇩1x⇩n
AOT_assume ‹[[G]⇩w]x⇩1...x⇩n›
AOT_hence ‹[λx⇩1...x⇩n w ⊨ [G]x⇩1...x⇩n]x⇩1...x⇩n›
using "rule-id-df:2:a[2]"[where τ="λ (Π, κ). «[Π]⇩κ»" and
σ="λ(Π, κ). «[λx⇩1...x⇩n κ ⊨ [Π]x⇩1...x⇩n]»",
simplified, OF "w-index", OF "w-rel:3"]
by fast
AOT_hence ‹w ⊨ [G]x⇩1...x⇩n›
by (metis "β→C"(1))
AOT_hence ‹□w ⊨ [G]x⇩1...x⇩n›
using "rigid-truth-at:1"[unvarify p, OF "log-prop-prop:2", THEN "≡E"(1)]
by blast
moreover AOT_have ‹□w ⊨ [G]x⇩1...x⇩n → □[λx⇩1...x⇩n w ⊨ [G]x⇩1...x⇩n]x⇩1...x⇩n›
proof (rule RM; rule "→I")
AOT_modally_strict {
AOT_assume ‹w ⊨ [G]x⇩1...x⇩n›
AOT_thus ‹[λx⇩1...x⇩n w ⊨ [G]x⇩1...x⇩n]x⇩1...x⇩n›
by (auto intro!: "β←C"(1) simp: "w-rel:3" "cqt:2")
}
qed
ultimately AOT_have 1: ‹□[λx⇩1...x⇩n w ⊨ [G]x⇩1...x⇩n]x⇩1...x⇩n›
using "→E" by blast
AOT_show ‹□[[G]⇩w]x⇩1...x⇩n›
by (rule "rule-id-df:2:b[2]"[where τ="λ (Π, κ). «[Π]⇩κ»" and
σ="λ(Π, κ). «[λx⇩1...x⇩n κ ⊨ [Π]x⇩1...x⇩n]»",
simplified, OF "w-index"])
(auto simp: 1 "w-rel:3")
}
qed
AOT_thus ‹□∀x⇩1...∀x⇩n ([[G]⇩w]x⇩1...x⇩n → □[[G]⇩w]x⇩1...x⇩n)›
using "→E" by blast
qed
AOT_theorem "rigid-der:3": ‹∃F Rigidifies(F, G)›
proof -
AOT_obtain w where w: ‹∀p (w ⊨ p ≡ p)›
using "act-world:1" "PossibleWorld.∃E"[rotated] by meson
show ?thesis
proof (rule "∃I"(1)[where τ=‹«[G]⇩w»›])
AOT_show ‹Rigidifies([G]⇩w, [G])›
proof(safe intro!: "≡⇩d⇩fI"[OF "df-rigid-rel:2"] "&I" GEN)
AOT_show ‹Rigid([G]⇩w)›
using "rigid-der:2" by blast
next
fix x⇩1x⇩n
AOT_have ‹[[G]⇩w]x⇩1...x⇩n ≡ [λx⇩1...x⇩n w ⊨ [G]x⇩1...x⇩n]x⇩1...x⇩n›
proof(rule "≡I"; rule "→I")
AOT_assume ‹[[G]⇩w]x⇩1...x⇩n›
AOT_thus ‹[λx⇩1...x⇩n w ⊨ [G]x⇩1...x⇩n]x⇩1...x⇩n›
by (rule "rule-id-df:2:a[2]"
[where τ="λ (Π, κ). «[Π]⇩κ»" and
σ="λ(Π, κ). «[λx⇩1...x⇩n κ ⊨ [Π]x⇩1...x⇩n]»",
simplified, OF "w-index", OF "w-rel:3"])
next
AOT_assume ‹[λx⇩1...x⇩n w ⊨ [G]x⇩1...x⇩n]x⇩1...x⇩n›
AOT_thus ‹[[G]⇩w]x⇩1...x⇩n›
by (rule "rule-id-df:2:b[2]"
[where τ="λ (Π, κ). «[Π]⇩κ»" and
σ="λ(Π, κ). «[λx⇩1...x⇩n κ ⊨ [Π]x⇩1...x⇩n]»",
simplified, OF "w-index", OF "w-rel:3"])
qed
also AOT_have ‹… ≡ w ⊨ [G]x⇩1...x⇩n›
by (rule "beta-C-meta"[THEN "→E"])
(fact "w-rel:3")
also AOT_have ‹… ≡ [G]x⇩1...x⇩n›
using w[THEN "∀E"(1), OF "log-prop-prop:2"] by blast
finally AOT_show ‹[[G]⇩w]x⇩1...x⇩n ≡ [G]x⇩1...x⇩n›.
qed
next
AOT_show ‹[G]⇩w↓›
by (rule "rule-id-df:2:b[2]"[where τ="λ (Π, κ). «[Π]⇩κ»"
and σ="λ(Π, κ). «[λx⇩1...x⇩n κ ⊨ [Π]x⇩1...x⇩n]»",
simplified, OF "w-index"])
(auto simp: "w-rel:3")
qed
qed
AOT_theorem "rigid-rel-thms:1":
‹□(∀x⇩1...∀x⇩n ([F]x⇩1...x⇩n → □[F]x⇩1...x⇩n)) ≡ ∀x⇩1...∀x⇩n(◇[F]x⇩1...x⇩n → □[F]x⇩1...x⇩n)›
proof(safe intro!: "≡I" "→I" GEN)
fix x⇩1x⇩n
AOT_assume ‹□∀x⇩1...∀x⇩n ([F]x⇩1...x⇩n → □[F]x⇩1...x⇩n)›
AOT_hence ‹∀x⇩1...∀x⇩n □([F]x⇩1...x⇩n → □[F]x⇩1...x⇩n)›
by (metis "→E" GEN RM "cqt-orig:3")
AOT_hence ‹□([F]x⇩1...x⇩n → □[F]x⇩1...x⇩n)›
using "∀E"(2) by blast
AOT_hence ‹◇[F]x⇩1...x⇩n → □[F]x⇩1...x⇩n›
by (metis "≡E"(1) "sc-eq-box-box:1")
moreover AOT_assume ‹◇[F]x⇩1...x⇩n›
ultimately AOT_show ‹□[F]x⇩1...x⇩n›
using "→E" by blast
next
AOT_assume ‹∀x⇩1...∀x⇩n (◇[F]x⇩1...x⇩n → □[F]x⇩1...x⇩n)›
AOT_hence ‹◇[F]x⇩1...x⇩n → □[F]x⇩1...x⇩n› for x⇩1x⇩n
using "∀E"(2) by blast
AOT_hence ‹□([F]x⇩1...x⇩n → □[F]x⇩1...x⇩n)› for x⇩1x⇩n
by (metis "≡E"(2) "sc-eq-box-box:1")
AOT_hence 0: ‹∀x⇩1...∀x⇩n □([F]x⇩1...x⇩n → □[F]x⇩1...x⇩n)›
by (rule GEN)
AOT_thus ‹□(∀x⇩1...∀x⇩n ([F]x⇩1...x⇩n → □[F]x⇩1...x⇩n))›
using "BF" "vdash-properties:10" by blast
qed
AOT_theorem "rigid-rel-thms:2":
‹□(∀x⇩1...∀x⇩n ([F]x⇩1...x⇩n → □[F]x⇩1...x⇩n)) ≡ ∀x⇩1...∀x⇩n(□[F]x⇩1...x⇩n ∨ □¬[F]x⇩1...x⇩n)›
proof(safe intro!: "≡I" "→I")
AOT_assume ‹□(∀x⇩1...∀x⇩n ([F]x⇩1...x⇩n → □[F]x⇩1...x⇩n))›
AOT_hence 0: ‹∀x⇩1...∀x⇩n □([F]x⇩1...x⇩n → □[F]x⇩1...x⇩n)›
using CBF[THEN "→E"] by blast
AOT_show ‹∀x⇩1...∀x⇩n(□[F]x⇩1...x⇩n ∨ □¬[F]x⇩1...x⇩n)›
proof(rule GEN)
fix x⇩1x⇩n
AOT_have 1: ‹□([F]x⇩1...x⇩n → □[F]x⇩1...x⇩n)›
using 0[THEN "∀E"(2)].
AOT_hence 2: ‹◇[F]x⇩1...x⇩n → [F]x⇩1...x⇩n›
using "B◇" "Hypothetical Syllogism" "K◇" "vdash-properties:10" by blast
AOT_have ‹[F]x⇩1...x⇩n ∨ ¬[F]x⇩1...x⇩n›
using "exc-mid".
moreover {
AOT_assume ‹[F]x⇩1...x⇩n›
AOT_hence ‹□[F]x⇩1...x⇩n›
using 1[THEN "qml:2"[axiom_inst, THEN "→E"], THEN "→E"] by blast
}
moreover {
AOT_assume 3: ‹¬[F]x⇩1...x⇩n›
AOT_have ‹□¬[F]x⇩1...x⇩n›
proof(rule "raa-cor:1")
AOT_assume ‹¬□¬[F]x⇩1...x⇩n›
AOT_hence ‹◇[F]x⇩1...x⇩n›
by (AOT_subst_def "conventions:5")
AOT_hence ‹[F]x⇩1...x⇩n› using 2[THEN "→E"] by blast
AOT_thus ‹[F]x⇩1...x⇩n & ¬[F]x⇩1...x⇩n›
using 3 "&I" by blast
qed
}
ultimately AOT_show ‹□[F]x⇩1...x⇩n ∨ □¬[F]x⇩1...x⇩n›
by (metis "∨I"(1,2) "raa-cor:1")
qed
next
AOT_assume 0: ‹∀x⇩1...∀x⇩n(□[F]x⇩1...x⇩n ∨ □¬[F]x⇩1...x⇩n)›
{
fix x⇩1x⇩n
AOT_have ‹□[F]x⇩1...x⇩n ∨ □¬[F]x⇩1...x⇩n› using 0[THEN "∀E"(2)] by blast
moreover {
AOT_assume ‹□[F]x⇩1...x⇩n›
AOT_hence ‹□□[F]x⇩1...x⇩n›
using "S5Basic:6"[THEN "≡E"(1)] by blast
AOT_hence ‹□([F]x⇩1...x⇩n → □[F]x⇩1...x⇩n)›
using "KBasic:1"[THEN "→E"] by blast
}
moreover {
AOT_assume ‹□¬[F]x⇩1...x⇩n›
AOT_hence ‹□([F]x⇩1...x⇩n → □[F]x⇩1...x⇩n)›
using "KBasic:2"[THEN "→E"] by blast
}
ultimately AOT_have ‹□([F]x⇩1...x⇩n → □[F]x⇩1...x⇩n)›
using "con-dis-i-e:4:b" "raa-cor:1" by blast
}
AOT_hence ‹∀x⇩1...∀x⇩n □([F]x⇩1...x⇩n → □[F]x⇩1...x⇩n)›
by (rule GEN)
AOT_thus ‹□(∀x⇩1...∀x⇩n ([F]x⇩1...x⇩n → □[F]x⇩1...x⇩n))›
using BF[THEN "→E"] by fast
qed
AOT_theorem "rigid-rel-thms:3": ‹Rigid(F) ≡ ∀x⇩1...∀x⇩n (□[F]x⇩1...x⇩n ∨ □¬[F]x⇩1...x⇩n)›
by (AOT_subst_thm "df-rigid-rel:1"[THEN "≡Df", THEN "≡S"(1), OF "cqt:2"(1)];
AOT_subst_thm "rigid-rel-thms:2")
(simp add: "oth-class-taut:3:a")
end