Theory AOT_PossibleWorlds
1
2theory AOT_PossibleWorlds
3 imports AOT_PLM AOT_BasicLogicalObjects AOT_RestrictedVariables
4begin
5
6
7section‹Possible Worlds›
8
9AOT_define Situation :: ‹τ ⇒ φ› (‹Situation'(_')›)
10 situations: ‹Situation(x) ≡⇩d⇩f A!x & ∀F (x[F] → Propositional([F]))›
11
12AOT_theorem "T-sit": ‹TruthValue(x) → Situation(x)›
13proof(rule "→I")
14 AOT_assume ‹TruthValue(x)›
15 AOT_hence ‹∃p TruthValueOf(x,p)›
16 using "T-value"[THEN "≡⇩d⇩fE"] by blast
17 then AOT_obtain p where ‹TruthValueOf(x,p)› using "∃E"[rotated] by blast
18 AOT_hence θ: ‹A!x & ∀F (x[F] ≡ ∃q((q ≡ p) & F = [λy q]))›
19 using "tv-p"[THEN "≡⇩d⇩fE"] by blast
20 AOT_show ‹Situation(x)›
21 proof(rule situations[THEN "≡⇩d⇩fI"]; safe intro!: "&I" GEN "→I" θ[THEN "&E"(1)])
22 fix F
23 AOT_assume ‹x[F]›
24 AOT_hence ‹∃q((q ≡ p) & F = [λy q])›
25 using θ[THEN "&E"(2), THEN "∀E"(2)[where β=F], THEN "≡E"(1)] by argo
26 then AOT_obtain q where ‹(q ≡ p) & F = [λy q]› using "∃E"[rotated] by blast
27 AOT_hence ‹∃p F = [λy p]› using "&E"(2) "∃I"(2) by metis
28 AOT_thus ‹Propositional([F])›
29 by (metis "≡⇩d⇩fI" "prop-prop1")
30 qed
31qed
32
33AOT_theorem "possit-sit:1": ‹Situation(x) ≡ □Situation(x)›
34proof(rule "≡I"; rule "→I")
35 AOT_assume ‹Situation(x)›
36 AOT_hence 0: ‹A!x & ∀F (x[F] → Propositional([F]))›
37 using situations[THEN "≡⇩d⇩fE"] by blast
38 AOT_have 1: ‹□(A!x & ∀F (x[F] → Propositional([F])))›
39 proof(rule "KBasic:3"[THEN "≡E"(2)]; rule "&I")
40 AOT_show ‹□A!x› using 0[THEN "&E"(1)] by (metis "oa-facts:2"[THEN "→E"])
41 next
42 AOT_have ‹∀F (x[F] → Propositional([F])) → □∀F (x[F] → Propositional([F]))›
43 by (AOT_subst ‹Propositional([F])› ‹∃p (F = [λy p])› for: F :: ‹<κ>›)
44 (auto simp: "prop-prop1" "≡Df" "enc-prop-nec:2")
45 AOT_thus ‹□∀F (x[F] → Propositional([F]))›
46 using 0[THEN "&E"(2)] "→E" by blast
47 qed
48 AOT_show ‹□Situation(x)›
49 by (AOT_subst ‹Situation(x)› ‹A!x & ∀F (x[F] → Propositional([F]))›)
50 (auto simp: 1 "≡Df" situations)
51next
52 AOT_show ‹Situation(x)› if ‹□Situation(x)›
53 using "qml:2"[axiom_inst, THEN "→E", OF that].
54qed
55
56AOT_theorem "possit-sit:2": ‹◇Situation(x) ≡ Situation(x)›
57 using "possit-sit:1"
58 by (metis "RE◇" "S5Basic:2" "≡E"(1) "≡E"(5) "Commutativity of ≡")
59
60AOT_theorem "possit-sit:3": ‹◇Situation(x) ≡ □Situation(x)›
61 using "possit-sit:1" "possit-sit:2" by (meson "≡E"(5))
62
63AOT_theorem "possit-sit:4": ‹❙𝒜Situation(x) ≡ Situation(x)›
64 by (meson "Act-Basic:5" "Act-Sub:2" "RA[2]" "≡E"(1) "≡E"(6) "possit-sit:2")
65
66AOT_theorem "possit-sit:5": ‹Situation(∘p)›
67proof (safe intro!: situations[THEN "≡⇩d⇩fI"] "&I" GEN "→I" "prop-prop1"[THEN "≡⇩d⇩fI"])
68 AOT_have ‹∃F ∘p[F]›
69 using "tv-id:2"[THEN "prop-enc"[THEN "≡⇩d⇩fE"], THEN "&E"(2)]
70 "existential:1" "prop-prop2:2" by blast
71 AOT_thus ‹A!∘p›
72 by (safe intro!: "encoders-are-abstract"[unvarify x, THEN "→E"]
73 "t=t-proper:2"[THEN "→E", OF "ext-p-tv:3"])
74next
75 fix F
76 AOT_assume ‹∘p[F]›
77 AOT_hence ‹❙ιx(A!x & ∀F (x[F] ≡ ∃q ((q ≡ p) & F = [λy q])))[F]›
78 using "tv-id:1" "rule=E" by fast
79 AOT_hence ‹❙𝒜∃q ((q ≡ p) & F = [λy q])›
80 using "≡E"(1) "desc-nec-encode:1" by fast
81 AOT_hence ‹∃q ❙𝒜((q ≡ p) & F = [λy q])›
82 by (metis "Act-Basic:10" "≡E"(1))
83 then AOT_obtain q where ‹❙𝒜((q ≡ p) & F = [λy q])› using "∃E"[rotated] by blast
84 AOT_hence ‹❙𝒜F = [λy q]› by (metis "Act-Basic:2" "con-dis-i-e:2:b" "intro-elim:3:a")
85 AOT_hence ‹F = [λy q]›
86 using "id-act:1"[unvarify β, THEN "≡E"(2)] by (metis "prop-prop2:2")
87 AOT_thus ‹∃p F = [λy p]›
88 using "∃I" by fast
89qed
90
91AOT_theorem "possit-sit:6": ‹Situation(⊤)›
92proof -
93 AOT_have true_def: ‹❙⊢⇩□ ⊤ = ❙ιx (A!x & ∀F (x[F] ≡ ∃p(p & F = [λy p])))›
94 by (simp add: "A-descriptions" "rule-id-df:1[zero]" "the-true:1")
95 AOT_hence true_den: ‹❙⊢⇩□ ⊤↓›
96 using "t=t-proper:1" "vdash-properties:6" by blast
97 AOT_have ‹❙𝒜TruthValue(⊤)›
98 using "actual-desc:2"[unvarify x, OF true_den, THEN "→E", OF true_def]
99 using "TV-lem2:1"[unvarify x, OF true_den, THEN "RA[2]",
100 THEN "act-cond"[THEN "→E"], THEN "→E"]
101 by blast
102 AOT_hence ‹❙𝒜Situation(⊤)›
103 using "T-sit"[unvarify x, OF true_den, THEN "RA[2]",
104 THEN "act-cond"[THEN "→E"], THEN "→E"] by blast
105 AOT_thus ‹Situation(⊤)›
106 using "possit-sit:4"[unvarify x, OF true_den, THEN "≡E"(1)] by blast
107qed
108
109AOT_theorem "possit-sit:7": ‹Situation(⊥)›
110proof -
111 AOT_have true_def: ‹❙⊢⇩□ ⊥ = ❙ιx (A!x & ∀F (x[F] ≡ ∃p(¬p & F = [λy p])))›
112 by (simp add: "A-descriptions" "rule-id-df:1[zero]" "the-true:2")
113 AOT_hence true_den: ‹❙⊢⇩□ ⊥↓›
114 using "t=t-proper:1" "vdash-properties:6" by blast
115 AOT_have ‹❙𝒜TruthValue(⊥)›
116 using "actual-desc:2"[unvarify x, OF true_den, THEN "→E", OF true_def]
117 using "TV-lem2:2"[unvarify x, OF true_den, THEN "RA[2]",
118 THEN "act-cond"[THEN "→E"], THEN "→E"]
119 by blast
120 AOT_hence ‹❙𝒜Situation(⊥)›
121 using "T-sit"[unvarify x, OF true_den, THEN "RA[2]",
122 THEN "act-cond"[THEN "→E"], THEN "→E"] by blast
123 AOT_thus ‹Situation(⊥)›
124 using "possit-sit:4"[unvarify x, OF true_den, THEN "≡E"(1)] by blast
125qed
126
127AOT_register_rigid_restricted_type
128 Situation: ‹Situation(κ)›
129proof
130 AOT_modally_strict {
131 fix p
132 AOT_obtain x where ‹TruthValueOf(x,p)›
133 by (metis "instantiation" "p-has-!tv:1")
134 AOT_hence ‹∃p TruthValueOf(x,p)› by (rule "∃I")
135 AOT_hence ‹TruthValue(x)› by (metis "≡⇩d⇩fI" "T-value")
136 AOT_hence ‹Situation(x)› using "T-sit"[THEN "→E"] by blast
137 AOT_thus ‹∃x Situation(x)› by (rule "∃I")
138 }
139next
140 AOT_modally_strict {
141 AOT_show ‹Situation(κ) → κ↓› for κ
142 proof (rule "→I")
143 AOT_assume ‹Situation(κ)›
144 AOT_hence ‹A!κ› by (metis "≡⇩d⇩fE" "&E"(1) situations)
145 AOT_thus ‹κ↓› by (metis "russell-axiom[exe,1].ψ_denotes_asm")
146 qed
147 }
148next
149 AOT_modally_strict {
150 AOT_show ‹∀α(Situation(α) → □Situation(α))›
151 using "possit-sit:1"[THEN "conventions:3"[THEN "≡⇩d⇩fE"],
152 THEN "&E"(1)] GEN by fast
153 }
154qed
155
156AOT_register_variable_names
157 Situation: s
158
159AOT_define TruthInSituation :: ‹τ ⇒ φ ⇒ φ› ("(_ ⊨/ _)" [100, 40] 100)
160 "true-in-s": ‹s ⊨ p ≡⇩d⇩f s❙Σp›
161
162notepad
163begin
164
165 fix x p q
166 have ‹«x ⊨ p → q» = «(x ⊨ p) → q»›
167 by simp
168 have ‹«x ⊨ p & q» = «(x ⊨ p) & q»›
169 by simp
170 have ‹«x ⊨ ¬p» = «x ⊨ (¬p)»›
171 by simp
172 have ‹«x ⊨ □p» = «x ⊨ (□p)»›
173 by simp
174 have ‹«x ⊨ ❙𝒜p» = «x ⊨ (❙𝒜p)»›
175 by simp
176 have ‹«□x ⊨ p» = «□(x ⊨ p)»›
177 by simp
178 have ‹«¬x ⊨ p» = «¬(x ⊨ p)»›
179 by simp
180end
181
182
183AOT_theorem lem1: ‹Situation(x) → (x ⊨ p ≡ x[λy p])›
184proof (rule "→I"; rule "≡I"; rule "→I")
185 AOT_assume ‹Situation(x)›
186 AOT_assume ‹x ⊨ p›
187 AOT_hence ‹x❙Σp›
188 using "true-in-s"[THEN "≡⇩d⇩fE"] "&E" by blast
189 AOT_thus ‹x[λy p]› using "prop-enc"[THEN "≡⇩d⇩fE"] "&E" by blast
190next
191 AOT_assume 1: ‹Situation(x)›
192 AOT_assume ‹x[λy p]›
193 AOT_hence ‹x❙Σp›
194 using "prop-enc"[THEN "≡⇩d⇩fI", OF "&I", OF "cqt:2"(1)] by blast
195 AOT_thus ‹x ⊨ p›
196 using "true-in-s"[THEN "≡⇩d⇩fI"] 1 "&I" by blast
197qed
198
199AOT_theorem "lem2:1": ‹s ⊨ p ≡ □s ⊨ p›
200proof -
201 AOT_have sit: ‹Situation(s)›
202 by (simp add: Situation.ψ)
203 AOT_have ‹s ⊨ p ≡ s[λy p]›
204 using lem1[THEN "→E", OF sit] by blast
205 also AOT_have ‹… ≡ □s[λy p]›
206 by (rule "en-eq:2[1]"[unvarify F]) "cqt:2[lambda]"
207 also AOT_have ‹… ≡ □s ⊨ p›
208 using lem1[THEN RM, THEN "→E", OF "possit-sit:1"[THEN "≡E"(1), OF sit]]
209 by (metis "KBasic:6" "≡E"(2) "Commutativity of ≡" "→E")
210 finally show ?thesis.
211qed
212
213AOT_theorem "lem2:2": ‹◇s ⊨ p ≡ s ⊨ p›
214proof -
215 AOT_have ‹□(s ⊨ p → □s ⊨ p)›
216 using "possit-sit:1"[THEN "≡E"(1), OF Situation.ψ]
217 "lem2:1"[THEN "conventions:3"[THEN "≡⇩d⇩fE", THEN "&E"(1)]]
218 RM[OF "→I", THEN "→E"] by blast
219 thus ?thesis by (metis "B◇" "S5Basic:13" "T◇" "≡I" "≡E"(1) "→E")
220qed
221
222AOT_theorem "lem2:3": ‹◇s ⊨ p ≡ □s ⊨ p›
223 using "lem2:1" "lem2:2" by (metis "≡E"(5))
224
225AOT_theorem "lem2:4": ‹❙𝒜(s ⊨ p) ≡ s ⊨ p›
226proof -
227 AOT_have ‹□(s ⊨ p → □s ⊨ p)›
228 using "possit-sit:1"[THEN "≡E"(1), OF Situation.ψ]
229 "lem2:1"[THEN "conventions:3"[THEN "≡⇩d⇩fE", THEN "&E"(1)]]
230 RM[OF "→I", THEN "→E"] by blast
231 thus ?thesis
232 using "sc-eq-fur:2"[THEN "→E"] by blast
233qed
234
235AOT_theorem "lem2:5": ‹¬s ⊨ p ≡ □¬s ⊨ p›
236 by (metis "KBasic2:1" "contraposition:1[2]" "→I" "≡I" "≡E"(3) "≡E"(4) "lem2:2")
237
238AOT_theorem "sit-identity": ‹s = s' ≡ ∀p(s ⊨ p ≡ s' ⊨ p)›
239proof(rule "≡I"; rule "→I")
240 AOT_assume ‹s = s'›
241 moreover AOT_have ‹∀p(s ⊨ p ≡ s ⊨ p)›
242 by (simp add: "oth-class-taut:3:a" "universal-cor")
243 ultimately AOT_show ‹∀p(s ⊨ p ≡ s' ⊨ p)›
244 using "rule=E" by fast
245next
246 AOT_assume a: ‹∀p (s ⊨ p ≡ s' ⊨ p)›
247 AOT_show ‹s = s'›
248 proof(safe intro!: "ab-obey:1"[THEN "→E", THEN "→E"] "&I" GEN "≡I" "→I")
249 AOT_show ‹A!s› using Situation.ψ "≡⇩d⇩fE" "&E"(1) situations by blast
250 next
251 AOT_show ‹A!s'› using Situation.ψ "≡⇩d⇩fE" "&E"(1) situations by blast
252 next
253 fix F
254 AOT_assume 0: ‹s[F]›
255 AOT_hence ‹∃p (F = [λy p])›
256 using Situation.ψ[THEN situations[THEN "≡⇩d⇩fE"], THEN "&E"(2),
257 THEN "∀E"(2)[where β=F], THEN "→E"]
258 "prop-prop1"[THEN "≡⇩d⇩fE"] by blast
259 then AOT_obtain p where F_def: ‹F = [λy p]›
260 using "∃E" by metis
261 AOT_hence ‹s[λy p]›
262 using 0 "rule=E" by blast
263 AOT_hence ‹s ⊨ p›
264 using lem1[THEN "→E", OF Situation.ψ, THEN "≡E"(2)] by blast
265 AOT_hence ‹s' ⊨ p›
266 using a[THEN "∀E"(2)[where β=p], THEN "≡E"(1)] by blast
267 AOT_hence ‹s'[λy p]›
268 using lem1[THEN "→E", OF Situation.ψ, THEN "≡E"(1)] by blast
269 AOT_thus ‹s'[F]›
270 using F_def[symmetric] "rule=E" by blast
271 next
272 fix F
273 AOT_assume 0: ‹s'[F]›
274 AOT_hence ‹∃p (F = [λy p])›
275 using Situation.ψ[THEN situations[THEN "≡⇩d⇩fE"], THEN "&E"(2),
276 THEN "∀E"(2)[where β=F], THEN "→E"]
277 "prop-prop1"[THEN "≡⇩d⇩fE"] by blast
278 then AOT_obtain p where F_def: ‹F = [λy p]›
279 using "∃E" by metis
280 AOT_hence ‹s'[λy p]›
281 using 0 "rule=E" by blast
282 AOT_hence ‹s' ⊨ p›
283 using lem1[THEN "→E", OF Situation.ψ, THEN "≡E"(2)] by blast
284 AOT_hence ‹s ⊨ p›
285 using a[THEN "∀E"(2)[where β=p], THEN "≡E"(2)] by blast
286 AOT_hence ‹s[λy p]›
287 using lem1[THEN "→E", OF Situation.ψ, THEN "≡E"(1)] by blast
288 AOT_thus ‹s[F]›
289 using F_def[symmetric] "rule=E" by blast
290 qed
291qed
292
293AOT_define PartOfSituation :: ‹τ ⇒ τ ⇒ φ› (infixl ‹⊴› 80)
294 "sit-part-whole": ‹s ⊴ s' ≡⇩d⇩f ∀p (s ⊨ p → s' ⊨ p)›
295
296AOT_theorem "part:1": ‹s ⊴ s›
297 by (rule "sit-part-whole"[THEN "≡⇩d⇩fI"])
298 (safe intro!: "&I" Situation.ψ GEN "→I")
299
300AOT_theorem "part:2": ‹s ⊴ s' & s ≠ s' → ¬(s' ⊴ s)›
301proof(rule "→I"; frule "&E"(1); drule "&E"(2); rule "raa-cor:2")
302 AOT_assume 0: ‹s ⊴ s'›
303 AOT_hence a: ‹s ⊨ p → s' ⊨ p› for p
304 using "∀E"(2) "sit-part-whole"[THEN "≡⇩d⇩fE"] "&E" by blast
305 AOT_assume ‹s' ⊴ s›
306 AOT_hence b: ‹s' ⊨ p → s ⊨ p› for p
307 using "∀E"(2) "sit-part-whole"[THEN "≡⇩d⇩fE"] "&E" by blast
308 AOT_have ‹∀p (s ⊨ p ≡ s' ⊨ p)›
309 using a b by (simp add: "≡I" "universal-cor")
310 AOT_hence 1: ‹s = s'›
311 using "sit-identity"[THEN "≡E"(2)] by metis
312 AOT_assume ‹s ≠ s'›
313 AOT_hence ‹¬(s = s')›
314 by (metis "≡⇩d⇩fE" "=-infix")
315 AOT_thus ‹s = s' & ¬(s = s')›
316 using 1 "&I" by blast
317qed
318
319AOT_theorem "part:3": ‹s ⊴ s' & s' ⊴ s'' → s ⊴ s''›
320proof(rule "→I"; frule "&E"(1); drule "&E"(2);
321 safe intro!: "&I" GEN "→I" "sit-part-whole"[THEN "≡⇩d⇩fI"] Situation.ψ)
322 fix p
323 AOT_assume ‹s ⊨ p›
324 moreover AOT_assume ‹s ⊴ s'›
325 ultimately AOT_have ‹s' ⊨ p›
326 using "sit-part-whole"[THEN "≡⇩d⇩fE", THEN "&E"(2),
327 THEN "∀E"(2)[where β=p], THEN "→E"] by blast
328 moreover AOT_assume ‹s' ⊴ s''›
329 ultimately AOT_show ‹s'' ⊨ p›
330 using "sit-part-whole"[THEN "≡⇩d⇩fE", THEN "&E"(2),
331 THEN "∀E"(2)[where β=p], THEN "→E"] by blast
332qed
333
334AOT_theorem "sit-identity2:1": ‹s = s' ≡ s ⊴ s' & s' ⊴ s›
335proof (safe intro!: "≡I" "&I" "→I")
336 AOT_show ‹s ⊴ s'› if ‹s = s'›
337 using "rule=E" "part:1" that by blast
338next
339 AOT_show ‹s' ⊴ s› if ‹s = s'›
340 using "rule=E" "part:1" that[symmetric] by blast
341next
342 AOT_assume ‹s ⊴ s' & s' ⊴ s›
343 AOT_thus ‹s = s'› using "part:2"[THEN "→E", OF "&I"]
344 by (metis "≡⇩d⇩fI" "&E"(1) "&E"(2) "=-infix" "raa-cor:3")
345qed
346
347AOT_theorem "sit-identity2:2": ‹s = s' ≡ ∀s'' (s'' ⊴ s ≡ s'' ⊴ s')›
348proof(safe intro!: "≡I" "→I" Situation.GEN "sit-identity"[THEN "≡E"(2)]
349 GEN[where 'a=𝗈])
350 AOT_show ‹s'' ⊴ s'› if ‹s'' ⊴ s› and ‹s = s'› for s''
351 using "rule=E" that by blast
352next
353 AOT_show ‹s'' ⊴ s› if ‹s'' ⊴ s'› and ‹s = s'› for s''
354 using "rule=E" id_sym that by blast
355next
356 AOT_show ‹s' ⊨ p› if ‹s ⊨ p› and ‹∀s'' (s'' ⊴ s ≡ s'' ⊴ s')› for p
357 using "sit-part-whole"[THEN "≡⇩d⇩fE", THEN "&E"(2),
358 OF that(2)[THEN "Situation.∀E", THEN "≡E"(1), OF "part:1"],
359 THEN "∀E"(2), THEN "→E", OF that(1)].
360next
361 AOT_show ‹s ⊨ p› if ‹s' ⊨ p› and ‹∀s'' (s'' ⊴ s ≡ s'' ⊴ s')› for p
362 using "sit-part-whole"[THEN "≡⇩d⇩fE", THEN "&E"(2),
363 OF that(2)[THEN "Situation.∀E", THEN "≡E"(2), OF "part:1"],
364 THEN "∀E"(2), THEN "→E", OF that(1)].
365qed
366
367AOT_define Persistent :: ‹φ ⇒ φ› (‹Persistent'(_')›)
368 persistent: ‹Persistent(p) ≡⇩d⇩f ∀s (s ⊨ p → ∀s' (s ⊴ s' → s' ⊨ p))›
369
370AOT_theorem "pers-prop": ‹∀p Persistent(p)›
371 by (safe intro!: GEN[where 'a=𝗈] Situation.GEN persistent[THEN "≡⇩d⇩fI"] "→I")
372 (simp add: "sit-part-whole"[THEN "≡⇩d⇩fE", THEN "&E"(2), THEN "∀E"(2), THEN "→E"])
373
374AOT_define NullSituation :: ‹τ ⇒ φ› (‹NullSituation'(_')›)
375 "df-null-trivial:1": ‹NullSituation(s) ≡⇩d⇩f ¬∃p s ⊨ p›
376
377AOT_define TrivialSituation :: ‹τ ⇒ φ› (‹TrivialSituation'(_')›)
378 "df-null-trivial:2": ‹TrivialSituation(s) ≡⇩d⇩f ∀p s ⊨ p›
379
380AOT_theorem "thm-null-trivial:1": ‹∃!x NullSituation(x)›
381proof (AOT_subst ‹NullSituation(x)› ‹A!x & ∀F (x[F] ≡ F ≠ F)› for: x)
382 AOT_modally_strict {
383 AOT_show ‹NullSituation(x) ≡ A!x & ∀F (x[F] ≡ F ≠ F)› for x
384 proof (safe intro!: "≡I" "→I" "df-null-trivial:1"[THEN "≡⇩d⇩fI"]
385 dest!: "df-null-trivial:1"[THEN "≡⇩d⇩fE"])
386 AOT_assume 0: ‹Situation(x) & ¬∃p x ⊨ p›
387 AOT_have 1: ‹A!x›
388 using 0[THEN "&E"(1), THEN situations[THEN "≡⇩d⇩fE"], THEN "&E"(1)].
389 AOT_have 2: ‹x[F] → ∃p F = [λy p]› for F
390 using 0[THEN "&E"(1), THEN situations[THEN "≡⇩d⇩fE"],
391 THEN "&E"(2), THEN "∀E"(2)]
392 by (metis "≡⇩d⇩fE" "→I" "prop-prop1" "→E")
393 AOT_show ‹A!x & ∀F (x[F] ≡ F ≠ F)›
394 proof (safe intro!: "&I" 1 GEN "≡I" "→I")
395 fix F
396 AOT_assume ‹x[F]›
397 moreover AOT_obtain p where ‹F = [λy p]›
398 using calculation 2[THEN "→E"] "∃E"[rotated] by blast
399 ultimately AOT_have ‹x[λy p]›
400 by (metis "rule=E")
401 AOT_hence ‹x ⊨ p›
402 using lem1[THEN "→E", OF 0[THEN "&E"(1)], THEN "≡E"(2)] by blast
403 AOT_hence ‹∃p (x ⊨ p)›
404 by (rule "∃I")
405 AOT_thus ‹F ≠ F›
406 using 0[THEN "&E"(2)] "raa-cor:1" "&I" by blast
407 next
408 fix F :: ‹<κ> AOT_var›
409 AOT_assume ‹F ≠ F›
410 AOT_hence ‹¬(F = F)› by (metis "≡⇩d⇩fE" "=-infix")
411 moreover AOT_have ‹F = F›
412 by (simp add: "id-eq:1")
413 ultimately AOT_show ‹x[F]› using "&I" "raa-cor:1" by blast
414 qed
415 next
416 AOT_assume 0: ‹A!x & ∀F (x[F] ≡ F ≠ F)›
417 AOT_hence ‹x[F] ≡ F ≠ F› for F
418 using "∀E" "&E" by blast
419 AOT_hence 1: ‹¬x[F]› for F
420 using "≡⇩d⇩fE" "id-eq:1" "=-infix" "reductio-aa:1" "≡E"(1) by blast
421 AOT_show ‹Situation(x) & ¬∃p x ⊨ p›
422 proof (safe intro!: "&I" situations[THEN "≡⇩d⇩fI"] 0[THEN "&E"(1)] GEN "→I")
423 AOT_show ‹Propositional([F])› if ‹x[F]› for F
424 using that 1 "&I" "raa-cor:1" by fast
425 next
426 AOT_show ‹¬∃p x ⊨ p›
427 proof(rule "raa-cor:2")
428 AOT_assume ‹∃p x ⊨ p›
429 then AOT_obtain p where ‹x ⊨ p› using "∃E"[rotated] by blast
430 AOT_hence ‹x[λy p]›
431 using "≡⇩d⇩fE" "&E"(1) "≡E"(1) lem1 "modus-tollens:1"
432 "raa-cor:3" "true-in-s" by fast
433 moreover AOT_have ‹¬x[λy p]›
434 by (rule 1[unvarify F]) "cqt:2[lambda]"
435 ultimately AOT_show ‹p & ¬p› for p using "&I" "raa-cor:1" by blast
436 qed
437 qed
438 qed
439 }
440next
441 AOT_show ‹∃!x ([A!]x & ∀F (x[F] ≡ F ≠ F))›
442 by (simp add: "A-objects!")
443qed
444
445
446AOT_theorem "thm-null-trivial:2": ‹∃!x TrivialSituation(x)›
447proof (AOT_subst ‹TrivialSituation(x)› ‹A!x & ∀F (x[F] ≡ ∃p F = [λy p])› for: x)
448 AOT_modally_strict {
449 AOT_show ‹TrivialSituation(x) ≡ A!x & ∀F (x[F] ≡ ∃p F = [λy p])› for x
450 proof (safe intro!: "≡I" "→I" "df-null-trivial:2"[THEN "≡⇩d⇩fI"]
451 dest!: "df-null-trivial:2"[THEN "≡⇩d⇩fE"])
452 AOT_assume 0: ‹Situation(x) & ∀p x ⊨ p›
453 AOT_have 1: ‹A!x›
454 using 0[THEN "&E"(1), THEN situations[THEN "≡⇩d⇩fE"], THEN "&E"(1)].
455 AOT_have 2: ‹x[F] → ∃p F = [λy p]› for F
456 using 0[THEN "&E"(1), THEN situations[THEN "≡⇩d⇩fE"],
457 THEN "&E"(2), THEN "∀E"(2)]
458 by (metis "≡⇩d⇩fE" "deduction-theorem" "prop-prop1" "→E")
459 AOT_show ‹A!x & ∀F (x[F] ≡ ∃p F = [λy p])›
460 proof (safe intro!: "&I" 1 GEN "≡I" "→I" 2)
461 fix F
462 AOT_assume ‹∃p F = [λy p]›
463 then AOT_obtain p where ‹F = [λy p]›
464 using "∃E"[rotated] by blast
465 moreover AOT_have ‹x ⊨ p›
466 using 0[THEN "&E"(2)] "∀E" by blast
467 ultimately AOT_show ‹x[F]›
468 by (metis 0 "rule=E" "&E"(1) id_sym "≡E"(2) lem1
469 "Commutativity of ≡" "→E")
470 qed
471 next
472 AOT_assume 0: ‹A!x & ∀F (x[F] ≡ ∃p F = [λy p])›
473 AOT_hence 1: ‹x[F] ≡ ∃p F = [λy p]› for F
474 using "∀E" "&E" by blast
475 AOT_have 2: ‹Situation(x)›
476 proof (safe intro!: "&I" situations[THEN "≡⇩d⇩fI"] 0[THEN "&E"(1)] GEN "→I")
477 AOT_show ‹Propositional([F])› if ‹x[F]› for F
478 using 1[THEN "≡E"(1), OF that]
479 by (metis "≡⇩d⇩fI" "prop-prop1")
480 qed
481 AOT_show ‹Situation(x) & ∀p (x ⊨ p)›
482 proof (safe intro!: "&I" 2 0[THEN "&E"(1)] GEN "→I")
483 AOT_have ‹x[λy p] ≡ ∃q [λy p] = [λy q]› for p
484 by (rule 1[unvarify F, where τ="«[λy p]»"]) "cqt:2[lambda]"
485 moreover AOT_have ‹∃q [λy p] = [λy q]› for p
486 by (rule "∃I"(2)[where β=p])
487 (simp add: "rule=I:1" "prop-prop2:2")
488 ultimately AOT_have ‹x[λy p]› for p by (metis "≡E"(2))
489 AOT_thus ‹x ⊨ p› for p
490 by (metis "2" "≡E"(2) lem1 "→E")
491 qed
492 qed
493 }
494next
495 AOT_show ‹∃!x ([A!]x & ∀F (x[F] ≡ ∃p F = [λy p]))›
496 by (simp add: "A-objects!")
497qed
498
499AOT_theorem "thm-null-trivial:3": ‹❙ιx NullSituation(x)↓›
500 by (meson "A-Exists:2" "RA[2]" "≡E"(2) "thm-null-trivial:1")
501
502AOT_theorem "thm-null-trivial:4": ‹❙ιx TrivialSituation(x)↓›
503 using "A-Exists:2" "RA[2]" "≡E"(2) "thm-null-trivial:2" by blast
504
505AOT_define TheNullSituation :: ‹κ⇩s› (‹❙s⇩∅›)
506 "df-the-null-sit:1": ‹❙s⇩∅ =⇩d⇩f ❙ιx NullSituation(x)›
507
508AOT_define TheTrivialSituation :: ‹κ⇩s› (‹❙s⇩V›)
509 "df-the-null-sit:2": ‹❙s⇩V =⇩d⇩f ❙ιx TrivialSituation(x)›
510
511AOT_theorem "null-triv-sc:1": ‹NullSituation(x) → □NullSituation(x)›
512proof(safe intro!: "→I" dest!: "df-null-trivial:1"[THEN "≡⇩d⇩fE"];
513 frule "&E"(1); drule "&E"(2))
514 AOT_assume 1: ‹¬∃p (x ⊨ p)›
515 AOT_assume 0: ‹Situation(x)›
516 AOT_hence ‹□Situation(x)› by (metis "≡E"(1) "possit-sit:1")
517 moreover AOT_have ‹□¬∃p (x ⊨ p)›
518 proof(rule "raa-cor:1")
519 AOT_assume ‹¬□¬∃p (x ⊨ p)›
520 AOT_hence ‹◇∃p (x ⊨ p)›
521 by (metis "≡⇩d⇩fI" "conventions:5")
522 AOT_hence ‹∃p ◇(x ⊨ p)› by (metis "BF◇" "→E")
523 then AOT_obtain p where ‹◇(x ⊨ p)› using "∃E"[rotated] by blast
524 AOT_hence ‹x ⊨ p›
525 by (metis "≡E"(1) "lem2:2"[unconstrain s, THEN "→E", OF 0])
526 AOT_hence ‹∃p x ⊨ p› using "∃I" by fast
527 AOT_thus ‹∃p x ⊨ p & ¬∃p x ⊨ p› using 1 "&I" by blast
528 qed
529 ultimately AOT_have 2: ‹□(Situation(x) & ¬∃p x ⊨ p)›
530 by (metis "KBasic:3" "&I" "≡E"(2))
531 AOT_show ‹□NullSituation(x)›
532 by (AOT_subst ‹NullSituation(x)› ‹Situation(x) & ¬∃p x ⊨ p›)
533 (auto simp: "df-null-trivial:1" "≡Df" 2)
534qed
535
536
537AOT_theorem "null-triv-sc:2": ‹TrivialSituation(x) → □TrivialSituation(x)›
538proof(safe intro!: "→I" dest!: "df-null-trivial:2"[THEN "≡⇩d⇩fE"];
539 frule "&E"(1); drule "&E"(2))
540 AOT_assume 0: ‹Situation(x)›
541 AOT_hence 1: ‹□Situation(x)› by (metis "≡E"(1) "possit-sit:1")
542 AOT_assume ‹∀p x ⊨ p›
543 AOT_hence ‹x ⊨ p› for p
544 using "∀E" by blast
545 AOT_hence ‹□x ⊨ p› for p
546 using 0 "≡E"(1) "lem2:1"[unconstrain s, THEN "→E"] by blast
547 AOT_hence ‹∀p □x ⊨ p›
548 by (rule GEN)
549 AOT_hence ‹□∀p x ⊨ p›
550 by (rule BF[THEN "→E"])
551 AOT_hence 2: ‹□(Situation(x) & ∀p x ⊨ p)›
552 using 1 by (metis "KBasic:3" "&I" "≡E"(2))
553 AOT_show ‹□TrivialSituation(x)›
554 by (AOT_subst ‹TrivialSituation(x)› ‹Situation(x) & ∀p x ⊨ p›)
555 (auto simp: "df-null-trivial:2" "≡Df" 2)
556qed
557
558AOT_theorem "null-triv-sc:3": ‹NullSituation(❙s⇩∅)›
559 by (safe intro!: "df-the-null-sit:1"[THEN "=⇩d⇩fI"(2)] "thm-null-trivial:3"
560 "rule=I:1"[OF "thm-null-trivial:3"]
561 "!box-desc:2"[THEN "→E", THEN "→E", rotated, OF "thm-null-trivial:1",
562 OF "∀I", OF "null-triv-sc:1", THEN "∀E"(1), THEN "→E"])
563
564AOT_theorem "null-triv-sc:4": ‹TrivialSituation(❙s⇩V)›
565 by (safe intro!: "df-the-null-sit:2"[THEN "=⇩d⇩fI"(2)] "thm-null-trivial:4"
566 "rule=I:1"[OF "thm-null-trivial:4"]
567 "!box-desc:2"[THEN "→E", THEN "→E", rotated, OF "thm-null-trivial:2",
568 OF "∀I", OF "null-triv-sc:2", THEN "∀E"(1), THEN "→E"])
569
570AOT_theorem "null-triv-facts:1": ‹NullSituation(x) ≡ Null(x)›
571proof (safe intro!: "≡I" "→I" "df-null-uni:1"[THEN "≡⇩d⇩fI"]
572 "df-null-trivial:1"[THEN "≡⇩d⇩fI"]
573 dest!: "df-null-uni:1"[THEN "≡⇩d⇩fE"] "df-null-trivial:1"[THEN "≡⇩d⇩fE"])
574 AOT_assume 0: ‹Situation(x) & ¬∃p x ⊨ p›
575 AOT_have 1: ‹x[F] → ∃p F = [λy p]› for F
576 using 0[THEN "&E"(1), THEN situations[THEN "≡⇩d⇩fE"], THEN "&E"(2), THEN "∀E"(2)]
577 by (metis "≡⇩d⇩fE" "deduction-theorem" "prop-prop1" "→E")
578 AOT_show ‹A!x & ¬∃F x[F]›
579 proof (safe intro!: "&I" 0[THEN "&E"(1), THEN situations[THEN "≡⇩d⇩fE"],
580 THEN "&E"(1)];
581 rule "raa-cor:2")
582 AOT_assume ‹∃F x[F]›
583 then AOT_obtain F where F_prop: ‹x[F]›
584 using "∃E"[rotated] by blast
585 AOT_hence ‹∃p F = [λy p]›
586 using 1[THEN "→E"] by blast
587 then AOT_obtain p where ‹F = [λy p]›
588 using "∃E"[rotated] by blast
589 AOT_hence ‹x[λy p]›
590 by (metis "rule=E" F_prop)
591 AOT_hence ‹x ⊨ p›
592 using lem1[THEN "→E", OF 0[THEN "&E"(1)], THEN "≡E"(2)] by blast
593 AOT_hence ‹∃p x ⊨ p›
594 by (rule "∃I")
595 AOT_thus ‹∃p x ⊨ p & ¬∃p x ⊨ p›
596 using 0[THEN "&E"(2)] "&I" by blast
597 qed
598next
599 AOT_assume 0: ‹A!x & ¬∃F x[F]›
600 AOT_have ‹Situation(x)›
601 apply (rule situations[THEN "≡⇩d⇩fI", OF "&I", OF 0[THEN "&E"(1)]]; rule GEN)
602 using 0[THEN "&E"(2)] by (metis "→I" "existential:2[const_var]" "raa-cor:3")
603 moreover AOT_have ‹¬∃p x ⊨ p›
604 proof (rule "raa-cor:2")
605 AOT_assume ‹∃p x ⊨ p›
606 then AOT_obtain p where ‹x ⊨ p› by (metis "instantiation")
607 AOT_hence ‹x[λy p]› by (metis "≡⇩d⇩fE" "&E"(2) "prop-enc" "true-in-s")
608 AOT_hence ‹∃F x[F]› by (rule "∃I") "cqt:2[lambda]"
609 AOT_thus ‹∃F x[F] & ¬∃F x[F]› using 0[THEN "&E"(2)] "&I" by blast
610 qed
611 ultimately AOT_show ‹Situation(x) & ¬∃p x ⊨ p› using "&I" by blast
612qed
613
614AOT_theorem "null-triv-facts:2": ‹❙s⇩∅ = a⇩∅›
615 apply (rule "=⇩d⇩fI"(2)[OF "df-the-null-sit:1"])
616 apply (fact "thm-null-trivial:3")
617 apply (rule "=⇩d⇩fI"(2)[OF "df-null-uni-terms:1"])
618 apply (fact "null-uni-uniq:3")
619 apply (rule "equiv-desc-eq:3"[THEN "→E"])
620 apply (rule "&I")
621 apply (fact "thm-null-trivial:3")
622 by (rule RN; rule GEN; rule "null-triv-facts:1")
623
624AOT_theorem "null-triv-facts:3": ‹❙s⇩V ≠ a⇩V›
625proof(rule "=-infix"[THEN "≡⇩d⇩fI"])
626 AOT_have ‹Universal(a⇩V)›
627 by (simp add: "null-uni-facts:4")
628 AOT_hence 0: ‹a⇩V[A!]›
629 using "df-null-uni:2"[THEN "≡⇩d⇩fE"] "&E" "∀E"(1)
630 by (metis "cqt:5:a" "vdash-properties:10" "vdash-properties:1[2]")
631 moreover AOT_have 1: ‹¬❙s⇩V[A!]›
632 proof(rule "raa-cor:2")
633 AOT_have ‹Situation(❙s⇩V)›
634 using "≡⇩d⇩fE" "&E"(1) "df-null-trivial:2" "null-triv-sc:4" by blast
635 AOT_hence ‹∀F (❙s⇩V[F] → Propositional([F]))›
636 by (metis "≡⇩d⇩fE" "&E"(2) situations)
637 moreover AOT_assume ‹❙s⇩V[A!]›
638 ultimately AOT_have ‹Propositional(A!)›
639 using "∀E"(1)[rotated, OF "oa-exist:2"] "→E" by blast
640 AOT_thus ‹Propositional(A!) & ¬Propositional(A!)›
641 using "prop-in-f:4:d" "&I" by blast
642 qed
643 AOT_show ‹¬(❙s⇩V = a⇩V)›
644 proof (rule "raa-cor:2")
645 AOT_assume ‹❙s⇩V = a⇩V›
646 AOT_hence ‹❙s⇩V[A!]› using 0 "rule=E" id_sym by fast
647 AOT_thus ‹❙s⇩V[A!] & ¬❙s⇩V[A!]› using 1 "&I" by blast
648 qed
649qed
650
651definition ConditionOnPropositionalProperties :: ‹(<κ> ⇒ 𝗈) ⇒ bool› where
652 "cond-prop": ‹ConditionOnPropositionalProperties ≡ λ φ . ∀ v .
653 [v ⊨ ∀F (φ{F} → Propositional([F]))]›
654
655syntax ConditionOnPropositionalProperties :: ‹id_position ⇒ AOT_prop›
656 ("CONDITION'_ON'_PROPOSITIONAL'_PROPERTIES'(_')")
657
658AOT_theorem "cond-prop[E]":
659 assumes ‹CONDITION_ON_PROPOSITIONAL_PROPERTIES(φ)›
660 shows ‹∀F (φ{F} → Propositional([F]))›
661 using assms[unfolded "cond-prop"] by auto
662
663AOT_theorem "cond-prop[I]":
664 assumes ‹❙⊢⇩□ ∀F (φ{F} → Propositional([F]))›
665 shows ‹CONDITION_ON_PROPOSITIONAL_PROPERTIES(φ)›
666 using assms "cond-prop" by metis
667
668AOT_theorem "pre-comp-sit":
669 assumes ‹CONDITION_ON_PROPOSITIONAL_PROPERTIES(φ)›
670 shows ‹(Situation(x) & ∀F (x[F] ≡ φ{F})) ≡ (A!x & ∀F (x[F] ≡ φ{F}))›
671proof(rule "≡I"; rule "→I")
672 AOT_assume ‹Situation(x) & ∀F (x[F] ≡ φ{F})›
673 AOT_thus ‹A!x & ∀F (x[F] ≡ φ{F})›
674 using "&E" situations[THEN "≡⇩d⇩fE"] "&I" by blast
675next
676 AOT_assume 0: ‹A!x & ∀F (x[F] ≡ φ{F})›
677 AOT_show ‹Situation(x) & ∀F (x[F] ≡ φ{F})›
678 proof (safe intro!: situations[THEN "≡⇩d⇩fI"] "&I")
679 AOT_show ‹A!x› using 0[THEN "&E"(1)].
680 next
681 AOT_show ‹∀F (x[F] → Propositional([F]))›
682 proof(rule GEN; rule "→I")
683 fix F
684 AOT_assume ‹x[F]›
685 AOT_hence ‹φ{F}›
686 using 0[THEN "&E"(2)] "∀E" "≡E" by blast
687 AOT_thus ‹Propositional([F])›
688 using "cond-prop[E]"[OF assms] "∀E" "→E" by blast
689 qed
690 next
691 AOT_show ‹∀F (x[F] ≡ φ{F})› using 0 "&E" by blast
692 qed
693qed
694
695AOT_theorem "comp-sit:1":
696 assumes ‹CONDITION_ON_PROPOSITIONAL_PROPERTIES(φ)›
697 shows ‹∃s ∀F(s[F] ≡ φ{F})›
698 by (AOT_subst ‹Situation(x) & ∀F(x[F] ≡ φ{F})› ‹A!x & ∀F (x[F] ≡ φ{F})› for: x)
699 (auto simp: "pre-comp-sit"[OF assms] "A-objects"[where φ=φ, axiom_inst])
700
701AOT_theorem "comp-sit:2":
702 assumes ‹CONDITION_ON_PROPOSITIONAL_PROPERTIES(φ)›
703 shows ‹∃!s ∀F(s[F] ≡ φ{F})›
704 by (AOT_subst ‹Situation(x) & ∀F(x[F] ≡ φ{F})› ‹A!x & ∀F (x[F] ≡ φ{F})› for: x)
705 (auto simp: assms "pre-comp-sit" "pre-comp-sit"[OF assms] "A-objects!")
706
707AOT_theorem "can-sit-desc:1":
708 assumes ‹CONDITION_ON_PROPOSITIONAL_PROPERTIES(φ)›
709 shows ‹❙ιs(∀F (s[F] ≡ φ{F}))↓›
710 using "comp-sit:2"[OF assms] "A-Exists:2" "RA[2]" "≡E"(2) by blast
711
712AOT_theorem "can-sit-desc:2":
713 assumes ‹CONDITION_ON_PROPOSITIONAL_PROPERTIES(φ)›
714 shows ‹❙ιs(∀F (s[F] ≡ φ{F})) = ❙ιx(A!x & ∀F (x[F] ≡ φ{F}))›
715 by (auto intro!: "equiv-desc-eq:2"[THEN "→E", OF "&I",
716 OF "can-sit-desc:1"[OF assms]]
717 "RA[2]" GEN "pre-comp-sit"[OF assms])
718
719AOT_theorem "strict-sit":
720 assumes ‹RIGID_CONDITION(φ)›
721 and ‹CONDITION_ON_PROPOSITIONAL_PROPERTIES(φ)›
722 shows ‹y = ❙ιs(∀F (s[F] ≡ φ{F})) → ∀F (y[F] ≡ φ{F})›
723 using "rule=E"[rotated, OF "can-sit-desc:2"[OF assms(2), symmetric]]
724 "box-phi-a:2"[OF assms(1)] "→E" "→I" "&E" by fast
725
726
727
728AOT_define actual :: ‹τ ⇒ φ› (‹Actual'(_')›)
729 ‹Actual(s) ≡⇩d⇩f ∀p (s ⊨ p → p)›
730
731AOT_theorem "act-and-not-pos": ‹∃s (Actual(s) & ◇¬Actual(s))›
732proof -
733 AOT_obtain q⇩1 where q⇩1_prop: ‹q⇩1 & ◇¬q⇩1›
734 by (metis "≡⇩d⇩fE" "instantiation" "cont-tf:1" "cont-tf-thm:1")
735 AOT_have ‹∃s (∀F (s[F] ≡ F = [λy q⇩1]))›
736 proof (safe intro!: "comp-sit:1" "cond-prop[I]" GEN "→I")
737 AOT_modally_strict {
738 AOT_show ‹Propositional([F])› if ‹F = [λy q⇩1]› for F
739 using "≡⇩d⇩fI" "existential:2[const_var]" "prop-prop1" that by fastforce
740 }
741 qed
742 then AOT_obtain s⇩1 where s_prop: ‹∀F (s⇩1[F] ≡ F = [λy q⇩1])›
743 using "Situation.∃E"[rotated] by meson
744 AOT_have ‹Actual(s⇩1)›
745 proof(safe intro!: actual[THEN "≡⇩d⇩fI"] "&I" GEN "→I" s_prop Situation.ψ)
746 fix p
747 AOT_assume ‹s⇩1 ⊨ p›
748 AOT_hence ‹s⇩1[λy p]›
749 by (metis "≡⇩d⇩fE" "&E"(2) "prop-enc" "true-in-s")
750 AOT_hence ‹[λy p] = [λy q⇩1]›
751 by (rule s_prop[THEN "∀E"(1), THEN "≡E"(1), rotated]) "cqt:2[lambda]"
752 AOT_hence ‹p = q⇩1› by (metis "≡E"(2) "p-identity-thm2:3")
753 AOT_thus ‹p› using q⇩1_prop[THEN "&E"(1)] "rule=E" id_sym by fast
754 qed
755 moreover AOT_have ‹◇¬Actual(s⇩1)›
756 proof(rule "raa-cor:1"; drule "KBasic:12"[THEN "≡E"(2)])
757 AOT_assume ‹□Actual(s⇩1)›
758 AOT_hence ‹□(Situation(s⇩1) & ∀p (s⇩1 ⊨ p → p))›
759 using actual[THEN "≡Df", THEN "conventions:3"[THEN "≡⇩d⇩fE"],
760 THEN "&E"(1), THEN RM, THEN "→E"] by blast
761 AOT_hence ‹□∀p (s⇩1 ⊨ p → p)›
762 by (metis "RM:1" "Conjunction Simplification"(2) "→E")
763 AOT_hence ‹∀p □(s⇩1 ⊨ p → p)›
764 by (metis "CBF" "vdash-properties:10")
765 AOT_hence ‹□(s⇩1 ⊨ q⇩1 → q⇩1)›
766 using "∀E" by blast
767 AOT_hence ‹□s⇩1 ⊨ q⇩1 → □q⇩1›
768 by (metis "→E" "qml:1" "vdash-properties:1[2]")
769 moreover AOT_have ‹s⇩1 ⊨ q⇩1›
770 using s_prop[THEN "∀E"(1), THEN "≡E"(2),
771 THEN lem1[THEN "→E", OF Situation.ψ, THEN "≡E"(2)]]
772 "rule=I:1" "prop-prop2:2" by blast
773 ultimately AOT_have ‹□q⇩1›
774 using "≡⇩d⇩fE" "&E"(1) "≡E"(1) "lem2:1" "true-in-s" "→E" by fast
775 AOT_thus ‹◇¬q⇩1 & ¬◇¬q⇩1›
776 using "KBasic:12"[THEN "≡E"(1)] q⇩1_prop[THEN "&E"(2)] "&I" by blast
777 qed
778 ultimately AOT_have ‹(Actual(s⇩1) & ◇¬Actual(s⇩1))›
779 using s_prop "&I" by blast
780 thus ?thesis
781 by (rule "Situation.∃I")
782qed
783
784AOT_theorem "actual-s:1": ‹∃s Actual(s)›
785proof -
786 AOT_obtain s where ‹(Actual(s) & ◇¬Actual(s))›
787 using "act-and-not-pos" "Situation.∃E"[rotated] by meson
788 AOT_hence ‹Actual(s)› using "&E" "&I" by metis
789 thus ?thesis by (rule "Situation.∃I")
790qed
791
792AOT_theorem "actual-s:2": ‹∃s ¬Actual(s)›
793proof(rule "∃I"(1)[where τ=‹«❙s⇩V»›]; (rule "&I")?)
794 AOT_show ‹Situation(❙s⇩V)›
795 using "≡⇩d⇩fE" "&E"(1) "df-null-trivial:2" "null-triv-sc:4" by blast
796next
797 AOT_show ‹¬Actual(❙s⇩V)›
798 proof(rule "raa-cor:2")
799 AOT_assume 0: ‹Actual(❙s⇩V)›
800 AOT_obtain p⇩1 where notp⇩1: ‹¬p⇩1›
801 by (metis "∃E" "∃I"(1) "log-prop-prop:2" "non-contradiction")
802 AOT_have ‹❙s⇩V ⊨ p⇩1›
803 using "null-triv-sc:4"[THEN "≡⇩d⇩fE"[OF "df-null-trivial:2"], THEN "&E"(2)]
804 "∀E" by blast
805 AOT_hence ‹p⇩1›
806 using 0[THEN actual[THEN "≡⇩d⇩fE"], THEN "&E"(2), THEN "∀E"(2), THEN "→E"]
807 by blast
808 AOT_thus ‹p & ¬p› for p using notp⇩1 by (metis "raa-cor:3")
809 qed
810next
811 AOT_show ‹❙s⇩V↓›
812 using "df-the-null-sit:2" "rule-id-df:2:b[zero]" "thm-null-trivial:4" by blast
813qed
814
815AOT_theorem "actual-s:3": ‹∃p∀s(Actual(s) → ¬s ⊨ p)›
816proof -
817 AOT_obtain p⇩1 where notp⇩1: ‹¬p⇩1›
818 by (metis "∃E" "∃I"(1) "log-prop-prop:2" "non-contradiction")
819 AOT_have ‹∀s (Actual(s) → ¬(s ⊨ p⇩1))›
820 proof (rule Situation.GEN; rule "→I"; rule "raa-cor:2")
821 fix s
822 AOT_assume ‹Actual(s)›
823 moreover AOT_assume ‹s ⊨ p⇩1›
824 ultimately AOT_have ‹p⇩1›
825 using actual[THEN "≡⇩d⇩fE", THEN "&E"(2), THEN "∀E"(2), THEN "→E"] by blast
826 AOT_thus ‹p⇩1 & ¬p⇩1›
827 using notp⇩1 "&I" by simp
828 qed
829 thus ?thesis by (rule "∃I")
830qed
831
832AOT_theorem comp:
833 ‹∃s (s' ⊴ s & s'' ⊴ s & ∀s''' (s' ⊴ s''' & s'' ⊴ s''' → s ⊴ s'''))›
834proof -
835 have cond_prop: ‹ConditionOnPropositionalProperties (λ Π . «s'[Π] ∨ s''[Π]»)›
836 proof(safe intro!: "cond-prop[I]" GEN "oth-class-taut:8:c"[THEN "→E", THEN "→E"];
837 rule "→I")
838 AOT_modally_strict {
839 fix F
840 AOT_have ‹Situation(s')›
841 by (simp add: Situation.restricted_var_condition)
842 AOT_hence ‹s'[F] → Propositional([F])›
843 using "situations"[THEN "≡⇩d⇩fE", THEN "&E"(2), THEN "∀E"(2)] by blast
844 moreover AOT_assume ‹s'[F]›
845 ultimately AOT_show ‹Propositional([F])›
846 using "→E" by blast
847 }
848 next
849 AOT_modally_strict {
850 fix F
851 AOT_have ‹Situation(s'')›
852 by (simp add: Situation.restricted_var_condition)
853 AOT_hence ‹s''[F] → Propositional([F])›
854 using "situations"[THEN "≡⇩d⇩fE", THEN "&E"(2), THEN "∀E"(2)] by blast
855 moreover AOT_assume ‹s''[F]›
856 ultimately AOT_show ‹Propositional([F])›
857 using "→E" by blast
858 }
859 qed
860 AOT_obtain s⇩3 where θ: ‹∀F (s⇩3[F] ≡ s'[F] ∨ s''[F])›
861 using "comp-sit:1"[OF cond_prop] "Situation.∃E"[rotated] by meson
862 AOT_have ‹s' ⊴ s⇩3 & s'' ⊴ s⇩3 & ∀s''' (s' ⊴ s''' & s'' ⊴ s''' → s⇩3 ⊴ s''')›
863 proof(safe intro!: "&I" "≡⇩d⇩fI"[OF "true-in-s"] "≡⇩d⇩fI"[OF "prop-enc"]
864 "Situation.GEN" "GEN"[where 'a=𝗈] "→I"
865 "sit-part-whole"[THEN "≡⇩d⇩fI"]
866 Situation.ψ "cqt:2[const_var]"[axiom_inst])
867 fix p
868 AOT_assume ‹s' ⊨ p›
869 AOT_hence ‹s'[λx p]›
870 by (metis "&E"(2) "prop-enc" "≡⇩d⇩fE" "true-in-s")
871 AOT_thus ‹s⇩3[λx p]›
872 using θ[THEN "∀E"(1),OF "prop-prop2:2", THEN "≡E"(2), OF "∨I"(1)] by blast
873 next
874 fix p
875 AOT_assume ‹s'' ⊨ p›
876 AOT_hence ‹s''[λx p]›
877 by (metis "&E"(2) "prop-enc" "≡⇩d⇩fE" "true-in-s")
878 AOT_thus ‹s⇩3[λx p]›
879 using θ[THEN "∀E"(1),OF "prop-prop2:2", THEN "≡E"(2), OF "∨I"(2)] by blast
880 next
881 fix s p
882 AOT_assume 0: ‹s' ⊴ s & s'' ⊴ s›
883 AOT_assume ‹s⇩3 ⊨ p›
884 AOT_hence ‹s⇩3[λx p]›
885 by (metis "&E"(2) "prop-enc" "≡⇩d⇩fE" "true-in-s")
886 AOT_hence ‹s'[λx p] ∨ s''[λx p]›
887 using θ[THEN "∀E"(1),OF "prop-prop2:2", THEN "≡E"(1)] by blast
888 moreover {
889 AOT_assume ‹s'[λx p]›
890 AOT_hence ‹s' ⊨ p›
891 by (safe intro!: "prop-enc"[THEN "≡⇩d⇩fI"] "true-in-s"[THEN "≡⇩d⇩fI"] "&I"
892 Situation.ψ "cqt:2[const_var]"[axiom_inst])
893 moreover AOT_have ‹s' ⊨ p → s ⊨ p›
894 using "sit-part-whole"[THEN "≡⇩d⇩fE", THEN "&E"(2)] 0[THEN "&E"(1)]
895 "∀E"(2) by blast
896 ultimately AOT_have ‹s ⊨ p›
897 using "→E" by blast
898 AOT_hence ‹s[λx p]›
899 using "true-in-s"[THEN "≡⇩d⇩fE"] "prop-enc"[THEN "≡⇩d⇩fE"] "&E" by blast
900 }
901 moreover {
902 AOT_assume ‹s''[λx p]›
903 AOT_hence ‹s'' ⊨ p›
904 by (safe intro!: "prop-enc"[THEN "≡⇩d⇩fI"] "true-in-s"[THEN "≡⇩d⇩fI"] "&I"
905 Situation.ψ "cqt:2[const_var]"[axiom_inst])
906 moreover AOT_have ‹s'' ⊨ p → s ⊨ p›
907 using "sit-part-whole"[THEN "≡⇩d⇩fE", THEN "&E"(2)] 0[THEN "&E"(2)]
908 "∀E"(2) by blast
909 ultimately AOT_have ‹s ⊨ p›
910 using "→E" by blast
911 AOT_hence ‹s[λx p]›
912 using "true-in-s"[THEN "≡⇩d⇩fE"] "prop-enc"[THEN "≡⇩d⇩fE"] "&E" by blast
913 }
914 ultimately AOT_show ‹s[λx p]›
915 by (metis "∨E"(1) "→I")
916 qed
917 thus ?thesis
918 using "Situation.∃I" by fast
919qed
920
921AOT_theorem "act-sit:1": ‹Actual(s) → (s ⊨ p → [λy p]s)›
922proof (safe intro!: "→I")
923 AOT_assume ‹Actual(s)›
924 AOT_hence p if ‹s ⊨ p›
925 using actual[THEN "≡⇩d⇩fE", THEN "&E"(2), THEN "∀E"(2), THEN "→E"] that by blast
926 moreover AOT_assume ‹s ⊨ p›
927 ultimately AOT_have p by blast
928 AOT_thus ‹[λy p]s›
929 by (safe intro!: "β←C"(1) "cqt:2")
930qed
931
932AOT_theorem "act-sit:2":
933 ‹(Actual(s') & Actual(s'')) → ∃x (Actual(x) & s' ⊴ x & s'' ⊴ x)›
934proof(rule "→I"; frule "&E"(1); drule "&E"(2))
935 AOT_assume act_s': ‹Actual(s')›
936 AOT_assume act_s'': ‹Actual(s'')›
937 have "cond-prop": ‹ConditionOnPropositionalProperties
938 (λ Π . «∃p (Π = [λy p] & (s' ⊨ p ∨ s'' ⊨ p))»)›
939 proof (safe intro!: "cond-prop[I]" "∀I" "→I" "prop-prop1"[THEN "≡⇩d⇩fI"])
940 AOT_modally_strict {
941 fix β
942 AOT_assume ‹∃p (β = [λy p] & (s' ⊨ p ∨ s'' ⊨ p))›
943 then AOT_obtain p where ‹β = [λy p]› using "∃E"[rotated] "&E" by blast
944 AOT_thus ‹∃p β = [λy p]› by (rule "∃I")
945 }
946 qed
947 have rigid: ‹rigid_condition (λ Π . «∃p (Π = [λy p] & (s' ⊨ p ∨ s'' ⊨ p))»)›
948 proof(safe intro!: "strict-can:1[I]" "→I" GEN)
949 AOT_modally_strict {
950 fix F
951 AOT_assume ‹∃p (F = [λy p] & (s' ⊨ p ∨ s'' ⊨ p))›
952 then AOT_obtain p⇩1 where p⇩1_prop: ‹F = [λy p⇩1] & (s' ⊨ p⇩1 ∨ s'' ⊨ p⇩1)›
953 using "∃E"[rotated] by blast
954 AOT_hence ‹□(F = [λy p⇩1])›
955 using "&E"(1) "id-nec:2" "vdash-properties:10" by blast
956 moreover AOT_have ‹□(s' ⊨ p⇩1 ∨ s'' ⊨ p⇩1)›
957 proof(rule "∨E"; (rule "→I"; rule "KBasic:15"[THEN "→E"])?)
958 AOT_show ‹s' ⊨ p⇩1 ∨ s'' ⊨ p⇩1› using p⇩1_prop "&E" by blast
959 next
960 AOT_show ‹□s' ⊨ p⇩1 ∨ □s'' ⊨ p⇩1› if ‹s' ⊨ p⇩1›
961 apply (rule "∨I"(1))
962 using "≡⇩d⇩fE" "&E"(1) "≡E"(1) "lem2:1" that "true-in-s" by blast
963 next
964 AOT_show ‹□s' ⊨ p⇩1 ∨ □s'' ⊨ p⇩1› if ‹s'' ⊨ p⇩1›
965 apply (rule "∨I"(2))
966 using "≡⇩d⇩fE" "&E"(1) "≡E"(1) "lem2:1" that "true-in-s" by blast
967 qed
968 ultimately AOT_have ‹□(F = [λy p⇩1] & (s' ⊨ p⇩1 ∨ s'' ⊨ p⇩1))›
969 by (metis "KBasic:3" "&I" "≡E"(2))
970 AOT_hence ‹∃p □(F = [λy p] & (s' ⊨ p ∨ s'' ⊨ p))› by (rule "∃I")
971 AOT_thus ‹□∃p (F = [λy p] & (s' ⊨ p ∨ s'' ⊨ p))›
972 using Buridan[THEN "→E"] by fast
973 }
974 qed
975
976 AOT_have desc_den: ‹❙ιs(∀F (s[F] ≡ ∃p (F = [λy p] & (s' ⊨ p ∨ s'' ⊨ p))))↓›
977 by (rule "can-sit-desc:1"[OF "cond-prop"])
978 AOT_obtain x⇩0
979 where x⇩0_prop1: ‹x⇩0 = ❙ιs(∀F (s[F] ≡ ∃p (F = [λy p] & (s' ⊨ p ∨ s'' ⊨ p))))›
980 by (metis (no_types, lifting) "∃E" "rule=I:1" desc_den "∃I"(1) id_sym)
981 AOT_hence x⇩0_sit: ‹Situation(x⇩0)›
982 using "actual-desc:3"[THEN "→E"] "Act-Basic:2" "&E"(1) "≡E"(1)
983 "possit-sit:4" by blast
984
985 AOT_have 1: ‹∀F (x⇩0[F] ≡ ∃p (F = [λy p] & (s' ⊨ p ∨ s'' ⊨ p)))›
986 using "strict-sit"[OF rigid, OF "cond-prop", THEN "→E", OF x⇩0_prop1].
987 AOT_have 2: ‹(x⇩0 ⊨ p) ≡ (s' ⊨ p ∨ s'' ⊨ p)› for p
988 proof (rule "≡I"; rule "→I")
989 AOT_assume ‹x⇩0 ⊨ p›
990 AOT_hence ‹x⇩0[λy p]› using lem1[THEN "→E", OF x⇩0_sit, THEN "≡E"(1)] by blast
991 then AOT_obtain q where ‹[λy p] = [λy q] & (s' ⊨ q ∨ s'' ⊨ q)›
992 using 1[THEN "∀E"(1)[where τ="«[λy p]»"], OF "prop-prop2:2", THEN "≡E"(1)]
993 "∃E"[rotated] by blast
994 AOT_thus ‹s' ⊨ p ∨ s'' ⊨ p›
995 by (metis "rule=E" "&E"(1) "&E"(2) "∨I"(1) "∨I"(2)
996 "∨E"(1) "deduction-theorem" id_sym "≡E"(2) "p-identity-thm2:3")
997 next
998 AOT_assume ‹s' ⊨ p ∨ s'' ⊨ p›
999 AOT_hence ‹[λy p] = [λy p] & (s' ⊨ p ∨ s'' ⊨ p)›
1000 by (metis "rule=I:1" "&I" "prop-prop2:2")
1001 AOT_hence ‹∃q ([λy p] = [λy q] & (s' ⊨ q ∨ s'' ⊨ q))›
1002 by (rule "∃I")
1003 AOT_hence ‹x⇩0[λy p]›
1004 using 1[THEN "∀E"(1), OF "prop-prop2:2", THEN "≡E"(2)] by blast
1005 AOT_thus ‹x⇩0 ⊨ p›
1006 by (metis "≡⇩d⇩fI" "&I" "ex:1:a" "prop-enc" "rule-ui:2[const_var]"
1007 x⇩0_sit "true-in-s")
1008 qed
1009
1010 AOT_have ‹Actual(x⇩0) & s' ⊴ x⇩0 & s'' ⊴ x⇩0›
1011 proof(safe intro!: "→I" "&I" "∃I"(1) actual[THEN "≡⇩d⇩fI"] x⇩0_sit GEN
1012 "sit-part-whole"[THEN "≡⇩d⇩fI"])
1013 fix p
1014 AOT_assume ‹x⇩0 ⊨ p›
1015 AOT_hence ‹s' ⊨ p ∨ s'' ⊨ p›
1016 using 2 "≡E"(1) by metis
1017 AOT_thus ‹p›
1018 using act_s' act_s''
1019 actual[THEN "≡⇩d⇩fE", THEN "&E"(2), THEN "∀E"(2), THEN "→E"]
1020 by (metis "∨E"(3) "reductio-aa:1")
1021 next
1022 AOT_show ‹x⇩0 ⊨ p› if ‹s' ⊨ p› for p
1023 using 2[THEN "≡E"(2), OF "∨I"(1), OF that].
1024 next
1025 AOT_show ‹x⇩0 ⊨ p› if ‹s'' ⊨ p› for p
1026 using 2[THEN "≡E"(2), OF "∨I"(2), OF that].
1027 next
1028 AOT_show ‹Situation(s')›
1029 using act_s'[THEN actual[THEN "≡⇩d⇩fE"]] "&E" by blast
1030 next
1031 AOT_show ‹Situation(s'')›
1032 using act_s''[THEN actual[THEN "≡⇩d⇩fE"]] "&E" by blast
1033 qed
1034 AOT_thus ‹∃x (Actual(x) & s' ⊴ x & s'' ⊴ x)›
1035 by (rule "∃I")
1036qed
1037
1038AOT_define Consistent :: ‹τ ⇒ φ› (‹Consistent'(_')›)
1039 cons: ‹Consistent(s) ≡⇩d⇩f ¬∃p (s ⊨ p & s ⊨ ¬p)›
1040
1041AOT_theorem "sit-cons": ‹Actual(s) → Consistent(s)›
1042proof(safe intro!: "→I" cons[THEN "≡⇩d⇩fI"] "&I" Situation.ψ
1043 dest!: actual[THEN "≡⇩d⇩fE"]; frule "&E"(1); drule "&E"(2))
1044 AOT_assume 0: ‹∀p (s ⊨ p → p)›
1045 AOT_show ‹¬∃p (s ⊨ p & s ⊨ ¬p)›
1046 proof (rule "raa-cor:2")
1047 AOT_assume ‹∃p (s ⊨ p & s ⊨ ¬p)›
1048 then AOT_obtain p where ‹s ⊨ p & s ⊨ ¬p›
1049 using "∃E"[rotated] by blast
1050 AOT_hence ‹p & ¬p›
1051 using 0[THEN "∀E"(1)[where τ=‹«¬p»›, THEN "→E"], OF "log-prop-prop:2"]
1052 0[THEN "∀E"(2)[where β=p], THEN "→E"] "&E" "&I" by blast
1053 AOT_thus ‹p & ¬p› for p by (metis "raa-cor:1")
1054 qed
1055qed
1056
1057AOT_theorem "cons-rigid:1": ‹¬Consistent(s) ≡ □¬Consistent(s)›
1058proof (rule "≡I"; rule "→I")
1059 AOT_assume ‹¬Consistent(s)›
1060 AOT_hence ‹∃p (s ⊨ p & s ⊨ ¬p)›
1061 using cons[THEN "≡⇩d⇩fI", OF "&I", OF Situation.ψ]
1062 by (metis "raa-cor:3")
1063 then AOT_obtain p where p_prop: ‹s ⊨ p & s ⊨ ¬p›
1064 using "∃E"[rotated] by blast
1065 AOT_hence ‹□s ⊨ p›
1066 using "&E"(1) "≡E"(1) "lem2:1" by blast
1067 moreover AOT_have ‹□s ⊨ ¬p›
1068 using p_prop "T◇" "&E" "≡E"(1)
1069 "modus-tollens:1" "raa-cor:3" "lem2:3"[unvarify p]
1070 "log-prop-prop:2" by metis
1071 ultimately AOT_have ‹□(s ⊨ p & s ⊨ ¬p)›
1072 by (metis "KBasic:3" "&I" "≡E"(2))
1073 AOT_hence ‹∃p □(s ⊨ p & s ⊨ ¬p)›
1074 by (rule "∃I")
1075 AOT_hence ‹□∃p(s ⊨ p & s ⊨ ¬p)›
1076 by (metis Buridan "vdash-properties:10")
1077 AOT_thus ‹□¬Consistent(s)›
1078 apply (rule "qml:1"[axiom_inst, THEN "→E", THEN "→E", rotated])
1079 apply (rule RN)
1080 using "≡⇩d⇩fE" "&E"(2) cons "deduction-theorem" "raa-cor:3" by blast
1081next
1082 AOT_assume ‹□¬Consistent(s)›
1083 AOT_thus ‹¬Consistent(s)› using "qml:2"[axiom_inst, THEN "→E"] by auto
1084qed
1085
1086AOT_theorem "cons-rigid:2": ‹◇Consistent(x) ≡ Consistent(x)›
1087proof(rule "≡I"; rule "→I")
1088 AOT_assume 0: ‹◇Consistent(x)›
1089 AOT_have ‹◇(Situation(x) & ¬∃p (x ⊨ p & x ⊨ ¬p))›
1090 apply (AOT_subst ‹Situation(x) & ¬∃p (x ⊨ p & x ⊨ ¬p)› ‹Consistent(x)›)
1091 using cons "≡E"(2) "Commutativity of ≡" "≡Df" apply blast
1092 by (simp add: 0)
1093 AOT_hence ‹◇Situation(x)› and 1: ‹◇¬∃p (x ⊨ p & x ⊨ ¬p)›
1094 using "RM◇" "Conjunction Simplification"(1) "Conjunction Simplification"(2)
1095 "modus-tollens:1" "raa-cor:3" by blast+
1096 AOT_hence 2: ‹Situation(x)› by (metis "≡E"(1) "possit-sit:2")
1097 AOT_have 3: ‹¬□∃p (x ⊨ p & x ⊨ ¬p)›
1098 using 2 using 1 "KBasic:11" "≡E"(2) by blast
1099 AOT_show ‹Consistent(x)›
1100 proof (rule "raa-cor:1")
1101 AOT_assume ‹¬Consistent(x)›
1102 AOT_hence ‹∃p (x ⊨ p & x ⊨ ¬p)›
1103 using 0 "≡⇩d⇩fE" "conventions:5" 2 "cons-rigid:1"[unconstrain s, THEN "→E"]
1104 "modus-tollens:1" "raa-cor:3" "≡E"(4) by meson
1105 then AOT_obtain p where ‹x ⊨ p› and 4: ‹x ⊨ ¬p›
1106 using "∃E"[rotated] "&E" by blast
1107 AOT_hence ‹□x ⊨ p›
1108 by (metis "2" "≡E"(1) "lem2:1"[unconstrain s, THEN "→E"])
1109 moreover AOT_have ‹□x ⊨ ¬p›
1110 using 4 "lem2:1"[unconstrain s, unvarify p, THEN "→E"]
1111 by (metis 2 "≡E"(1) "log-prop-prop:2")
1112 ultimately AOT_have ‹□(x ⊨ p & x ⊨ ¬p)›
1113 by (metis "KBasic:3" "&I" "≡E"(3) "raa-cor:3")
1114 AOT_hence ‹∃p □(x ⊨ p & x ⊨ ¬p)›
1115 by (metis "existential:1" "log-prop-prop:2")
1116 AOT_hence ‹□∃p (x ⊨ p & x ⊨ ¬p)›
1117 by (metis Buridan "vdash-properties:10")
1118 AOT_thus ‹p & ¬p› for p
1119 using 3 "&I" by (metis "raa-cor:3")
1120 qed
1121next
1122 AOT_show ‹◇Consistent(x)› if ‹Consistent(x)›
1123 using "T◇" that "vdash-properties:10" by blast
1124qed
1125
1126AOT_define possible :: ‹τ ⇒ φ› (‹Possible'(_')›)
1127 pos: ‹Possible(s) ≡⇩d⇩f ◇Actual(s)›
1128
1129AOT_theorem "sit-pos:1": ‹Actual(s) → Possible(s)›
1130 apply(rule "→I"; rule pos[THEN "≡⇩d⇩fI"]; rule "&I")
1131 apply (meson "≡⇩d⇩fE" actual "&E"(1))
1132 using "T◇" "vdash-properties:10" by blast
1133
1134AOT_theorem "sit-pos:2": ‹∃p ((s ⊨ p) & ¬◇p) → ¬Possible(s)›
1135proof(rule "→I")
1136 AOT_assume ‹∃p ((s ⊨ p) & ¬◇p)›
1137 then AOT_obtain p where a: ‹(s ⊨ p) & ¬◇p›
1138 using "∃E"[rotated] by blast
1139 AOT_hence ‹□(s ⊨ p)›
1140 using "&E" by (metis "T◇" "≡E"(1) "lem2:3" "vdash-properties:10")
1141 moreover AOT_have ‹□¬p›
1142 using a[THEN "&E"(2)] by (metis "KBasic2:1" "≡E"(2))
1143 ultimately AOT_have ‹□(s ⊨ p & ¬p)›
1144 by (metis "KBasic:3" "&I" "≡E"(3) "raa-cor:3")
1145 AOT_hence ‹∃p □(s ⊨ p & ¬p)›
1146 by (rule "∃I")
1147 AOT_hence 1: ‹□∃q (s ⊨ q & ¬q)›
1148 by (metis Buridan "vdash-properties:10")
1149 AOT_have ‹□¬∀q (s ⊨ q → q)›
1150 apply (AOT_subst ‹s ⊨ q → q› ‹¬(s ⊨ q & ¬q)› for: q)
1151 apply (simp add: "oth-class-taut:1:a")
1152 apply (AOT_subst ‹¬∀q ¬(s ⊨ q & ¬q)› ‹∃q (s ⊨ q & ¬q)›)
1153 by (auto simp: "conventions:4" "df-rules-formulas[3]" "df-rules-formulas[4]" "≡I" 1)
1154 AOT_hence 0: ‹¬◇∀q (s ⊨ q → q)›
1155 by (metis "≡⇩d⇩fE" "conventions:5" "raa-cor:3")
1156 AOT_show ‹¬Possible(s)›
1157 apply (AOT_subst ‹Possible(s)› ‹Situation(s) & ◇Actual(s)›)
1158 apply (simp add: pos "≡Df")
1159 apply (AOT_subst ‹Actual(s)› ‹Situation(s) & ∀q (s ⊨ q → q)›)
1160 using actual "≡Df" apply presburger
1161 by (metis "0" "KBasic2:3" "&E"(2) "raa-cor:3" "vdash-properties:10")
1162qed
1163
1164AOT_theorem "pos-cons-sit:1": ‹Possible(s) → Consistent(s)›
1165 by (auto simp: "sit-cons"[THEN "RM◇", THEN "→E",
1166 THEN "cons-rigid:2"[THEN "≡E"(1)]]
1167 intro!: "→I" dest!: pos[THEN "≡⇩d⇩fE"] "&E"(2))
1168
1169AOT_theorem "pos-cons-sit:2": ‹∃s (Consistent(s) & ¬Possible(s))›
1170proof -
1171 AOT_obtain q⇩1 where ‹q⇩1 & ◇¬q⇩1›
1172 using "≡⇩d⇩fE" "instantiation" "cont-tf:1" "cont-tf-thm:1" by blast
1173 have "cond-prop": ‹ConditionOnPropositionalProperties
1174 (λ Π . «Π = [λy q⇩1 & ¬q⇩1]»)›
1175 by (auto intro!: "cond-prop[I]" GEN "→I" "prop-prop1"[THEN "≡⇩d⇩fI"]
1176 "∃I"(1)[where τ=‹«q⇩1 & ¬q⇩1»›, rotated, OF "log-prop-prop:2"])
1177 have rigid: ‹rigid_condition (λ Π . «Π = [λy q⇩1 & ¬q⇩1]»)›
1178 by (auto intro!: "strict-can:1[I]" GEN "→I" simp: "id-nec:2"[THEN "→E"])
1179
1180 AOT_obtain x where x_prop: ‹x = ❙ιs (∀F (s[F] ≡ F = [λy q⇩1 & ¬q⇩1]))›
1181 using "ex:1:b"[THEN "∀E"(1), OF "can-sit-desc:1", OF "cond-prop"]
1182 "∃E"[rotated] by blast
1183 AOT_hence 0: ‹❙𝒜(Situation(x) & ∀F (x[F] ≡ F = [λy q⇩1 & ¬q⇩1]))›
1184 using "→E" "actual-desc:2" by blast
1185 AOT_hence ‹❙𝒜(Situation(x))› by (metis "Act-Basic:2" "&E"(1) "≡E"(1))
1186 AOT_hence s_sit: ‹Situation(x)› by (metis "≡E"(1) "possit-sit:4")
1187 AOT_have s_enc_prop: ‹∀F (x[F] ≡ F = [λy q⇩1 & ¬q⇩1])›
1188 using "strict-sit"[OF rigid, OF "cond-prop", THEN "→E", OF x_prop].
1189 AOT_hence ‹x[λy q⇩1 & ¬q⇩1]›
1190 using "∀E"(1)[rotated, OF "prop-prop2:2"]
1191 "rule=I:1"[OF "prop-prop2:2"] "≡E" by blast
1192 AOT_hence ‹x ⊨ (q⇩1 & ¬q⇩1)›
1193 using lem1[THEN "→E", OF s_sit, unvarify p, THEN "≡E"(2), OF "log-prop-prop:2"]
1194 by blast
1195 AOT_hence ‹□(x ⊨ (q⇩1 & ¬q⇩1))›
1196 using "lem2:1"[unconstrain s, THEN "→E", OF s_sit, unvarify p,
1197 OF "log-prop-prop:2", THEN "≡E"(1)] by blast
1198 moreover AOT_have ‹□(x ⊨ (q⇩1 & ¬q⇩1) → ¬Actual(x))›
1199 proof(rule RN; rule "→I"; rule "raa-cor:2")
1200 AOT_modally_strict {
1201 AOT_assume ‹Actual(x)›
1202 AOT_hence ‹∀p (x ⊨ p → p)›
1203 using actual[THEN "≡⇩d⇩fE", THEN "&E"(2)] by blast
1204 moreover AOT_assume ‹x ⊨ (q⇩1 & ¬q⇩1)›
1205 ultimately AOT_show ‹q⇩1 & ¬q⇩1›
1206 using "∀E"(1)[rotated, OF "log-prop-prop:2"] "→E" by metis
1207 }
1208 qed
1209 ultimately AOT_have nec_not_actual_s: ‹□¬Actual(x)›
1210 using "qml:1"[axiom_inst, THEN "→E", THEN "→E"] by blast
1211 AOT_have 1: ‹¬∃p (x ⊨ p & x ⊨ ¬p)›
1212 proof (rule "raa-cor:2")
1213 AOT_assume ‹∃p (x ⊨ p & x ⊨ ¬p)›
1214 then AOT_obtain p where ‹x ⊨ p & x ⊨ ¬p›
1215 using "∃E"[rotated] by blast
1216 AOT_hence ‹x[λy p] & x[λy ¬p]›
1217 using lem1[unvarify p, THEN "→E", OF "log-prop-prop:2",
1218 OF s_sit, THEN "≡E"(1)] "&I" "&E" by metis
1219 AOT_hence ‹[λy p] = [λy q⇩1 & ¬q⇩1]› and ‹[λy ¬p] = [λy q⇩1 & ¬q⇩1]›
1220 by (auto intro!: "prop-prop2:2" s_enc_prop[THEN "∀E"(1), THEN "≡E"(1)]
1221 elim: "&E")
1222 AOT_hence i: ‹[λy p] = [λy ¬p]› by (metis "rule=E" id_sym)
1223 {
1224 AOT_assume 0: ‹p›
1225 AOT_have ‹[λy p]x› for x
1226 by (auto intro!: "β←C"(1) "cqt:2" 0)
1227 AOT_hence ‹[λy ¬p]x› for x using i "rule=E" by fast
1228 AOT_hence ‹¬p›
1229 using "β→C"(1) by auto
1230 }
1231 moreover {
1232 AOT_assume 0: ‹¬p›
1233 AOT_have ‹[λy ¬p]x› for x
1234 by (auto intro!: "β←C"(1) "cqt:2" 0)
1235 AOT_hence ‹[λy p]x› for x using i[symmetric] "rule=E" by fast
1236 AOT_hence ‹p›
1237 using "β→C"(1) by auto
1238 }
1239 ultimately AOT_show ‹p & ¬p› for p by (metis "raa-cor:1" "raa-cor:3")
1240 qed
1241 AOT_have 2: ‹¬Possible(x)›
1242 proof(rule "raa-cor:2")
1243 AOT_assume ‹Possible(x)›
1244 AOT_hence ‹◇Actual(x)›
1245 by (metis "≡⇩d⇩fE" "&E"(2) pos)
1246 moreover AOT_have ‹¬◇Actual(x)› using nec_not_actual_s
1247 using "≡⇩d⇩fE" "conventions:5" "reductio-aa:2" by blast
1248 ultimately AOT_show ‹◇Actual(x) & ¬◇Actual(x)› by (rule "&I")
1249 qed
1250 show ?thesis
1251 by(rule "∃I"(2)[where β=x]; safe intro!: "&I" 2 s_sit cons[THEN "≡⇩d⇩fI"] 1)
1252qed
1253
1254AOT_theorem "sit-classical:1": ‹∀p (s ⊨ p ≡ p) → ∀q(s ⊨ ¬q ≡ ¬s ⊨ q)›
1255proof(rule "→I"; rule GEN)
1256 fix q
1257 AOT_assume ‹∀p (s ⊨ p ≡ p)›
1258 AOT_hence ‹s ⊨ q ≡ q› and ‹s ⊨ ¬q ≡ ¬q›
1259 using "∀E"(1)[rotated, OF "log-prop-prop:2"] by blast+
1260 AOT_thus ‹s ⊨ ¬q ≡ ¬s ⊨ q›
1261 by (metis "deduction-theorem" "≡I" "≡E"(1) "≡E"(2) "≡E"(4))
1262qed
1263
1264AOT_theorem "sit-classical:2":
1265 ‹∀p (s ⊨ p ≡ p) → ∀q∀r((s ⊨ (q → r)) ≡ (s ⊨ q → s ⊨ r))›
1266proof(rule "→I"; rule GEN; rule GEN)
1267 fix q r
1268 AOT_assume ‹∀p (s ⊨ p ≡ p)›
1269 AOT_hence θ: ‹s ⊨ q ≡ q› and ξ: ‹s ⊨ r ≡ r› and ζ: ‹(s ⊨ (q → r)) ≡ (q → r)›
1270 using "∀E"(1)[rotated, OF "log-prop-prop:2"] by blast+
1271 AOT_show ‹(s ⊨ (q → r)) ≡ (s ⊨ q → s ⊨ r)›
1272 proof (safe intro!: "≡I" "→I")
1273 AOT_assume ‹s ⊨ (q → r)›
1274 moreover AOT_assume ‹s ⊨ q›
1275 ultimately AOT_show ‹s ⊨ r›
1276 using θ ξ ζ by (metis "≡E"(1) "≡E"(2) "vdash-properties:10")
1277 next
1278 AOT_assume ‹s ⊨ q → s ⊨ r›
1279 AOT_thus ‹s ⊨ (q → r)›
1280 using θ ξ ζ by (metis "deduction-theorem" "≡E"(1) "≡E"(2) "→E")
1281 qed
1282qed
1283
1284AOT_theorem "sit-classical:3":
1285 ‹∀p (s ⊨ p ≡ p) → ((s ⊨ ∀α φ{α}) ≡ ∀α s ⊨ φ{α})›
1286proof (rule "→I")
1287 AOT_assume ‹∀p (s ⊨ p ≡ p)›
1288 AOT_hence θ: ‹s ⊨ φ{α} ≡ φ{α}› and ξ: ‹s ⊨ ∀α φ{α} ≡ ∀α φ{α}› for α
1289 using "∀E"(1)[rotated, OF "log-prop-prop:2"] by blast+
1290 AOT_show ‹s ⊨ ∀α φ{α} ≡ ∀α s ⊨ φ{α}›
1291 proof (safe intro!: "≡I" "→I" GEN)
1292 fix α
1293 AOT_assume ‹s ⊨ ∀α φ{α}›
1294 AOT_hence ‹φ{α}› using ξ "∀E"(2) "≡E"(1) by blast
1295 AOT_thus ‹s ⊨ φ{α}› using θ "≡E"(2) by blast
1296 next
1297 AOT_assume ‹∀α s ⊨ φ{α}›
1298 AOT_hence ‹s ⊨ φ{α}› for α using "∀E"(2) by blast
1299 AOT_hence ‹φ{α}› for α using θ "≡E"(1) by blast
1300 AOT_hence ‹∀α φ{α}› by (rule GEN)
1301 AOT_thus ‹s ⊨ ∀α φ{α}› using ξ "≡E"(2) by blast
1302 qed
1303qed
1304
1305AOT_theorem "sit-classical:4": ‹∀p (s ⊨ p ≡ p) → ∀q (s ⊨ □q → □s ⊨ q)›
1306proof(rule "→I"; rule GEN; rule "→I")
1307 fix q
1308 AOT_assume ‹∀p (s ⊨ p ≡ p)›
1309 AOT_hence θ: ‹s ⊨ q ≡ q› and ξ: ‹s ⊨ □q ≡ □q›
1310 using "∀E"(1)[rotated, OF "log-prop-prop:2"] by blast+
1311 AOT_assume ‹s ⊨ □q›
1312 AOT_hence ‹□q› using ξ "≡E"(1) by blast
1313 AOT_hence ‹q› using "qml:2"[axiom_inst, THEN "→E"] by blast
1314 AOT_hence ‹s ⊨ q› using θ "≡E"(2) by blast
1315 AOT_thus ‹□s ⊨ q› using "≡⇩d⇩fE" "&E"(1) "≡E