Theory AOT_Possibilities
1theory AOT_Possibilities
2 imports AOT_PossibleWorlds
3begin
4
5section‹Possibilities›
6
7AOT_define ModallyClosed :: ‹τ ⇒ φ› (‹ModallyClosed'(_')›)
8 "sit-clo": ‹ModallyClosed(s) ≡⇩d⇩f ∀p((Actual(s) ⇒ p) → s ⊨ p)›
9
10AOT_theorem "modal-clos-facts:1": ‹ModallyClosed(s) → ∀p∀q((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 "≡⇩d⇩fE" "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 "≡⇩d⇩fI" "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) → ∀p⇩1∀p⇩2∀q((s ⊨ p⇩1 & s ⊨ p⇩2 & ((p⇩1 & p⇩2) ⇒ q)) → s ⊨ q)›
56proof(safe intro!: "→I" GEN)
57 fix p⇩1 p⇩2 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 ⊨ p⇩1 & s ⊨ p⇩2 & ((p⇩1 & p⇩2) ⇒ 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 "≡⇩d⇩fE" "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 ⊨ p⇩1 → □(Actual(s) → p⇩1)›
84 using "∀E" by blast
85 moreover AOT_have ‹□s ⊨ p⇩1›
86 using ξ "con-dis-i-e:2:a" "intro-elim:3:a" "lem2:1" by blast
87 ultimately AOT_have 1: ‹□(Actual(s) → p⇩1)›
88 using "vdash-properties:10" by blast
89 AOT_have ‹□s ⊨ p⇩2 → □(Actual(s) → p⇩2)›
90 using 0 "∀E" by blast
91 moreover AOT_have ‹□s ⊨ p⇩2›
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) → p⇩2)›
95 using "vdash-properties:10" by blast
96 AOT_hence ‹□(Actual(s) → (p⇩1 & p⇩2))›
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) ⇒ (p⇩1 & p⇩2)›
100 by (simp add: "nec-impl-p:1.≡⇩d⇩fI")
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 "≡⇩d⇩fE" "&E" "sit-clo" by blast
116 AOT_have ξ: ‹¬∃p(s ⊨ p & s ⊨ ¬p)›
117 using 1 by (metis (no_types, lifting) "≡⇩d⇩fE" "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 p⇩1 where ‹s ⊨ p⇩1 & ¬p⇩1›
147 using "∃E" by meson
148 AOT_hence ‹¬s ⊨ ¬p⇩1›
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) ⇒ ¬p⇩1) → s ⊨ ¬p⇩1)›
153 using θ "log-prop-prop:2" "rule-ui:1" by blast
154 ultimately AOT_have ‹¬(Actual(s) ⇒ ¬p⇩1)›
155 using "modus-tollens:1" by blast
156 AOT_hence ‹¬□(Actual(s) → ¬p⇩1)›
157 by (AOT_subst_def (reverse) "nec-impl-p:1")
158 AOT_hence 2: ‹◇¬(Actual(s) → ¬p⇩1)›
159 using "KBasic:11" "≡E"(1) by blast
160 AOT_have ‹◇(Actual(s) & ¬¬p⇩1)›
161 proof (AOT_subst ‹Actual(s) & ¬¬p⇩1› ‹¬(Actual(s) → ¬p⇩1)›)
162 AOT_modally_strict {
163 AOT_show ‹Actual(s) & ¬¬p⇩1 ≡ ¬(Actual(s) → ¬p⇩1)›
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) → ¬p⇩1)›
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 "≡⇩d⇩fI" "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 "≡⇩d⇩fE" "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 q⇩1 where ‹□q⇩1›
198 by (metis "∃I"(1) "instantiation" "log-prop-prop:2" RN)
199 AOT_hence ‹s ⊨ q⇩1›
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 "≡⇩d⇩fE" "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 "≡⇩d⇩fI" "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
229 AOT_have C: ‹PossibleWorld(w)›
230 by (simp add: PossibleWorld.restricted_var_condition)
231 AOT_hence C2: ‹◇∀p(w ⊨ p ≡ p)›
232 using "≡⇩d⇩fE" "con-dis-i-e:2:b" "world:1" by blast
233
234
235 {
236 fix q
237 AOT_assume 1: ‹Actual(w) ⇒ q›
238
239
240 AOT_have 2: ‹□(Actual(w) → q)›
241 using 1 "≡⇩d⇩fE" "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
250 AOT_hence ‹◇w ⊨ q›
251 using C "T◇" "→E" C2 "K◇" by blast
252
253
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 "≡⇩d⇩fE" "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!: "≡⇩d⇩fI"[OF "sit-clo"])
263qed
264
265
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 =⇩d⇩f ❙ι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 "≡⇩d⇩fE" "con-dis-i-e:2:a" "pext-lem:4" "true-in-s" by blast
343
344
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
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.≡⇩d⇩fE.&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 "≡⇩d⇩fE" "&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⇧⋆ =⇩d⇩f ❙ι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 "≡⇩d⇩fE" "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" "=⇩d⇩fI"(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 "≡⇩d⇩fI"] "&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.≡⇩d⇩fE.&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 "≡⇩d⇩fI" "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
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.≡⇩d⇩fE.&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 p⇩1 where p⇩1_prop: ‹s⇧⋆ ⊨ p⇩1 & ¬w ⊨ p⇩1›
645 using "∃E"[rotated] by meson
646 AOT_hence 2: ‹¬(w ⊨ p⇩1)›
647 using "con-dis-i-e:2:b" by blast
648 AOT_have ‹Actual(s) ⇒ p⇩1›
649 using p⇩1_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 ⊨ p⇩1›
652 using "poss-sit-part-w:3"[THEN "≡E"(2), THEN "PossibleWorld.∀E"]
653 by blast
654 AOT_hence 3: ‹w ⊨ p⇩1›
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 "≡⇩d⇩fE" "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 "≡⇩d⇩fI" "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 "≡⇩d⇩fI" "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) ≡⇩d⇩f Consistent(s) & ModallyClosed(s)›
837
838AOT_theorem "possibilites:2": ‹Possibility(w)›
839 apply(safe intro!: "≡⇩d⇩fI"[OF "possibilities:1"] "&I" "world-cons:1" "world-closed:1")
840 using "≡⇩d⇩fE" "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 "≡⇩d⇩fE"])
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!: "≡⇩d⇩fE"[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" "≡⇩d⇩fE" "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" "≡⇩d⇩fE" "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.≡⇩d⇩fE.&E_1" "possibilities:1.≡⇩d⇩fE.&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 ≡⇩d⇩f s ⊴ s' ›
922
923
924
925AOT_theorem "possibilitites:7(a)": ‹s ⊵ s›
926 by (meson "≡⇩d⇩fI" "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" "≡⇩d⇩fE" "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 "≡⇩d⇩fE" "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" "≡⇩d⇩fE" "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 "≡⇩d⇩fE" "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"≡⇩d⇩fE" "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 "≡⇩d⇩fI" "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 "≡⇩d⇩fE" "con-dis-i-e:2:b" "possibilities:5" by blast
967 AOT_hence ‹∀p(𝔰 ⊨ p → 𝔰' ⊨ p)›
968 using "≡⇩d⇩fE" "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⇩□ =⇩d⇩f ❙ιs∀p(s ⊨ p ≡ □p)›
975
976
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⇩□ = ❙ιs∀p(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 "≡⇩d⇩fE" "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 "≡⇩d⇩fI"] "&I" absolute_necessity_situation)
1042 qed
1043
1044AOT_theorem "possibilities:11": ‹Possibility(s⇩□)›
1045proof(safe intro!: "≡⇩d⇩fI"[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 q⇩1 where ‹s⇩□ ⊨ q⇩1 & s⇩□ ⊨ ¬q⇩1›
1054 using "∃E"[rotated] by blast
1055 AOT_hence ‹□q⇩1› and ‹□¬q⇩1›
1056 using "&E" "intro-elim:3:a" "log-prop-prop:2" "rule-ui:1" absolute_necessity_matrix by blast+
1057 AOT_hence ‹q⇩1 & ¬q⇩1›
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!: "≡⇩d⇩fI"[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 "≡⇩d⇩fE" "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 p⇩1 where ‹◇¬(s⇩□ ⊨ p⇩1 → p⇩1)›
1091 using "∃E"[rotated] by blast
1092 AOT_hence 1: ‹◇(s⇩□ ⊨ p⇩1 & ¬p⇩1)›
1093 apply (AOT_subst ‹s⇩□ ⊨ p⇩1 & ¬p⇩1› ‹¬(s⇩□ ⊨ p⇩1 → p⇩1)›)
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⇩□ ⊨ p⇩1› and 3: ‹◇¬p⇩1›
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: ‹¬□p⇩1›
1100 using 3 "KBasic:11" "intro-elim:3:b" by blast
1101 AOT_have ‹□(s⇩□ ⊨ p⇩1 → □p⇩1)›
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 ‹◇□p⇩1›
1105 using 2
1106 using "K◇" "vdash-properties:10" by blast
1107 AOT_hence ‹□p⇩1›
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" "≡⇩d⇩fE" "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 q⇩1 where ‹¬(s ⊨ q⇩1 ≡ s⇩□ ⊨ q⇩1)›
1136 using "∃E"[rotated] by blast
1137 AOT_hence ‹(s ⊨ q⇩1 & ¬s⇩□ ⊨ q⇩1) ∨ (s⇩□ ⊨ q⇩1 & ¬s ⊨ q⇩1)›
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 ⊨ q⇩1 & ¬s⇩□ ⊨ q⇩1›
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 "≡⇩d⇩fE" "con-dis-i-e:2:b" "sit-part-whole" by blast
1146 AOT_hence ‹s⇩□ ⊨ q⇩1›
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⇩□ ⊨ q⇩1 & ¬s ⊨ q⇩1›
1152 by (metis "con-dis-i-e:4:c" "instantiation" "raa-cor:1")
1153 AOT_hence 2: ‹□q⇩1›
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 ⊨ q⇩1›
1159 using 2 "possibilities:4" "rule-ui:2[const_var]" "vdash-properties:6" by blast
1160 AOT_thus ‹s ⊨ q⇩1 & ¬s ⊨ q⇩1›
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 "≡⇩d⇩fI"]
1183 "con-dis-i-e:1" Possibilities_are_Situations
1184 absolute_necessity_situation
1185 by presburger
1186 AOT_thus ‹𝔰 ⊵ s⇩□›
1187 by (meson "≡⇩d⇩fE" "≡⇩d⇩fI" "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.≡⇩d⇩fE.&E_2.&E_1" "routley-star:5.≡⇩d⇩fE.&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 "≡⇩d⇩fE"] "&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.≡⇩d⇩fE.&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.≡⇩d⇩fI" Possibilities_are_Situations sit)
1260 AOT_thus ‹𝔰⇧+p⇧⋆ ⊵ 𝔰›
1261 by (simp add: "con-dis-i-e:1" "possibilities:5.≡⇩d⇩fI" "sit-part-whole.≡⇩d⇩fE.&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.≡⇩d⇩fE.&E_2.∀E_1.→E"
1265 "situations:3.→E" "true-in-s.≡⇩d⇩fE.&E_1" Possibilities_are_Situations)
1266 AOT_show 1: ‹Possibility(𝔰⇧+p⇧⋆)›
1267 proof(safe intro!: "possibilities:1"[THEN "≡⇩d⇩fI"] "&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.≡⇩d⇩fE.&E_2.&E_2"
1293 "sit-clo.≡⇩d⇩fE.&E_2.∀E_1.→E" AOT_restricted_type.ψ
1294 Possibilities.AOT_restricted_type_axioms)
1295 moreover AOT_have ‹¬𝔰 ⊨ ¬p›
1296 using "routley-star:5.≡⇩d⇩fE.&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.≡⇩d⇩fE.&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.≡⇩d⇩fE.&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.≡⇩d⇩fE.&E_1"
1325 "routley-star:5.≡⇩d⇩fE.&E_2.&E_2" "routley-star:5.≡⇩d⇩fI")
1326 moreover {
1327 AOT_assume ‹𝔰 ⊨ ¬p›
1328 AOT_hence ‹∀p(p & ¬p)›
1329 by (smt (verit) "1" "raa-cor:3" "routley-star:5.≡⇩d⇩fE.&E_2.&E_2")
1330 }
1331 AOT_find_theorems item: 529
1332 moreover {
1333 AOT_have ‹ModallyClosed(𝔰)›
1334 by (simp add: "possibilities:1.≡⇩d⇩fE.&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.≡⇩d⇩fI"
1345 "useful-tautologies:1" RN)
1346 qed
1347 AOT_hence ‹∀p(p & ¬p)›
1348 using "1" "raa-cor:4" "routley-star:5.≡⇩d⇩fE.&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.≡⇩d⇩fE.&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.≡⇩d⇩fE.&E_2"
1379 "sit-part-whole.≡⇩d⇩fE.&E_2.∀E_1.→E" a by blast
1380 AOT_have ‹Consistent(𝔰⇩1)›
1381 using "possibilities:1.≡⇩d⇩fE.&E_2.&E_1" Possibilities.restricted_var_condition by auto
1382 AOT_hence ‹¬∃p (𝔰⇩1 ⊨ p & 𝔰⇩1 ⊨ ¬p)›
1383 by (simp add: "cons.≡⇩d⇩fE.&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.≡⇩d⇩fI" 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.≡⇩d⇩fE.&E_1"
1408 "possibilities:15[b]" "situations:3.→E")
1409 AOT_hence ‹¬∃p (𝔰⇩3 ⊨ p & 𝔰⇩3 ⊨ ¬p)›
1410 by (simp add: "cons.≡⇩d⇩fE.&E_2")
1411 moreover AOT_have ‹∃p (𝔰⇩3 ⊨ p & 𝔰⇩3 ⊨ ¬p)›
1412 by (meson "2" "3" "con-dis-i-e:2:b" "con-dis-taut:5.→E.→E" "existential:2[const_var]")
1413 ultimately AOT_have ‹p & ¬p›
1414 using "raa-cor:3" by blast
1415 }
1416 ultimately AOT_show ‹p & ¬p›
1417 using "raa-cor:1" by blast
1418 qed
1419qed
1420
1421AOT_theorem "possibilities:18": ‹𝔰 ⊨ ¬p ≡ ∀𝔰'(𝔰' ⊵ 𝔰 → ¬𝔰' ⊨ p)›
1422proof(safe intro!: "≡I" "→I" "Possibilities.GEN")
1423 fix 𝔰'
1424 AOT_assume 0: ‹𝔰 ⊨ ¬p›
1425 AOT_assume ‹𝔰' ⊵ 𝔰›
1426 AOT_hence 1: ‹𝔰 ⊴ 𝔰'›
1427 using "possibilities:5.≡⇩d⇩fE.&E_2" by auto
1428 AOT_hence ‹∀p(𝔰 ⊨ p → 𝔰' ⊨ p)›
1429 by (simp add: "deduction-theorem" "log-prop-prop:2"
1430 "sit-part-whole.≡⇩d⇩fE.&E_2.∀E_1.→E" "universal-cor")
1431 AOT_hence 2: ‹𝔰' ⊨ ¬p›
1432 using "0" "1" "log-prop-prop:2" "sit-part-whole.≡⇩d⇩fE.&E_2.∀E_1.→E" by auto
1433 AOT_show ‹¬𝔰' ⊨ p›
1434 proof(rule "raa-cor:2")
1435 AOT_assume ‹𝔰' ⊨ p›
1436 AOT_hence ‹∃q(𝔰' ⊨ q & 𝔰' ⊨ ¬q)›
1437 by (meson "2" "con-dis-taut:5.→E.→E" "existential:2[const_var]")
1438 AOT_hence ‹¬Consistent(𝔰')›
1439 using "cons.≡⇩d⇩fE.&E_2" "raa-cor:3" by blast
1440 moreover AOT_have ‹Consistent(𝔰')›
1441 by (simp add: "pos-cons-sit:1.unconstrain_s.∀E_1.→E.→E" "pos.≡⇩d⇩fE.&E_1"
1442 "possibilities:15[b]" "situations:3.→E")
1443 ultimately AOT_show ‹p & ¬p›
1444 using "raa-cor:3" by blast
1445 qed
1446next
1447 AOT_assume 1: ‹∀𝔰'(𝔰' ⊵ 𝔰 → ¬𝔰' ⊨ p)›
1448 AOT_show ‹𝔰 ⊨ ¬p›
1449 proof(rule "raa-cor:1")
1450 AOT_assume 2: ‹¬𝔰 ⊨ ¬p›
1451 AOT_have ‹𝔰 ⊵ 𝔰›
1452 using "cqt:2"(1) "possibilitites:7(a).unconstrain_s.∀E_1.→E"
1453 Possibilities_are_Situations by blast
1454 AOT_hence ‹¬𝔰 ⊨ p›
1455 using "1" "rule-ui:3" "vdash-properties:10" Possibilities.restricted_var_condition by blast
1456 AOT_hence ‹GapOn(𝔰, p)›
1457 by (simp add: "2" "con-dis-taut:5.→E.→E" "routley-star:5.≡⇩d⇩fI" Possibilities_are_Situations)
1458 AOT_hence ‹∃𝔰'(𝔰' ⊵ 𝔰 & 𝔰' ⊨ p)›
1459 using "con-dis-taut:1" "oth-class-taut:4:a.→E.→E.→E" "possibilities:16" by blast
1460 then AOT_obtain 𝔰⇩1 where 3: ‹𝔰⇩1 ⊵ 𝔰 & 𝔰⇩1 ⊨ p›
1461 using "Possibilities.∃E" by meson
1462 AOT_hence ‹¬𝔰⇩1 ⊨ p›
1463 using 1
1464 using "con-dis-i-e:2:a" "ded-thm-cor:4.→E" "rule-ui:3" Possibilities.ψ by blast
1465 AOT_thus ‹p & ¬p›
1466 using "3" "con-dis-i-e:2:b" "raa-cor:3" by blast
1467 qed
1468qed
1469
1470AOT_theorem "possibilities:19": ‹𝔰 ⊨ (p & q) ≡ (𝔰 ⊨ p & 𝔰 ⊨ q)›
1471proof(safe intro!: "≡I" "→I" "&I")
1472 AOT_assume ‹𝔰 ⊨ (p & q)›
1473 moreover AOT_have ‹(p & q) ⇒ p›
1474 by (simp add: "con-dis-taut:1" "nec-impl-p:1.≡⇩d⇩fI" RN)
1475 ultimately AOT_show ‹𝔰 ⊨ p›
1476 by (meson "con-dis-taut:5.→E.→E" "cqt:2"(1) "log-prop-prop:2"
1477 "modal-clos-facts:1.unconstrain_s.∀E_1.→E.→E.∀E_1.∀E_1.→E"
1478 "possibilities:1.≡⇩d⇩fE.&E_2.&E_2" "true-in-s.≡⇩d⇩fE.&E_1" Possibilities.ψ)
1479next
1480 AOT_assume ‹𝔰 ⊨ (p & q)›
1481 moreover AOT_have ‹(p & q) ⇒ q›
1482 using "con-dis-taut:2" "nec-impl-p:1.≡⇩d⇩fI" RN by blast
1483 ultimately AOT_show ‹𝔰 ⊨ q›
1484 by (meson "con-dis-taut:5.→E.→E" "cqt:2"(1) "log-prop-prop:2"
1485 "modal-clos-facts:1.unconstrain_s.∀E_1.→E.→E.∀E_1.∀E_1.→E"
1486 "possibilities:1.≡⇩d⇩fE.&E_2.&E_2" "true-in-s.≡⇩d⇩fE.&E_1" Possibilities.ψ)
1487next
1488 AOT_assume ‹𝔰 ⊨ p & 𝔰 ⊨ q›
1489 moreover AOT_have ‹(p & q) ⇒ (p & q)›
1490 using "log-prop-prop:2" "nec-impl-p:3[rec].unvarify_p.∀E_1" by auto
1491 ultimately AOT_show ‹𝔰 ⊨ (p & q)›
1492 by (meson "con-dis-i-e:1" "cqt:2"(1) "log-prop-prop:2"
1493 "modal-clos-facts:1b.unconstrain_s.∀E_1.→E.→E.∀E_1.∀E_1.∀E_1.→E"
1494 "possibilities:1.≡⇩d⇩fE.&E_2.&E_2" AOT_restricted_type.ψ
1495 Possibilities.AOT_restricted_type_axioms Possibilities_are_Situations)
1496qed
1497
1498AOT_theorem "possibilities:20": ‹◇p ≡ ∃𝔰(𝔰 ⊨ p)›
1499proof(safe intro!: "≡I" "→I")
1500 AOT_assume ‹◇p›
1501 AOT_hence ‹∃w w ⊨ p›
1502 using "fund:3.unvarify_p.∀E_1.≡E_2" "log-prop-prop:2" "reductio-aa:1" by blast
1503 then AOT_obtain w where ‹w ⊨ p›
1504 by (metis "PossibleWorld.∃E")
1505 AOT_thus ‹∃𝔰(𝔰 ⊨ p)›
1506 by (meson "con-dis-taut:5.→E.→E" "existential:2[const_var]" "possibilites:2")
1507next
1508 AOT_assume ‹∃𝔰(𝔰 ⊨ p)›
1509 then AOT_obtain 𝔰 where 1: ‹𝔰 ⊨ p›
1510 by (metis "Possibilities.∃E")
1511 AOT_have ‹Possible(𝔰)›
1512 by (simp add: "possibilities:15[b]")
1513 AOT_hence ‹∃w 𝔰 ⊴ w›
1514 by (meson "∃I"(2) "pos.≡⇩d⇩fE.&E_1" "situations:3.→E"
1515 "poss-sit-part-w:1.unconstrain_s.∀E_1.→E.≡E_1.∃E'")
1516 then AOT_obtain w where ‹𝔰 ⊴ w›
1517 using PossibleWorld.instantiation by blast
1518 AOT_hence ‹w ⊨ p›
1519 using 1 by (simp add: "log-prop-prop:2" "sit-part-whole.≡⇩d⇩fE.&E_2.∀E_1.→E")
1520 AOT_thus ‹◇p›
1521 by (metis (no_types, lifting) "con-dis-taut:5.→E.→E" "existential:2[const_var]"
1522 "fund:1" "intro-elim:3:b" PossibleWorld.restricted_var_condition)
1523qed
1524
1525AOT_theorem "possibilities:21": ‹□p ≡ ∀𝔰(𝔰 ⊨ p)›
1526proof(safe intro!: "≡I" "→I" Possibilities.GEN)
1527 fix 𝔰
1528 AOT_assume ‹□p›
1529 AOT_thus ‹𝔰 ⊨ p›
1530 by (simp add: "cqt:2"(1) "possibilities:4.unvarify_p.∀E_1.→E.∀E_1.→E" Possibilities.ψ)
1531next
1532 AOT_assume ‹∀𝔰(𝔰 ⊨ p)›
1533 AOT_hence ‹s⇩□ ⊨ p›
1534 using "Possibilities.res-var:3" "possibilities:11" "rule-ui:1" "vdash-properties:10" by blast
1535 AOT_thus ‹□p›
1536 by (simp add: "absolute_necessity_matrix.∀E_1.≡E_1" "cqt:2"(1))
1537qed
1538
1539end
1540