Theory AOT_Possibilities

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