Theory AOT_PossibleWorlds
1
2theory AOT_PossibleWorlds
3 imports AOT_PLM AOT_BasicLogicalObjects AOT_RestrictedVariables
4begin
5
6
7section‹Possible Worlds›
8
9AOT_define Situation :: ‹τ ⇒ φ› (‹Situation'(_')›)
10 "situations:1": ‹Situation(x) ≡⇩d⇩f A!x & ∀F (x[F] → Propositional([F]))›
11
12
13lemmas "situations" = "situations:1"
14
15AOT_theorem "situations:2": ‹∃x Situation(x)›
16proof -
17 AOT_have ‹∃x (A!x & ∀F (x[F] ≡ F = [λy [R]ab]))›
18 using "A-objects" "vdash-properties:1[2]" by auto
19 then AOT_obtain c where c_prop: ‹A!c & ∀F (c[F] ≡ F = [λy [R]ab])›
20 using "∃E" by meson
21 AOT_have ‹Situation(c)›
22 proof(safe intro!: "≡⇩d⇩fI"[OF "situations:1"] "&I" GEN "→I")
23 AOT_show ‹A!c›
24 using c_prop "&E" by blast
25 next
26 fix F
27 AOT_assume ‹c[F]›
28 AOT_hence F_eq: ‹F = [λy [R]ab]›
29 using "con-dis-i-e:2:b" "intro-elim:3:a" "rule-ui:3" c_prop by blast
30 AOT_find_theorems ‹Propositional([Π])›
31 AOT_show ‹Propositional([F])›
32 proof(rule "prop-prop1"[THEN "≡⇩d⇩fI"])
33 AOT_show "∃p F = [λy p]"
34 using F_eq "∃I"(1)
35 using "log-prop-prop:2" by fastforce
36 qed
37 qed
38 AOT_thus ‹∃x Situation(x)›
39 using "∃I" by blast
40qed
41
42AOT_theorem "situations:3": ‹Situation(κ) → κ↓›
43proof (rule "→I")
44 AOT_assume ‹Situation(κ)›
45 AOT_hence ‹A!κ› by (metis "≡⇩d⇩fE" "&E"(1) "situations:1")
46 AOT_thus ‹κ↓› by (metis "russell-axiom[exe,1].ψ_denotes_asm")
47qed
48
49AOT_theorem "T-sit": ‹TruthValue(x) → Situation(x)›
50proof(rule "→I")
51 AOT_assume ‹TruthValue(x)›
52 AOT_hence ‹∃p TruthValueOf(x,p)›
53 using "T-value"[THEN "≡⇩d⇩fE"] by blast
54 then AOT_obtain p where ‹TruthValueOf(x,p)› using "∃E"[rotated] by blast
55 AOT_hence θ: ‹A!x & ∀F (x[F] ≡ ∃q((q ≡ p) & F = [λy q]))›
56 using "tv-p"[THEN "≡⇩d⇩fE"] by blast
57 AOT_show ‹Situation(x)›
58 proof(rule "situations:1"[THEN "≡⇩d⇩fI"]; safe intro!: "&I" GEN "→I" θ[THEN "&E"(1)])
59 fix F
60 AOT_assume ‹x[F]›
61 AOT_hence ‹∃q((q ≡ p) & F = [λy q])›
62 using θ[THEN "&E"(2), THEN "∀E"(2)[where β=F], THEN "≡E"(1)] by argo
63 then AOT_obtain q where ‹(q ≡ p) & F = [λy q]› using "∃E"[rotated] by blast
64 AOT_hence ‹∃p F = [λy p]› using "&E"(2) "∃I"(2) by metis
65 AOT_thus ‹Propositional([F])›
66 by (metis "≡⇩d⇩fI" "prop-prop1")
67 qed
68qed
69
70AOT_theorem "possit-sit:1": ‹Situation(x) ≡ □Situation(x)›
71proof(rule "≡I"; rule "→I")
72 AOT_assume ‹Situation(x)›
73 AOT_hence 0: ‹A!x & ∀F (x[F] → Propositional([F]))›
74 using "situations:1"[THEN "≡⇩d⇩fE"] by blast
75 AOT_have 1: ‹□(A!x & ∀F (x[F] → Propositional([F])))›
76 proof(rule "KBasic:3"[THEN "≡E"(2)]; rule "&I")
77 AOT_show ‹□A!x› using 0[THEN "&E"(1)] by (metis "oa-facts:2"[THEN "→E"])
78 next
79 AOT_have ‹∀F (x[F] → Propositional([F])) → □∀F (x[F] → Propositional([F]))›
80 by (AOT_subst ‹Propositional([F])› ‹∃p (F = [λy p])› for: F :: ‹<κ>›)
81 (auto simp: "prop-prop1" "≡Df" "enc-prop-nec:2")
82 AOT_thus ‹□∀F (x[F] → Propositional([F]))›
83 using 0[THEN "&E"(2)] "→E" by blast
84 qed
85 AOT_show ‹□Situation(x)›
86 by (AOT_subst ‹Situation(x)› ‹A!x & ∀F (x[F] → Propositional([F]))›)
87 (auto simp: 1 "≡Df" "situations:1")
88next
89 AOT_show ‹Situation(x)› if ‹□Situation(x)›
90 using "qml:2"[axiom_inst, THEN "→E", OF that].
91qed
92
93AOT_theorem "possit-sit:2": ‹◇Situation(x) ≡ Situation(x)›
94 using "possit-sit:1"
95 by (metis "RE◇" "S5Basic:2" "≡E"(1) "≡E"(5) "Commutativity of ≡")
96
97AOT_theorem "possit-sit:3": ‹◇Situation(x) ≡ □Situation(x)›
98 using "possit-sit:1" "possit-sit:2" by (meson "≡E"(5))
99
100AOT_theorem "possit-sit:4": ‹❙𝒜Situation(x) ≡ Situation(x)›
101 by (meson "Act-Basic:5" "Act-Sub:2" "RA[2]" "≡E"(1) "≡E"(6) "possit-sit:2")
102
103AOT_theorem "possit-sit:5": ‹Situation(∘p)›
104proof (safe intro!: "situations:1"[THEN "≡⇩d⇩fI"] "&I" GEN "→I" "prop-prop1"[THEN "≡⇩d⇩fI"])
105 AOT_have ‹∃F ∘p[F]›
106 using "tv-id:2"[THEN "prop-enc"[THEN "≡⇩d⇩fE"], THEN "&E"(2)]
107 "existential:1" "prop-prop2:2" by blast
108 AOT_thus ‹A!∘p›
109 by (safe intro!: "encoders-are-abstract"[unvarify x, THEN "→E"]
110 "t=t-proper:2"[THEN "→E", OF "ext-p-tv:3"])
111next
112 fix F
113 AOT_assume ‹∘p[F]›
114 AOT_hence ‹❙ιx(A!x & ∀F (x[F] ≡ ∃q ((q ≡ p) & F = [λy q])))[F]›
115 using "tv-id:1" "rule=E" by fast
116 AOT_hence ‹❙𝒜∃q ((q ≡ p) & F = [λy q])›
117 using "≡E"(1) "desc-nec-encode:1" by fast
118 AOT_hence ‹∃q ❙𝒜((q ≡ p) & F = [λy q])›
119 by (metis "Act-Basic:10" "≡E"(1))
120 then AOT_obtain q where ‹❙𝒜((q ≡ p) & F = [λy q])› using "∃E"[rotated] by blast
121 AOT_hence ‹❙𝒜F = [λy q]› by (metis "Act-Basic:2" "con-dis-i-e:2:b" "intro-elim:3:a")
122 AOT_hence ‹F = [λy q]›
123 using "id-act:1"[unvarify β, THEN "≡E"(2)] by (metis "prop-prop2:2")
124 AOT_thus ‹∃p F = [λy p]›
125 using "∃I" by fast
126qed
127
128AOT_theorem "possit-sit:6": ‹Situation(⊤)›
129proof -
130 AOT_have true_def: ‹❙⊢⇩□ ⊤ = ❙ιx (A!x & ∀F (x[F] ≡ ∃p(p & F = [λy p])))›
131 by (simp add: "A-descriptions" "rule-id-df:1[zero]" "the-true:1")
132 AOT_hence true_den: ‹❙⊢⇩□ ⊤↓›
133 using "t=t-proper:1" "vdash-properties:6" by blast
134 AOT_have ‹❙𝒜TruthValue(⊤)›
135 using "actual-desc:2"[unvarify x, OF true_den, THEN "→E", OF true_def]
136 using "TV-lem2:1"[unvarify x, OF true_den, THEN "RA[2]",
137 THEN "act-cond"[THEN "→E"], THEN "→E"]
138 by blast
139 AOT_hence ‹❙𝒜Situation(⊤)›
140 using "T-sit"[unvarify x, OF true_den, THEN "RA[2]",
141 THEN "act-cond"[THEN "→E"], THEN "→E"] by blast
142 AOT_thus ‹Situation(⊤)›
143 using "possit-sit:4"[unvarify x, OF true_den, THEN "≡E"(1)] by blast
144qed
145
146AOT_theorem "possit-sit:7": ‹Situation(⊥)›
147proof -
148 AOT_have true_def: ‹❙⊢⇩□ ⊥ = ❙ιx (A!x & ∀F (x[F] ≡ ∃p(¬p & F = [λy p])))›
149 by (simp add: "A-descriptions" "rule-id-df:1[zero]" "the-true:2")
150 AOT_hence true_den: ‹❙⊢⇩□ ⊥↓›
151 using "t=t-proper:1" "vdash-properties:6" by blast
152 AOT_have ‹❙𝒜TruthValue(⊥)›
153 using "actual-desc:2"[unvarify x, OF true_den, THEN "→E", OF true_def]
154 using "TV-lem2:2"[unvarify x, OF true_den, THEN "RA[2]",
155 THEN "act-cond"[THEN "→E"], THEN "→E"]
156 by blast
157 AOT_hence ‹❙𝒜Situation(⊥)›
158 using "T-sit"[unvarify x, OF true_den, THEN "RA[2]",
159 THEN "act-cond"[THEN "→E"], THEN "→E"] by blast
160 AOT_thus ‹Situation(⊥)›
161 using "possit-sit:4"[unvarify x, OF true_den, THEN "≡E"(1)] by blast
162qed
163
164AOT_register_rigid_restricted_type
165 Situation: ‹Situation(κ)›
166proof
167 AOT_modally_strict {
168 AOT_show ‹∃x Situation(x)›
169 using "situations:2".
170 }
171next
172 AOT_modally_strict {
173 AOT_show ‹Situation(κ) → κ↓› for κ
174 using "situations:3".
175 }
176next
177 AOT_modally_strict {
178 AOT_show ‹∀α(Situation(α) → □Situation(α))›
179 using "possit-sit:1"[THEN "conventions:3"[THEN "≡⇩d⇩fE"],
180 THEN "&E"(1)] GEN by fast
181 }
182qed
183
184AOT_register_variable_names
185 Situation: s
186
187AOT_define TruthInSituation :: ‹τ ⇒ φ ⇒ φ› ("(_ ⊨/ _)" [100, 40] 100)
188 "true-in-s": ‹s ⊨ p ≡⇩d⇩f s❙Σp›
189
190notepad
191begin
192
193 fix x p q
194 have ‹«x ⊨ p → q» = «(x ⊨ p) → q»›
195 by simp
196 have ‹«x ⊨ p & q» = «(x ⊨ p) & q»›
197 by simp
198 have ‹«x ⊨ ¬p» = «x ⊨ (¬p)»›
199 by simp
200 have ‹«x ⊨ □p» = «x ⊨ (□p)»›
201 by simp
202 have ‹«x ⊨ ❙𝒜p» = «x ⊨ (❙𝒜p)»›
203 by simp
204 have ‹«□x ⊨ p» = «□(x ⊨ p)»›
205 by simp
206 have ‹«¬x ⊨ p» = «¬(x ⊨ p)»›
207 by simp
208end
209
210
211AOT_theorem lem1: ‹Situation(x) → (x ⊨ p ≡ x[λy p])›
212proof (rule "→I"; rule "≡I"; rule "→I")
213 AOT_assume ‹Situation(x)›
214 AOT_assume ‹x ⊨ p›
215 AOT_hence ‹x❙Σp›
216 using "true-in-s"[THEN "≡⇩d⇩fE"] "&E" by blast
217 AOT_thus ‹x[λy p]› using "prop-enc"[THEN "≡⇩d⇩fE"] "&E" by blast
218next
219 AOT_assume 1: ‹Situation(x)›
220 AOT_assume ‹x[λy p]›
221 AOT_hence ‹x❙Σp›
222 using "prop-enc"[THEN "≡⇩d⇩fI", OF "&I", OF "cqt:2"(1)] by blast
223 AOT_thus ‹x ⊨ p›
224 using "true-in-s"[THEN "≡⇩d⇩fI"] 1 "&I" by blast
225qed
226
227AOT_theorem "lem2:1": ‹s ⊨ p ≡ □s ⊨ p›
228proof -
229 AOT_have sit: ‹Situation(s)›
230 by (simp add: Situation.ψ)
231 AOT_have ‹s ⊨ p ≡ s[λy p]›
232 using lem1[THEN "→E", OF sit] by blast
233 also AOT_have ‹… ≡ □s[λy p]›
234 by (rule "en-eq:2[1]"[unvarify F]) "cqt:2[lambda]"
235 also AOT_have ‹… ≡ □s ⊨ p›
236 using lem1[THEN RM, THEN "→E", OF "possit-sit:1"[THEN "≡E"(1), OF sit]]
237 by (metis "KBasic:6" "≡E"(2) "Commutativity of ≡" "→E")
238 finally show ?thesis.
239qed
240
241AOT_theorem "lem2:2": ‹◇s ⊨ p ≡ s ⊨ p›
242proof -
243 AOT_have ‹□(s ⊨ p → □s ⊨ p)›
244 using "possit-sit:1"[THEN "≡E"(1), OF Situation.ψ]
245 "lem2:1"[THEN "conventions:3"[THEN "≡⇩d⇩fE", THEN "&E"(1)]]
246 RM[OF "→I", THEN "→E"] by blast
247 thus ?thesis by (metis "B◇" "S5Basic:13" "T◇" "≡I" "≡E"(1) "→E")
248qed
249
250AOT_theorem "lem2:3": ‹◇s ⊨ p ≡ □s ⊨ p›
251 using "lem2:1" "lem2:2" by (metis "≡E"(5))
252
253AOT_theorem "lem2:4": ‹❙𝒜(s ⊨ p) ≡ s ⊨ p›
254proof -
255 AOT_have ‹□(s ⊨ p → □s ⊨ p)›
256 using "possit-sit:1"[THEN "≡E"(1), OF Situation.ψ]
257 "lem2:1"[THEN "conventions:3"[THEN "≡⇩d⇩fE", THEN "&E"(1)]]
258 RM[OF "→I", THEN "→E"] by blast
259 thus ?thesis
260 using "sc-eq-fur:2"[THEN "→E"] by blast
261qed
262
263AOT_theorem "lem2:5": ‹¬s ⊨ p ≡ □¬s ⊨ p›
264 by (metis "KBasic2:1" "contraposition:1[2]" "→I" "≡I" "≡E"(3) "≡E"(4) "lem2:2")
265
266AOT_theorem "sit-identity": ‹s = s' ≡ ∀p(s ⊨ p ≡ s' ⊨ p)›
267proof(rule "≡I"; rule "→I")
268 AOT_assume ‹s = s'›
269 moreover AOT_have ‹∀p(s ⊨ p ≡ s ⊨ p)›
270 by (simp add: "oth-class-taut:3:a" "universal-cor")
271 ultimately AOT_show ‹∀p(s ⊨ p ≡ s' ⊨ p)›
272 using "rule=E" by fast
273next
274 AOT_assume a: ‹∀p (s ⊨ p ≡ s' ⊨ p)›
275 AOT_show ‹s = s'›
276 proof(safe intro!: "ab-obey:1"[THEN "→E", THEN "→E"] "&I" GEN "≡I" "→I")
277 AOT_show ‹A!s› using Situation.ψ "≡⇩d⇩fE" "&E"(1) situations by blast
278 next
279 AOT_show ‹A!s'› using Situation.ψ "≡⇩d⇩fE" "&E"(1) situations by blast
280 next
281 fix F
282 AOT_assume 0: ‹s[F]›
283 AOT_hence ‹∃p (F = [λy p])›
284 using Situation.ψ[THEN situations[THEN "≡⇩d⇩fE"], THEN "&E"(2),
285 THEN "∀E"(2)[where β=F], THEN "→E"]
286 "prop-prop1"[THEN "≡⇩d⇩fE"] by blast
287 then AOT_obtain p where F_def: ‹F = [λy p]›
288 using "∃E" by metis
289 AOT_hence ‹s[λy p]›
290 using 0 "rule=E" by blast
291 AOT_hence ‹s ⊨ p›
292 using lem1[THEN "→E", OF Situation.ψ, THEN "≡E"(2)] by blast
293 AOT_hence ‹s' ⊨ p›
294 using a[THEN "∀E"(2)[where β=p], THEN "≡E"(1)] by blast
295 AOT_hence ‹s'[λy p]›
296 using lem1[THEN "→E", OF Situation.ψ, THEN "≡E"(1)] by blast
297 AOT_thus ‹s'[F]›
298 using F_def[symmetric] "rule=E" by blast
299 next
300 fix F
301 AOT_assume 0: ‹s'[F]›
302 AOT_hence ‹∃p (F = [λy p])›
303 using Situation.ψ[THEN situations[THEN "≡⇩d⇩fE"], THEN "&E"(2),
304 THEN "∀E"(2)[where β=F], THEN "→E"]
305 "prop-prop1"[THEN "≡⇩d⇩fE"] by blast
306 then AOT_obtain p where F_def: ‹F = [λy p]›
307 using "∃E" by metis
308 AOT_hence ‹s'[λy p]›
309 using 0 "rule=E" by blast
310 AOT_hence ‹s' ⊨ p›
311 using lem1[THEN "→E", OF Situation.ψ, THEN "≡E"(2)] by blast
312 AOT_hence ‹s ⊨ p›
313 using a[THEN "∀E"(2)[where β=p], THEN "≡E"(2)] by blast
314 AOT_hence ‹s[λy p]›
315 using lem1[THEN "→E", OF Situation.ψ, THEN "≡E"(1)] by blast
316 AOT_thus ‹s[F]›
317 using F_def[symmetric] "rule=E" by blast
318 qed
319qed
320
321AOT_define PartOfSituation :: ‹τ ⇒ τ ⇒ φ› (infixl ‹⊴› 80)
322 "sit-part-whole": ‹s ⊴ s' ≡⇩d⇩f ∀p (s ⊨ p → s' ⊨ p)›
323
324AOT_theorem "part:1": ‹s ⊴ s›
325 by (rule "sit-part-whole"[THEN "≡⇩d⇩fI"])
326 (safe intro!: "&I" Situation.ψ GEN "→I")
327
328AOT_theorem "part:2": ‹s ⊴ s' & s ≠ s' → ¬(s' ⊴ s)›
329proof(rule "→I"; frule "&E"(1); drule "&E"(2); rule "raa-cor:2")
330 AOT_assume 0: ‹s ⊴ s'›
331 AOT_hence a: ‹s ⊨ p → s' ⊨ p› for p
332 using "∀E"(2) "sit-part-whole"[THEN "≡⇩d⇩fE"] "&E" by blast
333 AOT_assume ‹s' ⊴ s›
334 AOT_hence b: ‹s' ⊨ p → s ⊨ p› for p
335 using "∀E"(2) "sit-part-whole"[THEN "≡⇩d⇩fE"] "&E" by blast
336 AOT_have ‹∀p (s ⊨ p ≡ s' ⊨ p)›
337 using a b by (simp add: "≡I" "universal-cor")
338 AOT_hence 1: ‹s = s'›
339 using "sit-identity"[THEN "≡E"(2)] by metis
340 AOT_assume ‹s ≠ s'›
341 AOT_hence ‹¬(s = s')›
342 by (metis "≡⇩d⇩fE" "=-infix")
343 AOT_thus ‹s = s' & ¬(s = s')›
344 using 1 "&I" by blast
345qed
346
347AOT_theorem "part:3": ‹s ⊴ s' & s' ⊴ s'' → s ⊴ s''›
348proof(rule "→I"; frule "&E"(1); drule "&E"(2);
349 safe intro!: "&I" GEN "→I" "sit-part-whole"[THEN "≡⇩d⇩fI"] Situation.ψ)
350 fix p
351 AOT_assume ‹s ⊨ p›
352 moreover AOT_assume ‹s ⊴ s'›
353 ultimately AOT_have ‹s' ⊨ p›
354 using "sit-part-whole"[THEN "≡⇩d⇩fE", THEN "&E"(2),
355 THEN "∀E"(2)[where β=p], THEN "→E"] by blast
356 moreover AOT_assume ‹s' ⊴ s''›
357 ultimately AOT_show ‹s'' ⊨ p›
358 using "sit-part-whole"[THEN "≡⇩d⇩fE", THEN "&E"(2),
359 THEN "∀E"(2)[where β=p], THEN "→E"] by blast
360qed
361
362AOT_theorem "sit-identity2:1": ‹s = s' ≡ s ⊴ s' & s' ⊴ s›
363proof (safe intro!: "≡I" "&I" "→I")
364 AOT_show ‹s ⊴ s'› if ‹s = s'›
365 using "rule=E" "part:1" that by blast
366next
367 AOT_show ‹s' ⊴ s› if ‹s = s'›
368 using "rule=E" "part:1" that[symmetric] by blast
369next
370 AOT_assume ‹s ⊴ s' & s' ⊴ s›
371 AOT_thus ‹s = s'› using "part:2"[THEN "→E", OF "&I"]
372 by (metis "≡⇩d⇩fI" "&E"(1) "&E"(2) "=-infix" "raa-cor:3")
373qed
374
375AOT_theorem "sit-identity2:2": ‹s = s' ≡ ∀s'' (s'' ⊴ s ≡ s'' ⊴ s')›
376proof(safe intro!: "≡I" "→I" Situation.GEN "sit-identity"[THEN "≡E"(2)]
377 GEN[where 'a=𝗈])
378 AOT_show ‹s'' ⊴ s'› if ‹s'' ⊴ s› and ‹s = s'› for s''
379 using "rule=E" that by blast
380next
381 AOT_show ‹s'' ⊴ s› if ‹s'' ⊴ s'› and ‹s = s'› for s''
382 using "rule=E" id_sym that by blast
383next
384 AOT_show ‹s' ⊨ p› if ‹s ⊨ p› and ‹∀s'' (s'' ⊴ s ≡ s'' ⊴ s')› for p
385 using "sit-part-whole"[THEN "≡⇩d⇩fE", THEN "&E"(2),
386 OF that(2)[THEN "Situation.∀E", THEN "≡E"(1), OF "part:1"],
387 THEN "∀E"(2), THEN "→E", OF that(1)].
388next
389 AOT_show ‹s ⊨ p› if ‹s' ⊨ p› and ‹∀s'' (s'' ⊴ s ≡ s'' ⊴ s')› for p
390 using "sit-part-whole"[THEN "≡⇩d⇩fE", THEN "&E"(2),
391 OF that(2)[THEN "Situation.∀E", THEN "≡E"(2), OF "part:1"],
392 THEN "∀E"(2), THEN "→E", OF that(1)].
393qed
394
395
396AOT_define Persistent :: ‹φ ⇒ φ› (‹Persistent'(_')›)
397 persistent: ‹Persistent(p) ≡⇩d⇩f ∀s (s ⊨ p → ∀s' (s ⊴ s' → s' ⊨ p))›
398
399AOT_theorem "pers-prop": ‹∀p Persistent(p)›
400 by (safe intro!: GEN[where 'a=𝗈] Situation.GEN persistent[THEN "≡⇩d⇩fI"] "→I")
401 (simp add: "sit-part-whole"[THEN "≡⇩d⇩fE", THEN "&E"(2), THEN "∀E"(2), THEN "→E"])
402
403
404AOT_theorem "sit-comp-simp": ‹∃s∀p(s ⊨ p ≡ φ{p})›
405proof -
406 AOT_have ‹∃x (A!x & ∀F(x[F] ≡ ∃p (φ{p} & F = [λy p])))›
407 using "A-objects" "vdash-properties:1[2]" by force
408 then AOT_obtain c where c_prop: ‹A!c & ∀F(c[F] ≡ ∃p (φ{p} & F = [λy p]))›
409 using "∃E" by meson
410 AOT_have sit_c: ‹Situation(c)›
411 proof(safe intro!: "≡⇩d⇩fI"[OF situations] "&I" GEN "→I")
412 AOT_show ‹A!c›
413 using c_prop "&E" by blast
414 next
415 fix F
416 AOT_assume ‹c[F]›
417 AOT_hence F_eq: ‹∃p (φ{p} & F = [λy p])›
418 using "con-dis-i-e:2:b" "intro-elim:3:a" "rule-ui:3" c_prop by blast
419 then AOT_obtain q where q_prop: ‹φ{q} & F = [λy q]›
420 using "∃E" by meson
421 AOT_show ‹Propositional([F])›
422 proof(rule "prop-prop1"[THEN "≡⇩d⇩fI"])
423 AOT_show "∃p F = [λy p]"
424 using q_prop[THEN "&E"(2)] "∃I"(1)
425 by (metis "log-prop-prop:2")
426 qed
427 qed
428 moreover AOT_have ‹∀p(c ⊨ p ≡ φ{p})›
429 proof(safe intro!: GEN "≡I" "→I")
430 fix p
431 AOT_assume ‹c ⊨ p›
432 AOT_hence 1: ‹c[λy p]›
433 using "intro-elim:3:a" "vdash-properties:10" calculation lem1 by blast
434 AOT_have ‹∃q (φ{q} & [λy p] = [λy q])›
435 by (safe intro!: c_prop[THEN "&E"(2), THEN "∀E"(1)[where τ="«[λy p]»"], THEN "≡E"(1)] 1 "cqt:2")
436 then AOT_obtain q where 2: ‹φ{q} & [λy p] = [λy q]›
437 using "∃E" by meson
438 AOT_hence ‹p = q›
439 using "con-dis-i-e:2:b" "intro-elim:3:b" "p-identity-thm2:3" by blast
440 AOT_thus ‹φ{p}›
441 using 2
442 using "con-dis-i-e:2:a" "rule=E" id_sym by blast
443 next
444 fix p
445 AOT_assume ‹φ{p}›
446 moreover AOT_have ‹[λy p] = [λy p]›
447 by (simp add: "prop-prop2:2" "rule=I:1")
448 ultimately AOT_have ‹φ{p} & [λy p] = [λy p]› using "&I" by blast
449 AOT_hence ‹∃q (φ{q} & [λy p] = [λy q])›
450 using "∃I" by fast
451 AOT_hence ‹c[λy p]›
452 by (safe intro!: c_prop[THEN "&E"(2), THEN "∀E"(1)[where τ="«[λy p]»"], THEN "≡E"(2)] "cqt:2")
453 AOT_thus ‹c ⊨ p›
454 by (metis "intro-elim:3:b" "vdash-properties:10" sit_c lem1)
455 qed
456 ultimately AOT_show ‹∃s∀p(s ⊨ p ≡ φ{p})›
457 by (meson "con-dis-i-e:1" "existential:2[const_var]")
458qed
459
460AOT_theorem "sit-comp-simp-unique": ‹∃!s∀p(s ⊨ p ≡ φ{p})›
461proof(safe intro!: "uniqueness:1"[THEN "≡⇩d⇩fI"])
462 AOT_obtain s where s_prop: ‹∀p(s ⊨ p ≡ φ{p})›
463 using "sit-comp-simp" Situation.instantiation[rotated] by meson
464 AOT_show ‹∃α (Situation(α) & ∀p (α ⊨ p ≡ φ{p}) & ∀β (Situation(β) & ∀p (β ⊨ p ≡ φ{p}) → β = α))›
465 proof(safe intro!: "∃I"(2) "&I")
466 AOT_show ‹Situation(s)›
467 using "Situation.ψ" by auto
468 next
469 AOT_show ‹∀p(s ⊨ p ≡ φ{p})› using s_prop.
470 next
471 AOT_show ‹∀β (Situation(β) & ∀p (β ⊨ p ≡ φ{p}) → β = s)›
472 proof(safe intro!: GEN "→I")
473 fix x
474 AOT_assume 1: ‹Situation(x) & ∀p (x ⊨ p ≡ φ{p})›
475 AOT_show ‹x = s›
476 proof (safe intro!: "sit-identity"[unconstrain s, THEN "→E", THEN "≡E"(2)] 1[THEN "&E"(1)] GEN "≡I" "→I")
477 fix p
478 AOT_assume ‹x ⊨ p›
479 AOT_hence ‹φ{p}›
480 using "1" "con-dis-i-e:2:b" "intro-elim:3:a" "log-prop-prop:2" "rule-ui:1" by blast
481 AOT_thus ‹s ⊨ p›
482 using s_prop "intro-elim:3:b" "log-prop-prop:2" "rule-ui:1" by blast
483 next
484 fix p
485 AOT_assume ‹s ⊨ p›
486 AOT_hence ‹φ{p}›
487 using "intro-elim:3:a" "log-prop-prop:2" "rule-ui:1" s_prop by blast
488 AOT_thus ‹x ⊨ p›
489 using "1" "con-dis-i-e:2:b" "intro-elim:3:b" "log-prop-prop:2" "rule-ui:1" by blast
490 qed
491 qed
492 qed
493qed
494
495AOT_define NullSituation :: ‹τ ⇒ φ› (‹NullSituation'(_')›)
496 "df-null-trivial:1": ‹NullSituation(s) ≡⇩d⇩f ¬∃p s ⊨ p›
497
498AOT_define TrivialSituation :: ‹τ ⇒ φ› (‹TrivialSituation'(_')›)
499 "df-null-trivial:2": ‹TrivialSituation(s) ≡⇩d⇩f ∀p s ⊨ p›
500
501AOT_theorem "thm-null-trivial:1": ‹∃!x NullSituation(x)›
502proof (AOT_subst ‹NullSituation(x)› ‹A!x & ∀F (x[F] ≡ F ≠ F)› for: x)
503 AOT_modally_strict {
504 AOT_show ‹NullSituation(x) ≡ A!x & ∀F (x[F] ≡ F ≠ F)› for x
505 proof (safe intro!: "≡I" "→I" "df-null-trivial:1"[THEN "≡⇩d⇩fI"]
506 dest!: "df-null-trivial:1"[THEN "≡⇩d⇩fE"])
507 AOT_assume 0: ‹Situation(x) & ¬∃p x ⊨ p›
508 AOT_have 1: ‹A!x›
509 using 0[THEN "&E"(1), THEN situations[THEN "≡⇩d⇩fE"], THEN "&E"(1)].
510 AOT_have 2: ‹x[F] → ∃p F = [λy p]› for F
511 using 0[THEN "&E"(1), THEN situations[THEN "≡⇩d⇩fE"],
512 THEN "&E"(2), THEN "∀E"(2)]
513 by (metis "≡⇩d⇩fE" "→I" "prop-prop1" "→E")
514 AOT_show ‹A!x & ∀F (x[F] ≡ F ≠ F)›
515 proof (safe intro!: "&I" 1 GEN "≡I" "→I")
516 fix F
517 AOT_assume ‹x[F]›
518 moreover AOT_obtain p where ‹F = [λy p]›
519 using calculation 2[THEN "→E"] "∃E"[rotated] by blast
520 ultimately AOT_have ‹x[λy p]›
521 by (metis "rule=E")
522 AOT_hence ‹x ⊨ p›
523 using lem1[THEN "→E", OF 0[THEN "&E"(1)], THEN "≡E"(2)] by blast
524 AOT_hence ‹∃p (x ⊨ p)›
525 by (rule "∃I")
526 AOT_thus ‹F ≠ F›
527 using 0[THEN "&E"(2)] "raa-cor:1" "&I" by blast
528 next
529 fix F :: ‹<κ> AOT_var›
530 AOT_assume ‹F ≠ F›
531 AOT_hence ‹¬(F = F)› by (metis "≡⇩d⇩fE" "=-infix")
532 moreover AOT_have ‹F = F›
533 by (simp add: "id-eq:1")
534 ultimately AOT_show ‹x[F]› using "&I" "raa-cor:1" by blast
535 qed
536 next
537 AOT_assume 0: ‹A!x & ∀F (x[F] ≡ F ≠ F)›
538 AOT_hence ‹x[F] ≡ F ≠ F› for F
539 using "∀E" "&E" by blast
540 AOT_hence 1: ‹¬x[F]› for F
541 using "≡⇩d⇩fE" "id-eq:1" "=-infix" "reductio-aa:1" "≡E"(1) by blast
542 AOT_show ‹Situation(x) & ¬∃p x ⊨ p›
543 proof (safe intro!: "&I" situations[THEN "≡⇩d⇩fI"] 0[THEN "&E"(1)] GEN "→I")
544 AOT_show ‹Propositional([F])› if ‹x[F]› for F
545 using that 1 "&I" "raa-cor:1" by fast
546 next
547 AOT_show ‹¬∃p x ⊨ p›
548 proof(rule "raa-cor:2")
549 AOT_assume ‹∃p x ⊨ p›
550 then AOT_obtain p where ‹x ⊨ p› using "∃E"[rotated] by blast
551 AOT_hence ‹x[λy p]›
552 using "≡⇩d⇩fE" "&E"(1) "≡E"(1) lem1 "modus-tollens:1"
553 "raa-cor:3" "true-in-s" by fast
554 moreover AOT_have ‹¬x[λy p]›
555 by (rule 1[unvarify F]) "cqt:2[lambda]"
556 ultimately AOT_show ‹p & ¬p› for p using "&I" "raa-cor:1" by blast
557 qed
558 qed
559 qed
560 }
561next
562 AOT_show ‹∃!x ([A!]x & ∀F (x[F] ≡ F ≠ F))›
563 by (simp add: "A-objects!")
564qed
565
566
567AOT_theorem "thm-null-trivial:2": ‹∃!x TrivialSituation(x)›
568proof (AOT_subst ‹TrivialSituation(x)› ‹A!x & ∀F (x[F] ≡ ∃p F = [λy p])› for: x)
569 AOT_modally_strict {
570 AOT_show ‹TrivialSituation(x) ≡ A!x & ∀F (x[F] ≡ ∃p F = [λy p])› for x
571 proof (safe intro!: "≡I" "→I" "df-null-trivial:2"[THEN "≡⇩d⇩fI"]
572 dest!: "df-null-trivial:2"[THEN "≡⇩d⇩fE"])
573 AOT_assume 0: ‹Situation(x) & ∀p x ⊨ p›
574 AOT_have 1: ‹A!x›
575 using 0[THEN "&E"(1), THEN situations[THEN "≡⇩d⇩fE"], THEN "&E"(1)].
576 AOT_have 2: ‹x[F] → ∃p F = [λy p]› for F
577 using 0[THEN "&E"(1), THEN situations[THEN "≡⇩d⇩fE"],
578 THEN "&E"(2), THEN "∀E"(2)]
579 by (metis "≡⇩d⇩fE" "deduction-theorem" "prop-prop1" "→E")
580 AOT_show ‹A!x & ∀F (x[F] ≡ ∃p F = [λy p])›
581 proof (safe intro!: "&I" 1 GEN "≡I" "→I" 2)
582 fix F
583 AOT_assume ‹∃p F = [λy p]›
584 then AOT_obtain p where ‹F = [λy p]›
585 using "∃E"[rotated] by blast
586 moreover AOT_have ‹x ⊨ p›
587 using 0[THEN "&E"(2)] "∀E" by blast
588 ultimately AOT_show ‹x[F]›
589 by (metis 0 "rule=E" "&E"(1) id_sym "≡E"(2) lem1
590 "Commutativity of ≡" "→E")
591 qed
592 next
593 AOT_assume 0: ‹A!x & ∀F (x[F] ≡ ∃p F = [λy p])›
594 AOT_hence 1: ‹x[F] ≡ ∃p F = [λy p]› for F
595 using "∀E" "&E" by blast
596 AOT_have 2: ‹Situation(x)›
597 proof (safe intro!: "&I" situations[THEN "≡⇩d⇩fI"] 0[THEN "&E"(1)] GEN "→I")
598 AOT_show ‹Propositional([F])› if ‹x[F]› for F
599 using 1[THEN "≡E"(1), OF that]
600 by (metis "≡⇩d⇩fI" "prop-prop1")
601 qed
602 AOT_show ‹Situation(x) & ∀p (x ⊨ p)›
603 proof (safe intro!: "&I" 2 0[THEN "&E"(1)] GEN "→I")
604 AOT_have ‹x[λy p] ≡ ∃q [λy p] = [λy q]› for p
605 by (rule 1[unvarify F, where τ="«[λy p]»"]) "cqt:2[lambda]"
606 moreover AOT_have ‹∃q [λy p] = [λy q]› for p
607 by (rule "∃I"(2)[where β=p])
608 (simp add: "rule=I:1" "prop-prop2:2")
609 ultimately AOT_have ‹x[λy p]› for p by (metis "≡E"(2))
610 AOT_thus ‹x ⊨ p› for p
611 by (metis "2" "≡E"(2) lem1 "→E")
612 qed
613 qed
614 }
615next
616 AOT_show ‹∃!x ([A!]x & ∀F (x[F] ≡ ∃p F = [λy p]))›
617 by (simp add: "A-objects!")
618qed
619
620AOT_theorem "thm-null-trivial:3": ‹❙ιx NullSituation(x)↓›
621 by (meson "A-Exists:2" "RA[2]" "≡E"(2) "thm-null-trivial:1")
622
623AOT_theorem "thm-null-trivial:4": ‹❙ιx TrivialSituation(x)↓›
624 using "A-Exists:2" "RA[2]" "≡E"(2) "thm-null-trivial:2" by blast
625
626AOT_define TheNullSituation :: ‹κ⇩s› (‹❙s⇩∅›)
627 "df-the-null-sit:1": ‹❙s⇩∅ =⇩d⇩f ❙ιx NullSituation(x)›
628
629AOT_define TheTrivialSituation :: ‹κ⇩s› (‹❙s⇩V›)
630 "df-the-null-sit:2": ‹❙s⇩V =⇩d⇩f ❙ιx TrivialSituation(x)›
631
632AOT_theorem "null-triv-sc:1": ‹NullSituation(x) → □NullSituation(x)›
633proof(safe intro!: "→I" dest!: "df-null-trivial:1"[THEN "≡⇩d⇩fE"];
634 frule "&E"(1); drule "&E"(2))
635 AOT_assume 1: ‹¬∃p (x ⊨ p)›
636 AOT_assume 0: ‹Situation(x)›
637 AOT_hence ‹□Situation(x)› by (metis "≡E"(1) "possit-sit:1")
638 moreover AOT_have ‹□¬∃p (x ⊨ p)›
639 proof(rule "raa-cor:1")
640 AOT_assume ‹¬□¬∃p (x ⊨ p)›
641 AOT_hence ‹◇∃p (x ⊨ p)›
642 by (metis "≡⇩d⇩fI" "conventions:5")
643 AOT_hence ‹∃p ◇(x ⊨ p)› by (metis "BF◇" "→E")
644 then AOT_obtain p where ‹◇(x ⊨ p)› using "∃E"[rotated] by blast
645 AOT_hence ‹x ⊨ p›
646 by (metis "≡E"(1) "lem2:2"[unconstrain s, THEN "→E", OF 0])
647 AOT_hence ‹∃p x ⊨ p› using "∃I" by fast
648 AOT_thus ‹∃p x ⊨ p & ¬∃p x ⊨ p› using 1 "&I" by blast
649 qed
650 ultimately AOT_have 2: ‹□(Situation(x) & ¬∃p x ⊨ p)›
651 by (metis "KBasic:3" "&I" "≡E"(2))
652 AOT_show ‹□NullSituation(x)›
653 by (AOT_subst ‹NullSituation(x)› ‹Situation(x) & ¬∃p x ⊨ p›)
654 (auto simp: "df-null-trivial:1" "≡Df" 2)
655qed
656
657
658AOT_theorem "null-triv-sc:2": ‹TrivialSituation(x) → □TrivialSituation(x)›
659proof(safe intro!: "→I" dest!: "df-null-trivial:2"[THEN "≡⇩d⇩fE"];
660 frule "&E"(1); drule "&E"(2))
661 AOT_assume 0: ‹Situation(x)›
662 AOT_hence 1: ‹□Situation(x)› by (metis "≡E"(1) "possit-sit:1")
663 AOT_assume ‹∀p x ⊨ p›
664 AOT_hence ‹x ⊨ p› for p
665 using "∀E" by blast
666 AOT_hence ‹□x ⊨ p› for p
667 using 0 "≡E"(1) "lem2:1"[unconstrain s, THEN "→E"] by blast
668 AOT_hence ‹∀p □x ⊨ p›
669 by (rule GEN)
670 AOT_hence ‹□∀p x ⊨ p›
671 by (rule BF[THEN "→E"])
672 AOT_hence 2: ‹□(Situation(x) & ∀p x ⊨ p)›
673 using 1 by (metis "KBasic:3" "&I" "≡E"(2))
674 AOT_show ‹□TrivialSituation(x)›
675 by (AOT_subst ‹TrivialSituation(x)› ‹Situation(x) & ∀p x ⊨ p›)
676 (auto simp: "df-null-trivial:2" "≡Df" 2)
677qed
678
679AOT_theorem "null-triv-sc:3": ‹NullSituation(❙s⇩∅)›
680 by (safe intro!: "df-the-null-sit:1"[THEN "=⇩d⇩fI"(2)] "thm-null-trivial:3"
681 "rule=I:1"[OF "thm-null-trivial:3"]
682 "!box-desc:2"[THEN "→E", THEN "→E", rotated, OF "thm-null-trivial:1",
683 OF "∀I", OF "null-triv-sc:1", THEN "∀E"(1), THEN "→E"])
684
685AOT_theorem "null-triv-sc:4": ‹TrivialSituation(❙s⇩V)›
686 by (safe intro!: "df-the-null-sit:2"[THEN "=⇩d⇩fI"(2)] "thm-null-trivial:4"
687 "rule=I:1"[OF "thm-null-trivial:4"]
688 "!box-desc:2"[THEN "→E", THEN "→E", rotated, OF "thm-null-trivial:2",
689 OF "∀I", OF "null-triv-sc:2", THEN "∀E"(1), THEN "→E"])
690
691AOT_theorem "null-triv-facts:1": ‹NullSituation(x) ≡ Null(x)›
692proof (safe intro!: "≡I" "→I" "df-null-uni:1"[THEN "≡⇩d⇩fI"]
693 "df-null-trivial:1"[THEN "≡⇩d⇩fI"]
694 dest!: "df-null-uni:1"[THEN "≡⇩d⇩fE"] "df-null-trivial:1"[THEN "≡⇩d⇩fE"])
695 AOT_assume 0: ‹Situation(x) & ¬∃p x ⊨ p›
696 AOT_have 1: ‹x[F] → ∃p F = [λy p]› for F
697 using 0[THEN "&E"(1), THEN situations[THEN "≡⇩d⇩fE"], THEN "&E"(2), THEN "∀E"(2)]
698 by (metis "≡⇩d⇩fE" "deduction-theorem" "prop-prop1" "→E")
699 AOT_show ‹A!x & ¬∃F x[F]›
700 proof (safe intro!: "&I" 0[THEN "&E"(1), THEN situations[THEN "≡⇩d⇩fE"],
701 THEN "&E"(1)];
702 rule "raa-cor:2")
703 AOT_assume ‹∃F x[F]›
704 then AOT_obtain F where F_prop: ‹x[F]›
705 using "∃E"[rotated] by blast
706 AOT_hence ‹∃p F = [λy p]›
707 using 1[THEN "→E"] by blast
708 then AOT_obtain p where ‹F = [λy p]›
709 using "∃E"[rotated] by blast
710 AOT_hence ‹x[λy p]›
711 by (metis "rule=E" F_prop)
712 AOT_hence ‹x ⊨ p›
713 using lem1[THEN "→E", OF 0[THEN "&E"(1)], THEN "≡E"(2)] by blast
714 AOT_hence ‹∃p x ⊨ p›
715 by (rule "∃I")
716 AOT_thus ‹∃p x ⊨ p & ¬∃p x ⊨ p›
717 using 0[THEN "&E"(2)] "&I" by blast
718 qed
719next
720 AOT_assume 0: ‹A!x & ¬∃F x[F]›
721 AOT_have ‹Situation(x)›
722 apply (rule situations[THEN "≡⇩d⇩fI", OF "&I", OF 0[THEN "&E"(1)]]; rule GEN)
723 using 0[THEN "&E"(2)] by (metis "→I" "existential:2[const_var]" "raa-cor:3")
724 moreover AOT_have ‹¬∃p x ⊨ p›
725 proof (rule "raa-cor:2")
726 AOT_assume ‹∃p x ⊨ p›
727 then AOT_obtain p where ‹x ⊨ p› by (metis "instantiation")
728 AOT_hence ‹x[λy p]› by (metis "≡⇩d⇩fE" "&E"(2) "prop-enc" "true-in-s")
729 AOT_hence ‹∃F x[F]› by (rule "∃I") "cqt:2[lambda]"
730 AOT_thus ‹∃F x[F] & ¬∃F x[F]› using 0[THEN "&E"(2)] "&I" by blast
731 qed
732 ultimately AOT_show ‹Situation(x) & ¬∃p x ⊨ p› using "&I" by blast
733qed
734
735AOT_theorem "null-triv-facts:2": ‹❙s⇩∅ = a⇩∅›
736 apply (rule "=⇩d⇩fI"(2)[OF "df-the-null-sit:1"])
737 apply (fact "thm-null-trivial:3")
738 apply (rule "=⇩d⇩fI"(2)[OF "df-null-uni-terms:1"])
739 apply (fact "null-uni-uniq:3")
740 apply (rule "equiv-desc-eq:3"[THEN "→E"])
741 apply (rule "&I")
742 apply (fact "thm-null-trivial:3")
743 by (rule RN; rule GEN; rule "null-triv-facts:1")
744
745AOT_theorem "null-triv-facts:3": ‹❙s⇩V ≠ a⇩V›
746proof(rule "=-infix"[THEN "≡⇩d⇩fI"])
747 AOT_have ‹Universal(a⇩V)›
748 by (simp add: "null-uni-facts:4")
749 AOT_hence 0: ‹a⇩V[A!]›
750 using "df-null-uni:2"[THEN "≡⇩d⇩fE"] "&E" "∀E"(1)
751 by (metis "cqt:5:a" "vdash-properties:10" "vdash-properties:1[2]")
752 moreover AOT_have 1: ‹¬❙s⇩V[A!]›
753 proof(rule "raa-cor:2")
754 AOT_have ‹Situation(❙s⇩V)›
755 using "≡⇩d⇩fE" "&E"(1) "df-null-trivial:2" "null-triv-sc:4" by blast
756 AOT_hence ‹∀F (❙s⇩V[F] → Propositional([F]))›
757 by (metis "≡⇩d⇩fE" "&E"(2) situations)
758 moreover AOT_assume ‹❙s⇩V[A!]›
759 ultimately AOT_have ‹Propositional(A!)›
760 using "∀E"(1)[rotated, OF "oa-exist:2"] "→E" by blast
761 AOT_thus ‹Propositional(A!) & ¬Propositional(A!)›
762 using "prop-in-f:4:d" "&I" by blast
763 qed
764 AOT_show ‹¬(❙s⇩V = a⇩V)›
765 proof (rule "raa-cor:2")
766 AOT_assume ‹❙s⇩V = a⇩V›
767 AOT_hence ‹❙s⇩V[A!]› using 0 "rule=E" id_sym by fast
768 AOT_thus ‹❙s⇩V[A!] & ¬❙s⇩V[A!]› using 1 "&I" by blast
769 qed
770qed
771
772definition ConditionOnPropositionalProperties :: ‹(<κ> ⇒ 𝗈) ⇒ bool› where
773 "cond-prop": ‹ConditionOnPropositionalProperties ≡ λ φ . ∀ v .
774 [v ⊨ ∀F (φ{F} → Propositional([F]))]›
775
776syntax ConditionOnPropositionalProperties :: ‹id_position ⇒ AOT_prop›
777 ("CONDITION'_ON'_PROPOSITIONAL'_PROPERTIES'(_')")
778
779AOT_theorem "cond-prop[E]":
780 assumes ‹CONDITION_ON_PROPOSITIONAL_PROPERTIES(φ)›
781 shows ‹∀F (φ{F} → Propositional([F]))›
782 using assms[unfolded "cond-prop"] by auto
783
784AOT_theorem "cond-prop[I]":
785 assumes ‹❙⊢⇩□ ∀F (φ{F} → Propositional([F]))›
786 shows ‹CONDITION_ON_PROPOSITIONAL_PROPERTIES(φ)›
787 using assms "cond-prop" by metis
788
789AOT_theorem "pre-comp-sit":
790 assumes ‹CONDITION_ON_PROPOSITIONAL_PROPERTIES(φ)›
791 shows ‹(Situation(x) & ∀F (x[F] ≡ φ{F})) ≡ (A!x & ∀F (x[F] ≡ φ{F}))›
792proof(rule "≡I"; rule "→I")
793 AOT_assume ‹Situation(x) & ∀F (x[F] ≡ φ{F})›
794 AOT_thus ‹A!x & ∀F (x[F] ≡ φ{F})›
795 using "&E" situations[THEN "≡⇩d⇩fE"] "&I" by blast
796next
797 AOT_assume 0: ‹A!x & ∀F (x[F] ≡ φ{F})›
798 AOT_show ‹Situation(x) & ∀F (x[F] ≡ φ{F})›
799 proof (safe intro!: situations[THEN "≡⇩d⇩fI"] "&I")
800 AOT_show ‹A!x› using 0[THEN "&E"(1)].
801 next
802 AOT_show ‹∀F (x[F] → Propositional([F]))›
803 proof(rule GEN; rule "→I")
804 fix F
805 AOT_assume ‹x[F]›
806 AOT_hence ‹φ{F}›
807 using 0[THEN "&E"(2)] "∀E" "≡E" by blast
808 AOT_thus ‹Propositional([F])›
809 using "cond-prop[E]"[OF assms] "∀E" "→E" by blast
810 qed
811 next
812 AOT_show ‹∀F (x[F] ≡ φ{F})› using 0 "&E" by blast
813 qed
814qed
815
816AOT_theorem "comp-sit:1":
817 assumes ‹CONDITION_ON_PROPOSITIONAL_PROPERTIES(φ)›
818 shows ‹∃s ∀F(s[F] ≡ φ{F})›
819 by (AOT_subst ‹Situation(x) & ∀F(x[F] ≡ φ{F})› ‹A!x & ∀F (x[F] ≡ φ{F})› for: x)
820 (auto simp: "pre-comp-sit"[OF assms] "A-objects"[where φ=φ, axiom_inst])
821
822AOT_theorem "comp-sit:2":
823 assumes ‹CONDITION_ON_PROPOSITIONAL_PROPERTIES(φ)›
824 shows ‹∃!s ∀F(s[F] ≡ φ{F})›
825 by (AOT_subst ‹Situation(x) & ∀F(x[F] ≡ φ{F})› ‹A!x & ∀F (x[F] ≡ φ{F})› for: x)
826 (auto simp: assms "pre-comp-sit" "pre-comp-sit"[OF assms] "A-objects!")
827
828AOT_theorem "can-sit-desc:1":
829 assumes ‹CONDITION_ON_PROPOSITIONAL_PROPERTIES(φ)›
830 shows ‹❙ιs(∀F (s[F] ≡ φ{F}))↓›
831 using "comp-sit:2"[OF assms] "A-Exists:2" "RA[2]" "≡E"(2) by blast
832
833AOT_theorem "can-sit-desc:2":
834 assumes ‹CONDITION_ON_PROPOSITIONAL_PROPERTIES(φ)›
835 shows ‹❙ιs(∀F (s[F] ≡ φ{F})) = ❙ιx(A!x & ∀F (x[F] ≡ φ{F}))›
836 by (auto intro!: "equiv-desc-eq:2"[THEN "→E", OF "&I",
837 OF "can-sit-desc:1"[OF assms]]
838 "RA[2]" GEN "pre-comp-sit"[OF assms])
839
840AOT_theorem "strict-sit":
841 assumes ‹RIGID_CONDITION(φ)›
842 and ‹CONDITION_ON_PROPOSITIONAL_PROPERTIES(φ)›
843 shows ‹y = ❙ιs(∀F (s[F] ≡ φ{F})) → ∀F (y[F] ≡ φ{F})›
844 using "rule=E"[rotated, OF "can-sit-desc:2"[OF assms(2), symmetric]]
845 "box-phi-a:2"[OF assms(1)] "→E" "→I" "&E" by fast
846
847
848
849AOT_define actual :: ‹τ ⇒ φ› (‹Actual'(_')›)
850 ‹Actual(s) ≡⇩d⇩f ∀p (s ⊨ p → p)›
851
852AOT_theorem "act-and-not-pos": ‹∃s (Actual(s) & ◇¬Actual(s))›
853proof -
854 AOT_obtain q⇩1 where q⇩1_prop: ‹q⇩1 & ◇¬q⇩1›
855 by (metis "≡⇩d⇩fE" "instantiation" "cont-tf:1" "cont-tf-thm:1")
856 AOT_have ‹∃s (∀F (s[F] ≡ F = [λy q⇩1]))›
857 proof (safe intro!: "comp-sit:1" "cond-prop[I]" GEN "→I")
858 AOT_modally_strict {
859 AOT_show ‹Propositional([F])› if ‹F = [λy q⇩1]› for F
860 using "≡⇩d⇩fI" "existential:2[const_var]" "prop-prop1" that by fastforce
861 }
862 qed
863 then AOT_obtain s⇩1 where s_prop: ‹∀F (s⇩1[F] ≡ F = [λy q⇩1])›
864 using "Situation.∃E"[rotated] by meson
865 AOT_have ‹Actual(s⇩1)›
866 proof(safe intro!: actual[THEN "≡⇩d⇩fI"] "&I" GEN "→I" s_prop Situation.ψ)
867 fix p
868 AOT_assume ‹s⇩1 ⊨ p›
869 AOT_hence ‹s⇩1[λy p]›
870 by (metis "≡⇩d⇩fE" "&E"(2) "prop-enc" "true-in-s")
871 AOT_hence ‹[λy p] = [λy q⇩1]›
872 by (rule s_prop[THEN "∀E"(1), THEN "≡E"(1), rotated]) "cqt:2[lambda]"
873 AOT_hence ‹p = q⇩1› by (metis "≡E"(2) "p-identity-thm2:3")
874 AOT_thus ‹p› using q⇩1_prop[THEN "&E"(1)] "rule=E" id_sym by fast
875 qed
876 moreover AOT_have ‹◇¬Actual(s⇩1)›
877 proof(rule "raa-cor:1"; drule "KBasic:12"[THEN "≡E"(2)])
878 AOT_assume ‹□Actual(s⇩1)›
879 AOT_hence ‹□(Situation(s⇩1) & ∀p (s⇩1 ⊨ p → p))›
880 using actual[THEN "≡Df", THEN "conventions:3"[THEN "≡⇩d⇩fE"],
881 THEN "&E"(1), THEN RM, THEN "→E"] by blast
882 AOT_hence ‹□∀p (s⇩1 ⊨ p → p)›
883 by (metis "RM:1" "Conjunction Simplification"(2) "→E")
884 AOT_hence ‹∀p □(s⇩1 ⊨ p → p)›
885 by (metis "CBF" "vdash-properties:10")
886 AOT_hence ‹□(s⇩1 ⊨ q⇩1 → q⇩1)›
887 using "∀E" by blast
888 AOT_hence ‹□s⇩1 ⊨ q⇩1 → □q⇩1›
889 by (metis "→E" "qml:1" "vdash-properties:1[2]")
890 moreover AOT_have ‹s⇩1 ⊨ q⇩1›
891 using s_prop[THEN "∀E"(1), THEN "≡E"(2),
892 THEN lem1[THEN "→E", OF Situation.ψ, THEN "≡E"(2)]]
893 "rule=I:1" "prop-prop2:2" by blast
894 ultimately AOT_have ‹□q⇩1›
895 using "≡⇩d⇩fE" "&E"(1) "≡E"(1) "lem2:1" "true-in-s" "→E" by fast
896 AOT_thus ‹◇¬q⇩1 & ¬◇¬q⇩1›
897 using "KBasic:12"[THEN "≡E"(1)] q⇩1_prop[THEN "&E"(2)] "&I" by blast
898 qed
899 ultimately AOT_have ‹(Actual(s⇩1) & ◇¬Actual(s⇩1))›
900 using s_prop "&I" by blast
901 thus ?thesis
902 by (rule "Situation.∃I")
903qed
904
905AOT_theorem "actual-s:1": ‹∃s Actual(s)›
906proof -
907 AOT_obtain s where ‹(Actual(s) & ◇¬Actual(s))›
908 using "act-and-not-pos" "Situation.∃E"[rotated] by meson
909 AOT_hence ‹Actual(s)› using "&E" "&I" by metis
910 thus ?thesis by (rule "Situation.∃I")
911qed
912
913AOT_theorem "actual-s:2": ‹∃s ¬Actual(s)›
914proof(rule "∃I"(1)[where τ=‹«❙s⇩V»›]; (rule "&I")?)
915 AOT_show ‹Situation(❙s⇩V)›
916 using "≡⇩d⇩fE" "&E"(1) "df-null-trivial:2" "null-triv-sc:4" by blast
917next
918 AOT_show ‹¬Actual(❙s⇩V)›
919 proof(rule "raa-cor:2")
920 AOT_assume 0: ‹Actual(❙s⇩V)›
921 AOT_obtain p⇩1 where notp⇩1: ‹¬p⇩1›
922 by (metis "∃E" "∃I"(1) "log-prop-prop:2" "non-contradiction")
923 AOT_have ‹❙s⇩V ⊨ p⇩1›
924 using "null-triv-sc:4"[THEN "≡⇩d⇩fE"[OF "df-null-trivial:2"], THEN "&E"(2)]
925 "∀E" by blast
926 AOT_hence ‹p⇩1›
927 using 0[THEN actual[THEN "≡⇩d⇩fE"], THEN "&E"(2), THEN "∀E"(2), THEN "→E"]
928 by blast
929 AOT_thus ‹p & ¬p› for p using notp⇩1 by (metis "raa-cor:3")
930 qed
931next
932 AOT_show ‹❙s⇩V↓›
933 using "df-the-null-sit:2" "rule-id-df:2:b[zero]" "thm-null-trivial:4" by blast
934qed
935
936AOT_theorem "actual-s:3": ‹∃p∀s(Actual(s) → ¬s ⊨ p)›
937proof -
938 AOT_obtain p⇩1 where notp⇩1: ‹¬p⇩1›
939 by (metis "∃E" "∃I"(1) "log-prop-prop:2" "non-contradiction")
940 AOT_have ‹∀s (Actual(s) → ¬(s ⊨ p⇩1))›
941 proof (rule Situation.GEN; rule "→I"; rule "raa-cor:2")
942 fix s
943 AOT_assume ‹Actual(s)›
944 moreover AOT_assume ‹s ⊨ p⇩1›
945 ultimately AOT_have ‹p⇩1›
946 using actual[THEN "≡⇩d⇩fE", THEN "&E"(2), THEN "∀E"(2), THEN "→E"] by blast
947 AOT_thus ‹p⇩1 & ¬p⇩1›
948 using notp⇩1 "&I" by simp
949 qed
950 thus ?thesis by (rule "∃I")
951qed
952
953AOT_theorem comp:
954 ‹∃s (s' ⊴ s & s'' ⊴ s & ∀s''' (s' ⊴ s''' & s'' ⊴ s''' → s ⊴ s'''))›
955proof -
956 have cond_prop: ‹ConditionOnPropositionalProperties (λ Π . «s'[Π] ∨ s''[Π]»)›
957 proof(safe intro!: "cond-prop[I]" GEN "oth-class-taut:8:c"[THEN "→E", THEN "→E"];
958 rule "→I")
959 AOT_modally_strict {
960 fix F
961 AOT_have ‹Situation(s')›
962 by (simp add: Situation.restricted_var_condition)
963 AOT_hence ‹s'[F] → Propositional([F])›
964 using "situations"[THEN "≡⇩d⇩fE", THEN "&E"(2), THEN "∀E"(2)] by blast
965 moreover AOT_assume ‹s'[F]›
966 ultimately AOT_show ‹Propositional([F])›
967 using "→E" by blast
968 }
969 next
970 AOT_modally_strict {
971 fix F
972 AOT_have ‹Situation(s'')›
973 by (simp add: Situation.restricted_var_condition)
974 AOT_hence ‹s''[F] → Propositional([F])›
975 using "situations"[THEN "≡⇩d⇩fE", THEN "&E"(2), THEN "∀E"(2)] by blast
976 moreover AOT_assume ‹s''[F]›
977 ultimately AOT_show ‹Propositional([F])›
978 using "→E" by blast
979 }
980 qed
981 AOT_obtain s⇩3 where θ: ‹∀F (s⇩3[F] ≡ s'[F] ∨ s''[F])›
982 using "comp-sit:1"[OF cond_prop] "Situation.∃E"[rotated] by meson
983 AOT_have ‹s' ⊴ s⇩3 & s'' ⊴ s⇩3 & ∀s''' (s' ⊴ s''' & s'' ⊴ s''' → s⇩3 ⊴ s''')›
984 proof(safe intro!: "&I" "≡⇩d⇩fI"[OF "true-in-s"] "≡⇩d⇩fI"[OF "prop-enc"]
985 "Situation.GEN" "GEN"[where 'a=𝗈] "→I"
986 "sit-part-whole"[THEN "≡⇩d⇩fI"]
987 Situation.ψ "cqt:2[const_var]"[axiom_inst])
988 fix p
989 AOT_assume ‹s' ⊨ p›
990 AOT_hence ‹s'[λx p]›
991 by (metis "&E"(2) "prop-enc" "≡⇩d⇩fE" "true-in-s")
992 AOT_thus ‹s⇩3[λx p]›
993 using θ[THEN "∀E"(1),OF "prop-prop2:2", THEN "≡E"(2), OF "∨I"(1)] by blast
994 next
995 fix p
996 AOT_assume ‹s'' ⊨ p›
997 AOT_hence ‹s''[λx p]›
998 by (metis "&E"(2) "prop-enc" "≡⇩d⇩fE" "true-in-s")
999 AOT_thus ‹s⇩3[λx p]›
1000 using θ[THEN "∀E"(1),OF "prop-prop2:2", THEN "≡E"(2), OF "∨I"(2)] by blast
1001 next
1002 fix s p
1003 AOT_assume 0: ‹s' ⊴ s & s'' ⊴ s›
1004 AOT_assume ‹s⇩3 ⊨ p›
1005 AOT_hence ‹s⇩3[λx p]›
1006 by (metis "&E"(2) "prop-enc" "≡⇩d⇩fE" "true-in-s")
1007 AOT_hence ‹s'[λx p] ∨ s''[λx p]›
1008 using θ[THEN "∀E"(1),OF "prop-prop2:2", THEN "≡E"(1)] by blast
1009 moreover {
1010 AOT_assume ‹s'[λx p]›
1011 AOT_hence ‹s' ⊨ p›
1012 by (safe intro!: "prop-enc"[THEN "≡⇩d⇩fI"] "true-in-s"[THEN "≡⇩d⇩fI"] "&I"
1013 Situation.ψ "cqt:2[const_var]"[axiom_inst])
1014 moreover AOT_have ‹s' ⊨ p → s ⊨ p›
1015 using "sit-part-whole"[THEN "≡⇩d⇩fE", THEN "&E"(2)] 0[THEN "&E"(1)]
1016 "∀E"(2) by blast
1017 ultimately AOT_have ‹s ⊨ p›
1018 using "→E" by blast
1019 AOT_hence ‹s[λx p]›
1020 using "true-in-s"[THEN "≡⇩d⇩fE"] "prop-enc"[THEN "≡⇩d⇩fE"] "&E" by blast
1021 }
1022 moreover {
1023 AOT_assume ‹s''[λx p]›
1024 AOT_hence ‹s'' ⊨ p›
1025 by (safe intro!: "prop-enc"[THEN "≡⇩d⇩fI"] "true-in-s"[THEN "≡⇩d⇩fI"] "&I"
1026 Situation.ψ "cqt:2[const_var]"[axiom_inst])
1027 moreover AOT_have ‹s'' ⊨ p → s ⊨ p›
1028 using "sit-part-whole"[THEN "≡⇩d⇩fE", THEN "&E"(2)] 0[THEN "&E"(2)]
1029 "∀E"(2) by blast
1030 ultimately AOT_have ‹s ⊨ p›
1031 using "→E" by blast
1032 AOT_hence ‹s[λx p]›
1033 using "true-in-s"[THEN "≡⇩d⇩fE"] "prop-enc"[THEN "≡⇩d⇩fE"] "&E" by blast
1034 }
1035 ultimately AOT_show ‹s[λx p]›
1036 by (metis "∨E"(1) "→I")
1037 qed
1038 thus ?thesis
1039 using "Situation.∃I" by fast
1040qed
1041
1042AOT_theorem "act-sit:1": ‹Actual(s) → (s ⊨ p → [λy p]s)›
1043proof (safe intro!: "→I")
1044 AOT_assume ‹Actual(s)›
1045 AOT_hence p if ‹s ⊨ p›
1046 using actual[THEN "≡⇩d⇩fE", THEN "&E"(2), THEN "∀E"(2), THEN "→E"] that by blast
1047 moreover AOT_assume ‹s ⊨ p›
1048 ultimately AOT_have p by blast
1049 AOT_thus ‹[λy p]s›
1050 by (safe intro!: "β←C"(1) "cqt:2")
1051qed
1052
1053AOT_theorem "act-sit:2":
1054 ‹(Actual(s') & Actual(s'')) → ∃x (Actual(x) & s' ⊴ x & s'' ⊴ x)›
1055proof(rule "→I"; frule "&E"(1); drule "&E"(2))
1056 AOT_assume act_s': ‹Actual(s')›
1057 AOT_assume act_s'': ‹Actual(s'')›
1058 have "cond-prop": ‹ConditionOnPropositionalProperties
1059 (λ Π . «∃p (Π = [λy p] & (s' ⊨ p ∨ s'' ⊨ p))»)›
1060 proof (safe intro!: "cond-prop[I]" "∀I" "→I" "prop-prop1"[THEN "≡⇩d⇩fI"])
1061 AOT_modally_strict {
1062 fix β
1063 AOT_assume ‹∃p (β = [λy p] & (s' ⊨ p ∨ s'' ⊨ p))›
1064 then AOT_obtain p where ‹β = [λy p]› using "∃E"[rotated] "&E" by blast
1065 AOT_thus ‹∃p β = [λy p]› by (rule "∃I")
1066 }
1067 qed
1068 have rigid: ‹rigid_condition (λ Π . «∃p (Π = [λy p] & (s' ⊨ p ∨ s'' ⊨ p))»)›
1069 proof(safe intro!: "strict-can:1[I]" "→I" GEN)
1070 AOT_modally_strict {
1071 fix F
1072 AOT_assume ‹∃p (F = [λy p] & (s' ⊨ p ∨ s'' ⊨ p))›
1073 then AOT_obtain p⇩1 where p⇩1_prop: ‹F = [λy p⇩1] & (s' ⊨ p⇩1 ∨ s'' ⊨ p⇩1)›
1074 using "∃E"[rotated] by blast
1075 AOT_hence ‹□(F = [λy p⇩1])›
1076 using "&E"(1) "id-nec:2" "vdash-properties:10" by blast
1077 moreover AOT_have ‹□(s' ⊨ p⇩1 ∨ s'' ⊨ p⇩1)›
1078 proof(rule "∨E"; (rule "→I"; rule "KBasic:15"[THEN "→E"])?)
1079 AOT_show ‹s' ⊨ p⇩1 ∨ s'' ⊨ p⇩1› using p⇩1_prop "&E" by blast
1080 next
1081 AOT_show ‹□s' ⊨ p⇩1 ∨ □s'' ⊨ p⇩1› if ‹s' ⊨ p⇩1›
1082 apply (rule "∨I"(1))
1083 using "≡⇩d⇩fE" "&E"(1) "≡E"(1) "lem2:1" that "true-in-s" by blast
1084 next
1085 AOT_show ‹□s' ⊨ p⇩1 ∨ □s'' ⊨ p⇩1› if ‹s'' ⊨ p⇩1›
1086 apply (rule "∨I"(2))
1087 using "≡⇩d⇩fE" "&E"(1) "≡E"(1) "lem2:1" that "true-in-s" by blast
1088 qed
1089 ultimately AOT_have ‹□(F = [λy p⇩1] & (s' ⊨ p⇩1 ∨ s'' ⊨ p⇩1))›
1090 by (metis "KBasic:3" "&I" "≡E"(2))
1091 AOT_hence ‹∃p □(F = [λy p] & (s' ⊨ p ∨ s'' ⊨ p))› by (rule "∃I")
1092 AOT_thus ‹□∃p (F = [λy p] & (s' ⊨ p ∨ s'' ⊨ p))›
1093 using Buridan[THEN "→E"] by fast
1094 }
1095 qed
1096
1097 AOT_have desc_den: ‹❙ιs(∀F (s[F] ≡ ∃p (F = [λy p] & (s' ⊨ p ∨ s'' ⊨ p))))↓›
1098 by (rule "can-sit-desc:1"[OF "cond-prop"])
1099 AOT_obtain x⇩0
1100 where x⇩0_prop1: ‹x⇩0 = ❙ιs(∀F (s[F] ≡ ∃p (F = [λy p] & (s' ⊨ p ∨ s'' ⊨ p))))›
1101 by (metis (no_types, lifting) "∃E" "rule=I:1" desc_den "∃I"(1) id_sym)
1102 AOT_hence x⇩0_sit: ‹Situation(x⇩0)›
1103 using "actual-desc:3"[THEN "→E"] "Act-Basic:2" "&E"(1) "≡E"(1)
1104 "possit-sit:4" by blast
1105
1106 AOT_have 1: ‹∀F (x⇩0[F] ≡ ∃p (F = [λy p] & (s' ⊨ p ∨ s'' ⊨ p)))›
1107 using "strict-sit"[OF rigid, OF "cond-prop", THEN "→E", OF x⇩0_prop1].
1108 AOT_have 2: ‹(x⇩0 ⊨ p) ≡ (s' ⊨ p ∨ s'' ⊨ p)› for p
1109 proof (rule "≡I"; rule "→I")
1110 AOT_assume ‹x⇩0 ⊨ p›
1111 AOT_hence ‹x⇩0[λy p]› using lem1[THEN "→E", OF x⇩0_sit, THEN "≡E"(1)] by blast
1112 then AOT_obtain q where ‹[λy p] = [λy q] & (s' ⊨ q ∨ s'' ⊨ q)›
1113 using 1[THEN "∀E"(1)[where τ="«[λy p]»"], OF "prop-prop2:2", THEN "≡E"(1)]
1114 "∃E"[rotated] by blast
1115 AOT_thus ‹s' ⊨ p ∨ s'' ⊨ p›
1116 by (metis "rule=E" "&E"(1) "&E"(2) "∨I"(1) "∨I"(2)
1117 "∨E"(1) "deduction-theorem" id_sym "≡E"(2) "p-identity-thm2:3")
1118 next
1119 AOT_assume ‹s' ⊨ p ∨ s'' ⊨ p›
1120 AOT_hence ‹[λy p] = [λy p] & (s' ⊨ p ∨ s'' ⊨ p)›
1121 by (metis "rule=I:1" "&I" "prop-prop2:2")
1122 AOT_hence ‹∃q ([λy p] = [λy q] & (s' ⊨ q ∨ s'' ⊨ q))›
1123 by (rule "∃I")
1124 AOT_hence ‹x⇩0[λy p]›
1125 using 1[THEN "∀E"(1), OF "prop-prop2:2", THEN "≡E"(2)] by blast
1126 AOT_thus ‹x⇩0 ⊨ p›
1127 by (metis "≡⇩d⇩fI" "&I" "ex:1:a" "prop-enc" "rule-ui:2[const_var]"
1128 x⇩0_sit "true-in-s")
1129 qed
1130
1131 AOT_have ‹Actual(x⇩0) & s' ⊴ x⇩0 & s'' ⊴ x⇩0›
1132 proof(safe intro!: "→I" "&I" "∃I"(1) actual[THEN "≡⇩d⇩fI"] x⇩0_sit GEN
1133 "sit-part-whole"[THEN "≡⇩d⇩fI"])
1134 fix p
1135 AOT_assume ‹x⇩0 ⊨ p›
1136 AOT_hence ‹s' ⊨ p ∨ s'' ⊨ p›
1137 using 2 "≡E"(1) by metis
1138 AOT_thus ‹p›
1139 using act_s' act_s''
1140 actual[THEN "≡⇩d⇩fE", THEN "&E"(2), THEN "∀E"(2), THEN "→E"]
1141 by (metis "∨E"(3) "reductio-aa:1")
1142 next
1143 AOT_show ‹x⇩0 ⊨ p› if ‹s' ⊨ p› for p
1144 using 2[THEN "≡E"(2), OF "∨I"(1), OF that].
1145 next
1146 AOT_show ‹x⇩0 ⊨ p› if ‹s'' ⊨ p› for p
1147 using 2[THEN "≡E"(2), OF "∨I"(2), OF that].
1148 next
1149 AOT_show ‹Situation(s')›
1150 using act_s'[THEN actual[THEN "≡⇩d⇩fE"]] "&E" by blast
1151 next
1152 AOT_show ‹Situation(s'')›
1153 using act_s''[THEN actual[THEN "≡⇩d⇩fE"]] "&E" by blast
1154 qed
1155 AOT_thus ‹∃x (Actual(x) & s' ⊴ x & s'' ⊴ x)›
1156 by (rule "∃I")
1157qed
1158
1159AOT_define Consistent :: ‹τ ⇒ φ› (‹Consistent'(_')›)
1160 cons: ‹Consistent(s) ≡⇩d⇩f ¬∃p (s ⊨ p & s ⊨ ¬p)›
1161
1162AOT_theorem "sit-cons": ‹Actual(s) → Consistent(s)›
1163proof(safe intro!: "→I" cons[THEN "≡⇩d⇩fI"] "&I" Situation.ψ
1164 dest!: actual[THEN "≡⇩d⇩fE"]; frule "&E"(1); drule "&E"(2))
1165 AOT_assume 0: ‹∀p (s ⊨ p → p)›
1166 AOT_show ‹¬∃p (s ⊨ p & s ⊨ ¬p)›
1167 proof (rule "raa-cor:2")
1168 AOT_assume ‹∃p (s ⊨ p & s ⊨ ¬p)›
1169 then AOT_obtain p where ‹s ⊨ p & s ⊨ ¬p›
1170 using "∃E"[rotated] by blast
1171 AOT_hence ‹p & ¬p›
1172 using 0[THEN "∀E"(1)[where τ=‹«¬p»›, THEN "→E"], OF "log-prop-prop:2"]
1173 0[THEN "∀E"(2)[where β=p], THEN "→E"] "&E" "&I" by blast
1174 AOT_thus ‹p & ¬p› for p by (metis "raa-cor:1")
1175 qed
1176qed
1177
1178AOT_theorem "cons-rigid:1": ‹¬Consistent(s) ≡ □¬Consistent(s)›
1179proof (rule "≡I"; rule "→I")
1180 AOT_assume ‹¬Consistent(s)›
1181 AOT_hence ‹∃p (s ⊨ p & s ⊨ ¬p)›
1182 using cons[THEN "≡⇩d⇩fI", OF "&I", OF Situation.ψ]
1183 by (metis "raa-cor:3")
1184 then AOT_obtain p where p_prop: ‹s ⊨ p & s ⊨ ¬p›
1185 using "∃E"[rotated] by blast
1186 AOT_hence ‹□s ⊨ p›
1187 using "&E"(1) "≡E"(1) "lem2:1" by blast
1188 moreover AOT_have ‹□s ⊨ ¬p›
1189 using p_prop "T◇" "&E" "≡E"(1)
1190 "modus-tollens:1" "raa-cor:3" "lem2:3"[unvarify p]
1191 "log-prop-prop:2" by metis
1192 ultimately AOT_have ‹□(s ⊨ p & s ⊨ ¬p)›
1193 by (metis "KBasic:3" "&I" "≡E"(2))
1194 AOT_hence ‹∃p □(s ⊨ p & s ⊨ ¬p)›
1195 by (rule "∃I")
1196 AOT_hence ‹□∃p(s ⊨ p & s ⊨ ¬p)›
1197 by (metis Buridan "vdash-properties:10")
1198 AOT_thus ‹□¬Consistent(s)›
1199 apply (rule "qml:1"[axiom_inst, THEN "→E", THEN "→E", rotated])
1200 apply (rule RN)
1201 using "≡⇩d⇩fE" "&E"(2) cons "deduction-theorem" "raa-cor:3" by blast
1202next
1203 AOT_assume ‹□¬Consistent(s)›
1204 AOT_thus ‹¬Consistent(s)› using "qml:2"[axiom_inst, THEN "→E"] by auto
1205qed
1206
1207AOT_theorem "cons-rigid:2": ‹◇Consistent(x) ≡ Consistent(x)›
1208proof(rule "≡I"; rule "→I")
1209 AOT_assume 0: ‹◇Consistent(x)›
1210 AOT_have ‹◇(Situation(x) & ¬∃p (x ⊨ p & x ⊨ ¬p))›
1211 apply (AOT_subst ‹Situation(x) & ¬∃p (x ⊨ p & x ⊨ ¬p)› ‹Consistent(x)›)
1212 using cons "≡E"(2) "Commutativity of ≡" "≡Df" apply blast
1213 by (simp add: 0)
1214 AOT_hence ‹◇Situation(x)› and 1: ‹◇¬∃p (x ⊨ p & x ⊨ ¬p)›
1215 using "RM◇" "Conjunction Simplification"(1) "Conjunction Simplification"(2)
1216 "modus-tollens:1" "raa-cor:3" by blast+
1217 AOT_hence 2: ‹Situation(x)› by (metis "≡E"(1) "possit-sit:2")
1218 AOT_have 3: ‹¬□∃p (x ⊨ p & x ⊨ ¬p)›
1219 using 2 using 1 "KBasic:11" "≡E"(2) by blast
1220 AOT_show ‹Consistent(x)›
1221 proof (rule "raa-cor:1")
1222 AOT_assume ‹¬Consistent(x)›
1223 AOT_hence ‹∃p (x ⊨ p & x ⊨ ¬p)›
1224 using 0 "≡⇩d⇩fE" "conventions:5" 2 "cons-rigid:1"[unconstrain s, THEN "→E"]
1225 "modus-tollens:1" "raa-cor:3" "≡E"(4) by meson
1226 then AOT_obtain p where ‹x ⊨ p› and 4: ‹x ⊨ ¬p›
1227 using "∃E"[rotated] "&E" by blast
1228 AOT_hence ‹□x ⊨ p›
1229 by (metis "2" "≡E"(1) "lem2:1"[unconstrain s, THEN "→E"])
1230 moreover AOT_have ‹□x ⊨ ¬p›
1231 using 4 "lem2:1"[unconstrain s, unvarify p, THEN "→E"]
1232 by (metis 2 "≡E"(1) "log-prop-prop:2")
1233 ultimately AOT_have ‹□(x ⊨ p & x ⊨ ¬p)›
1234 by (metis "KBasic:3" "&I" "≡E"(3) "raa-cor:3")
1235 AOT_hence ‹∃p □(x ⊨ p & x ⊨ ¬p)›
1236 by (metis "existential:1" "log-prop-prop:2")
1237 AOT_hence ‹□∃p (x ⊨ p & x ⊨ ¬p)›
1238 by (metis Buridan "vdash-properties:10")
1239 AOT_thus ‹p & ¬p› for p
1240 using 3 "&I" by (metis "raa-cor:3")
1241 qed
1242next
1243 AOT_show ‹◇Consistent(x)› if ‹Consistent(x)›
1244 using "T◇" that "vdash-properties:10" by blast
1245qed
1246
1247AOT_define possible :: ‹τ ⇒ φ› (‹Possible'(_')›)
1248 pos: ‹Possible(s) ≡⇩d⇩f ◇Actual(s)›
1249
1250AOT_theorem "sit-pos:1": ‹Actual(s) → Possible(s)›
1251 apply(rule "→I"; rule pos[THEN "≡⇩d⇩fI"]; rule "&I")
1252 apply (meson "≡⇩d⇩fE" actual "&E"(1))
1253 using "T◇" "vdash-properties:10" by blast
1254
1255AOT_theorem "sit-pos:2": ‹∃p ((s ⊨ p) & ¬◇p) → ¬Possible(s)›
1256proof(rule "→I")
1257 AOT_assume ‹∃p ((s ⊨ p) & ¬◇p)›
1258 then AOT_obtain p where a: ‹(s ⊨ p) & ¬◇p›
1259 using "∃E"[rotated] by blast
1260 AOT_hence ‹□(s ⊨ p)›
1261 using "&E" by (metis "T◇" "≡E"(1) "lem2:3" "vdash-properties:10")
1262 moreover AOT_have ‹□¬p›
1263 using a[THEN "&E"(2)] by (metis "KBasic2:1" "≡E"(2))
1264 ultimately AOT_have ‹□(s ⊨ p & ¬p)›
1265 by (metis "KBasic:3" "&I" "≡E"(3) "raa-cor:3")
1266 AOT_hence ‹∃p □(s ⊨ p & ¬p)›
1267 by (rule "∃I")
1268 AOT_hence 1: ‹□∃q (s ⊨ q & ¬q)›
1269 by (metis Buridan "vdash-properties:10")
1270 AOT_have ‹□¬∀q (s ⊨ q → q)›
1271 apply (AOT_subst ‹s ⊨ q → q› ‹¬(s ⊨ q & ¬q)› for: q)
1272 apply (simp add: "oth-class-taut:1:a")
1273 apply (AOT_subst ‹¬∀q ¬(s ⊨ q & ¬q)› ‹∃q (s ⊨ q & ¬q)›)
1274 by (auto simp: "conventions:4" "df-rules-formulas[3]" "df-rules-formulas[4]" "≡I" 1)
1275 AOT_hence 0: ‹¬◇∀q (s ⊨ q → q)›
1276 by (metis "≡⇩d⇩fE" "conventions:5" "raa-cor:3")
1277 AOT_show ‹¬Possible(s)›
1278 apply (AOT_subst ‹Possible(s)› ‹Situation(s) & ◇Actual(s)›)
1279 apply (simp add: pos "≡Df")
1280 apply (AOT_subst ‹Actual(s)› ‹Situation(s) & ∀q (s ⊨ q → q)›)
1281 using actual "≡Df" apply presburger
1282 by (metis "0" "KBasic2:3" "&E"(2) "raa-cor:3" "vdash-properties:10")
1283qed
1284
1285AOT_theorem "pos-cons-sit:1": ‹Possible(s) → Consistent(s)›
1286 by (auto simp: "sit-cons"[THEN "RM◇", THEN "→E",
1287 THEN "cons-rigid:2"[THEN "≡E"(1)]]
1288 intro!: "→I" dest!: pos[THEN "≡⇩d⇩fE"] "&E"(2))
1289
1290AOT_theorem "pos-cons-sit:2": ‹∃s (Consistent(s) & ¬Possible(s))›
1291proof -
1292 AOT_obtain q⇩1 where ‹q⇩1 & ◇¬q⇩1›
1293 using "≡⇩d⇩fE" "instantiation" "cont-tf:1" "cont-tf-thm:1" by blast
1294 have "cond-prop": ‹ConditionOnPropositionalProperties
1295 (λ Π . «Π = [λy q⇩1 & ¬q⇩1]»)›
1296 by (auto intro!: "cond-prop[I]" GEN "→I" "prop-prop1"[THEN "≡⇩d⇩fI"]
1297 "∃I"(1)[where τ=‹«q⇩1 & ¬q⇩1»›, rotated, OF "log-prop-prop:2"])
1298 have rigid: ‹rigid_condition (λ Π . «Π = [λy q⇩1 & ¬q⇩1]»)›
1299 by (auto intro!: "strict-can:1[I]" GEN "→I" simp: "id-nec:2"[THEN "→E"])
1300
1301 AOT_obtain x where x_prop: ‹x = ❙ιs (∀F (s[F] ≡ F = [λy q⇩1 & ¬q⇩1]))›
1302 using "ex:1:b"[THEN "∀E"(1), OF "can-sit-desc:1", OF "cond-prop"]
1303 "∃E"[rotated] by blast
1304 AOT_hence 0: ‹❙𝒜(Situation(x) & ∀F (x[F] ≡ F = [λy q⇩1 & ¬q⇩1]))›
1305 using "→E" "actual-desc:2" by blast
1306 AOT_hence ‹❙𝒜(Situation(x))› by (metis "Act-Basic:2" "&E"(1) "≡E"(1))
1307 AOT_hence s_sit: ‹Situation(x)› by (metis "≡E"(1) "possit-sit:4")
1308 AOT_have s_enc_prop: ‹∀F (x[F] ≡ F = [λy q⇩1 & ¬q⇩1])›
1309 using "strict-sit"[OF rigid, OF "cond-prop", THEN "→E", OF x_prop].
1310 AOT_hence ‹x[λy q⇩1 & ¬q⇩1]›
1311 using "∀E"(1)[rotated, OF "prop-prop2:2"]
1312 "rule=I:1"[OF "prop-prop2:2"] "≡E" by blast
1313 AOT_hence ‹x ⊨ (q⇩1 & ¬q⇩1)›
1314 using lem1[THEN "→E", OF s_sit, unvarify p, THEN "≡E"(2), OF "log-prop-prop:2"]
1315 by blast
1316 AOT_hence ‹□(x ⊨ (q⇩1 & ¬q⇩1))›
1317 using "lem2:1"[unconstrain s, THEN "→E", OF s_sit, unvarify p,
1318 OF "log-prop-prop:2", THEN "≡E"(1)] by blast
1319 moreover AOT_have ‹□(x ⊨ (q⇩1 & ¬q⇩1) → ¬Actual(x))›
1320 proof(rule RN; rule "→I"; rule "raa-cor:2")
1321 AOT_modally_strict {
1322 AOT_assume ‹Actual(x)›
1323 AOT_hence ‹∀p (x ⊨ p → p)›
1324 using actual[THEN "≡⇩d⇩fE", THEN "&E"(2)] by blast
1325 moreover AOT_assume ‹x ⊨ (q⇩1 & ¬q⇩1)›
1326 ultimately AOT_show ‹q⇩1 & ¬q⇩1›
1327 using "∀E"(1)[rotated, OF "log-prop-prop:2"] "→E" by metis
1328 }
1329 qed
1330 ultimately AOT_have nec_not_actual_s: ‹□¬Actual(x)›
1331 using "qml:1"[axiom_inst, THEN "→E", THEN "→E"] by blast
1332 AOT_have 1: ‹¬∃p (x ⊨ p & x ⊨ ¬p)›
1333 proof (rule "raa-cor:2")
1334 AOT_assume ‹∃p (x ⊨ p & x ⊨ ¬p)›
1335 then AOT_obtain p where ‹x ⊨ p & x ⊨ ¬p›
1336 using "∃E"[rotated] by blast
1337 AOT_hence ‹x[λy p] & x[λy ¬p]›
1338 using lem1[unvarify p, THEN "→E", OF "log-prop-prop:2",
1339 OF s_sit, THEN "≡E"(1)] "&I" "&E" by metis
1340 AOT_hence ‹[λy p] = [λy q⇩1 & ¬q⇩1]› and ‹[λy ¬p] = [λy q⇩1 & ¬q⇩1]›
1341 by (auto intro!: "prop-prop2:2" s_enc_prop[THEN "∀E"(1), THEN "≡E"(1)]
1342 elim: "&E")
1343 AOT_hence i: ‹[λy p] = [λy ¬p]› by (metis "rule=E" id_sym)
1344 {
1345 AOT_assume 0: ‹p›
1346 AOT_have ‹[λy p]x› for x
1347 by (auto intro!: "β←C"(1) "cqt:2" 0)
1348 AOT_hence ‹[λy ¬p]x› for x using i "rule=E" by fast
1349 AOT_hence ‹¬p›
1350 using "β→C"(1) by auto
1351 }
1352 moreover {
1353 AOT_assume 0: ‹¬p›
1354 AOT_have ‹[λy ¬p]x› for x
1355 by (auto intro!: "β←C"(1) "cqt:2" 0)
1356 AOT_hence ‹[λy p]x› for x using i[symmetric] "rule=E" by fast
1357 AOT_hence ‹p›
1358 using "β→C"(1) by auto
1359 }
1360 ultimately AOT_show ‹p & ¬p› for p by (metis "raa-cor:1" "raa-cor:3")
1361 qed
1362 AOT_have 2: ‹¬Possible(x)›
1363 proof(rule "raa-cor:2")
1364 AOT_assume ‹Possible(x)›
1365 AOT_hence ‹◇Actual(x)›
1366 by (metis "≡⇩d⇩fE" "&E"(2) pos)
1367 moreover AOT_have ‹¬◇Actual(x)› using nec_not_actual_s
1368 using "≡⇩d⇩fE" "conventions:5" "reductio-aa:2" by blast
1369 ultimately AOT_show ‹◇Actual(x) & ¬◇Actual(x)› by (rule "&I")
1370 qed
1371 show ?thesis
1372 by(rule "∃I"(2)[where β=x]; safe intro!: "&I" 2 s_sit cons[THEN "≡⇩d⇩fI"] 1)
1373qed
1374
1375AOT_theorem "sit-classical:1": ‹∀p (s ⊨ p ≡ p) → ∀q(s ⊨ ¬q ≡ ¬s ⊨ q)›
1376proof(rule "→I"; rule GEN)
1377 fix q
1378 AOT_assume ‹∀p (s ⊨ p ≡ p)›
1379 AOT_hence ‹s ⊨ q ≡ q› and ‹s ⊨ ¬q ≡ ¬q›
1380 using "∀E"(1)[rotated, OF "log-prop-prop:2"] by blast+
1381 AOT_thus ‹s ⊨ ¬q ≡ ¬s ⊨ q›
1382 by (metis "deduction-theorem" "≡I" "≡E"(1) "≡E"(2) "≡E"(4))
1383qed
1384
1385AOT_theorem "sit-classical:2":
1386 ‹∀p (s ⊨ p ≡ p) → ∀q∀r((s ⊨ (q → r)) ≡ (s ⊨ q → s ⊨ r))›
1387proof(rule "→I"; rule GEN; rule GEN)
1388 fix q r
1389 AOT_assume ‹∀p (s ⊨ p ≡ p)›
1390 AOT_hence θ: ‹s ⊨ q ≡ q› and ξ: ‹s ⊨ r ≡ r› and ζ: ‹(s ⊨ (q → r)) ≡ (q → r)›
1391 using "∀E"(1)[rotated, OF "log-prop-prop:2"] by blast+
1392 AOT_show ‹(s ⊨ (q → r)) ≡ (s ⊨ q → s ⊨ r)›
1393 proof (safe intro!: "≡I" "→I")
1394 AOT_assume ‹s ⊨ (q → r)›
1395 moreover AOT_assume ‹s ⊨ q›
1396 ultimately AOT_show ‹s ⊨ r›
1397 using θ ξ ζ by (metis "≡E"(1) "≡E"(2) "vdash-properties:10")
1398 next
1399 AOT_assume ‹s ⊨ q → s ⊨ r›
1400 AOT_thus ‹s ⊨ (q → r)›
1401 using θ ξ ζ by (metis "deduction-theorem" "≡E"(1) "≡E"(2) "→E")
1402 qed
1403qed
1404
1405AOT_theorem "sit-classical:3":
1406 ‹∀p (s ⊨ p ≡ p) → ((s ⊨ ∀α φ{α}) ≡ ∀α s ⊨ φ{α})›
1407proof (rule "→I")
1408 AOT_assume ‹∀p (s ⊨ p ≡ p)›
1409 AOT_hence θ: ‹s ⊨ φ{α} ≡ φ{α}› and ξ: ‹s ⊨ ∀α φ{α} ≡ ∀α φ{α}› for α
1410 using "∀E"(1)[rotated, OF "log-prop-prop:2"] by blast+
1411 AOT_show ‹s ⊨ ∀α φ{α} ≡ ∀α s ⊨ φ{α}›
1412 proof (safe intro!: "≡I" "→I" GEN)
1413 fix α
1414 AOT_assume ‹s ⊨ ∀α φ{α}›
1415 AOT_hence ‹φ{α}› using ξ "∀E"(2) "≡E"(1) by blast
1416 AOT_thus ‹s ⊨ φ{α}› using θ "≡E"(2) by blast
1417 next
1418 AOT_assume ‹∀α s ⊨ φ{α}›
1419 AOT_hence ‹s ⊨ φ{α}› for α using "∀E"(2) by blast
1420 AOT_hence ‹φ{α}› for α using θ "≡E"(1) by blast
1421 AOT_hence ‹∀α φ{α}› by (rule GEN)
1422 AOT_thus ‹s ⊨ ∀α φ{α}› using ξ "≡E"(2) by blast
1423 qed
1424qed
1425
1426AOT_theorem "sit-classical:4": ‹∀p (s ⊨ p ≡ p) → ∀q (s ⊨ □q → □s ⊨ q)›
1427proof(rule "→I"; rule GEN; rule "→I")
1428 fix q
1429 AOT_assume ‹∀p (s ⊨ p ≡ p)›
1430 AOT_hence θ: ‹s ⊨ q ≡ q› and ξ: ‹s ⊨ □q ≡ □q›
1431 using "∀E"(1)[rotated, OF "log-prop-prop:2"] by blast+
1432 AOT_assume ‹s ⊨ □q›
1433 AOT_hence ‹□q› using ξ "≡E"(1) by blast
1434 AOT_hence ‹q› using "qml:2"[axiom_inst, THEN "→E"] by blast
1435 AOT_hence ‹s ⊨ q› using θ "≡E"(2) by blast
1436 AOT_thus ‹□s ⊨ q› using "≡⇩d⇩fE" "&E"(1) "≡E"(1) "lem2:1" "true-in-s" by blast
1437qed
1438
1439AOT_theorem "sit-classical:5":
1440 ‹∀p (s ⊨ p ≡ p) → ∃q(□(s ⊨ q) & ¬(s ⊨ □ q))›
1441proof (rule "→I")
1442 AOT_obtain r where A: ‹r› and ‹◇¬r›
1443 by (metis "&E"(1) "&E"(2) "≡⇩d⇩fE" "instantiation" "cont-tf:1" "cont-tf-thm:1")
1444 AOT_hence B: ‹¬□r›
1445 using "KBasic:11" "≡E"(2) by blast
1446 moreover AOT_assume asm: ‹∀ p (s ⊨ p ≡ p)›
1447 AOT_hence ‹s ⊨ r›
1448 using "∀E"(2) A "≡E"(2) by blast
1449 AOT_hence 1: ‹□s ⊨ r›
1450 using "≡⇩d⇩fE" "&E"(1) "≡E"(1) "lem2:1" "true-in-s" by blast
1451 AOT_have ‹s ⊨ ¬□r›
1452 using asm[THEN "∀E"(1)[rotated, OF "log-prop-prop:2"], THEN "≡E"(2)] B by blast
1453 AOT_hence ‹¬s ⊨ □r›
1454 using "sit-classical:1"[THEN "→E", OF asm,
1455 THEN "∀E"(1)[rotated, OF "log-prop-prop:2"], THEN "≡E"(1)] by blast
1456 AOT_hence ‹□s ⊨ r & ¬s ⊨ □r›
1457 using 1 "&I" by blast
1458 AOT_thus ‹∃r (□s ⊨ r & ¬s ⊨ □r)›
1459 by (rule "∃I")
1460qed
1461
1462AOT_theorem "sit-classical:6":
1463 ‹∃s ∀p (s ⊨ p ≡ p)›
1464proof -
1465 have "cond-prop": ‹ConditionOnPropositionalProperties
1466 (λ Π . «∃q (q & Π = [λy q])»)›
1467 proof (safe intro!: "cond-prop[I]" GEN "→I")
1468 fix F
1469 AOT_modally_strict {
1470 AOT_assume ‹∃q (q & F = [λy q])›
1471 then AOT_obtain q where ‹q & F = [λy q]›
1472 using "∃E"[rotated] by blast
1473 AOT_hence ‹F = [λy q]›
1474 using "&E" by blast
1475 AOT_hence ‹∃q F = [λy q]›
1476 by (rule "∃I")
1477 AOT_thus ‹Propositional([F])›
1478 by (metis "≡⇩d⇩fI" "prop-prop1")
1479 }
1480 qed
1481 AOT_have ‹∃s ∀F (s[F] ≡ ∃q (q & F = [λy q]))›
1482 using "comp-sit:1"[OF "cond-prop"].
1483 then AOT_obtain s⇩0 where s⇩0_prop: ‹∀F (s⇩0[F] ≡ ∃q (q & F = [λy q]))›
1484 using "Situation.∃E"[rotated] by meson
1485 AOT_have ‹∀p (s⇩0 ⊨ p ≡ p)›
1486 proof(safe intro!: GEN "≡I" "→I")
1487 fix p
1488 AOT_assume ‹s⇩0 ⊨ p›
1489 AOT_hence ‹s⇩0[λy p]›
1490 using lem1[THEN "→E", OF Situation.ψ, THEN "≡E"(1)] by blast
1491 AOT_hence ‹∃q (q & [λy p] = [λy q])›
1492 using s⇩0_prop[THEN "∀E"(1)[rotated, OF "prop-prop2:2"], THEN "≡E"(1)] by blast
1493 then AOT_obtain q⇩1 where q⇩1_prop: ‹q⇩1 & [λy p] = [λy q⇩1]›
1494 using "∃E"[rotated] by blast
1495 AOT_hence ‹p = q⇩1›
1496 by (metis "&E"(2) "≡E"(2) "p-identity-thm2:3")
1497 AOT_thus ‹p›
1498 using q⇩1_prop[THEN "&E"(1)] "rule=E" id_sym by fast
1499 next
1500 fix p
1501 AOT_assume ‹p›
1502 moreover AOT_have ‹[λy p] = [λy p]›
1503 by (simp add: "rule=I:1"[OF "prop-prop2:2"])
1504 ultimately AOT_have ‹p & [λy p] = [λy p]›
1505 using "&I" by blast
1506 AOT_hence ‹∃q (q & [λy p] = [λy q])›
1507 by (rule "∃I")
1508 AOT_hence ‹s⇩0[λy p]›
1509 using s⇩0_prop[THEN "∀E"(1)[rotated, OF "prop-prop2:2"], THEN "≡E"(2)] by blast
1510 AOT_thus ‹s⇩0 ⊨ p›
1511 using lem1[THEN "→E", OF Situation.ψ, THEN "≡E"(2)] by blast
1512 qed
1513 AOT_hence ‹∀p (s⇩0 ⊨ p ≡ p)›
1514 using "&I" by blast
1515 AOT_thus ‹∃s ∀p (s ⊨ p ≡ p)›
1516 by (rule "Situation.∃I")
1517qed
1518
1519AOT_define PossibleWorld :: ‹τ ⇒ φ› (‹PossibleWorld'(_')›)
1520 "world:1": ‹PossibleWorld(x) ≡⇩d⇩f Situation(x) & ◇∀p(x ⊨ p ≡ p)›
1521
1522AOT_theorem "world:2": ‹∃x PossibleWorld(x)›
1523proof -
1524 AOT_obtain s where s_prop: ‹∀p (s ⊨ p ≡ p)›
1525 using "sit-classical:6" "Situation.∃E"[rotated] by meson
1526 AOT_have ‹∀p (s ⊨ p ≡ p)›
1527 proof(safe intro!: GEN "≡I" "→I")
1528 fix p
1529 AOT_assume ‹s ⊨ p›
1530 AOT_thus ‹p›
1531 using s_prop[THEN "∀E"(2), THEN "≡E"(1)] by blast
1532 next
1533 fix p
1534 AOT_assume ‹p›
1535 AOT_thus ‹s ⊨ p›
1536 using s_prop[THEN "∀E"(2), THEN "≡E"(2)] by blast
1537 qed
1538 AOT_hence ‹◇∀p (s ⊨ p ≡ p)›
1539 by (metis "T◇"[THEN "→E"])
1540 AOT_hence ‹◇∀p (s ⊨ p ≡ p)›
1541 using s_prop "&I" by blast
1542 AOT_hence ‹PossibleWorld(s)›
1543 using "world:1"[THEN "≡⇩d⇩fI"] Situation.ψ "&I" by blast
1544 AOT_thus ‹∃x PossibleWorld(x)›
1545 by (rule "∃I")
1546qed
1547
1548AOT_theorem "world:3": ‹PossibleWorld(κ) → κ↓›
1549proof (rule "→I")
1550 AOT_assume ‹PossibleWorld(κ)›
1551 AOT_hence ‹Situation(κ)›
1552 using "world:1"[THEN "≡⇩d⇩fE"] "&E" by blast
1553 AOT_hence ‹A!κ›
1554 by (metis "≡⇩d⇩fE" "&E"(1) situations)
1555 AOT_thus ‹κ↓›
1556 by (metis "russell-axiom[exe,1].ψ_denotes_asm")
1557qed
1558
1559AOT_theorem "rigid-pw:1": ‹PossibleWorld(x) ≡ □PossibleWorld(x)›
1560proof(safe intro!: "≡I" "→I")
1561 AOT_assume ‹PossibleWorld(x)›
1562 AOT_hence ‹Situation(x) & ◇∀p(x ⊨ p ≡ p)›
1563 using "world:1"[THEN "≡⇩d⇩fE"] by blast
1564 AOT_hence ‹□Situation(x) & □◇∀p(x ⊨ p ≡ p)›
1565 by (metis "S5Basic:1" "&I" "&E"(1) "&E"(2) "≡E"(1) "possit-sit:1")
1566 AOT_hence 0: ‹□(Situation(x) & ◇∀p(x ⊨ p ≡ p))›
1567 by (metis "KBasic:3" "≡E"(2))
1568 AOT_show ‹□PossibleWorld(x)›
1569 by (AOT_subst ‹PossibleWorld(x)› ‹Situation(x) & ◇∀p(x ⊨ p ≡ p)›)
1570 (auto simp: "≡Df" "world:1" 0)
1571next
1572 AOT_show ‹PossibleWorld(x)› if ‹□PossibleWorld(x)›
1573 using that "qml:2"[axiom_inst, THEN "→E"] by blast
1574qed
1575
1576AOT_theorem "rigid-pw:2": ‹◇PossibleWorld(x) ≡ PossibleWorld(x)›
1577 using "rigid-pw:1"
1578 by (meson "RE◇" "S5Basic:2" "≡E"(2) "≡E"(6) "Commutativity of ≡")
1579
1580AOT_theorem "rigid-pw:3": ‹◇PossibleWorld(x) ≡ □PossibleWorld(x)›
1581 using "rigid-pw:1" "rigid-pw:2" by (meson "≡E"(5))
1582
1583AOT_theorem "rigid-pw:4": ‹❙𝒜PossibleWorld(x) ≡ PossibleWorld(x)›
1584 by (metis "Act-Sub:3" "→I" "≡I" "≡E"(6) "nec-imp-act" "rigid-pw:1" "rigid-pw:2")
1585
1586AOT_register_rigid_restricted_type
1587 PossibleWorld: ‹PossibleWorld(κ)›
1588proof
1589 AOT_modally_strict {
1590 AOT_show ‹∃x PossibleWorld(x)› using "world:2".
1591 }
1592next
1593 AOT_modally_strict {
1594 AOT_show ‹PossibleWorld(κ) → κ↓› for κ using "world:3".
1595 }
1596next
1597 AOT_modally_strict {
1598 AOT_show ‹∀α(PossibleWorld(α) → □PossibleWorld(α))›
1599 by (meson GEN "→I" "≡E"(1) "rigid-pw:1")
1600 }
1601qed
1602AOT_register_variable_names
1603 PossibleWorld: w
1604
1605AOT_theorem "world-pos": ‹Possible(w)›
1606proof (safe intro!: "≡⇩d⇩fE"[OF "world:1", OF PossibleWorld.ψ, THEN "&E"(1)]
1607 pos[THEN "≡⇩d⇩fI"] "&I" )
1608 AOT_have ‹◇∀p (w ⊨ p ≡ p)›
1609 using "world:1"[THEN "≡⇩d⇩fE", OF PossibleWorld.ψ, THEN "&E"(2)].
1610 AOT_hence ‹◇∀p (w ⊨ p → p)›
1611 proof (rule "RM◇"[THEN "→E", rotated]; safe intro!: "→I" GEN)
1612 AOT_modally_strict {
1613 fix p
1614 AOT_assume ‹∀p (w ⊨ p ≡ p)›
1615 AOT_hence ‹w ⊨ p ≡ p› using "∀E"(2) by blast
1616 moreover AOT_assume ‹w ⊨ p›
1617 ultimately AOT_show p using "≡E"(1) by blast
1618 }
1619 qed
1620 AOT_hence 0: ‹◇(Situation(w) & ∀p (w ⊨ p → p))›
1621 using "world:1"[THEN "≡⇩d⇩fE", OF PossibleWorld.ψ, THEN "&E"(1),
1622 THEN "possit-sit:1"[THEN "≡E"(1)]]
1623 by (metis "KBasic:16" "&I" "vdash-properties:10")
1624 AOT_show ‹◇Actual(w)›
1625 by (AOT_subst ‹Actual(w)› ‹Situation(w) & ∀p (w ⊨ p → p)›)
1626 (auto simp: actual "≡Df" 0)
1627qed
1628
1629AOT_theorem "world-cons:1": ‹Consistent(w)›
1630 using "world-pos"
1631 using "pos-cons-sit:1"[unconstrain s, THEN "→E", THEN "→E"]
1632 by (meson "≡⇩d⇩fE" "&E"(1) pos)
1633
1634AOT_theorem "world-cons:2": ‹¬TrivialSituation(w)›
1635proof(rule "raa-cor:2")
1636 AOT_assume ‹TrivialSituation(w)›
1637 AOT_hence ‹Situation(w) & ∀p w ⊨ p›
1638 using "df-null-trivial:2"[THEN "≡⇩d⇩fE"] by blast
1639 AOT_hence 0: ‹□w ⊨ (∃p (p & ¬p))›
1640 using "&E"
1641 by (metis "Buridan◇" "T◇" "&E"(2) "≡E"(1) "lem2:3"[unconstrain s, THEN "→E"]
1642 "log-prop-prop:2" "rule-ui:1" "universal-cor" "→E")
1643 AOT_have ‹◇∀p (w ⊨ p ≡ p)›
1644 using PossibleWorld.ψ "world:1"[THEN "≡⇩d⇩fE", THEN "&E"(2)] by metis
1645 AOT_hence ‹∀p ◇(w ⊨ p ≡ p)›
1646 using "Buridan◇"[THEN "→E"] by blast
1647 AOT_hence ‹◇(w ⊨ (∃p (p & ¬p)) ≡ (∃p (p & ¬p)))›
1648 by (metis "log-prop-prop:2" "rule-ui:1")
1649 AOT_hence ‹◇(w ⊨ (∃p (p & ¬p)) → (∃p (p & ¬p)))›
1650 using "RM◇"[THEN "→E"] "→I" "≡E"(1) by meson
1651 AOT_hence ‹◇(∃p (p & ¬p))› using 0
1652 by (metis "KBasic2:4" "≡E"(1) "→E")
1653 moreover AOT_have ‹¬◇(∃p (p & ¬p))›
1654 by (metis "instantiation" "KBasic2:1" RN "≡E"(1) "raa-cor:2")
1655 ultimately AOT_show ‹◇(∃p (p & ¬p)) & ¬◇(∃p (p & ¬p))›
1656 using "&I" by blast
1657qed
1658
1659AOT_theorem "rigid-truth-at:1": ‹w ⊨ p ≡ □w ⊨ p›
1660 using "lem2:1"[unconstrain s, THEN "→E",
1661 OF PossibleWorld.ψ[THEN "world:1"[THEN "≡⇩d⇩fE"], THEN "&E"(1)]].
1662
1663AOT_theorem "rigid-truth-at:2": ‹◇w ⊨ p ≡ w ⊨ p›
1664 using "lem2:2"[unconstrain s, THEN "→E",
1665 OF PossibleWorld.ψ[THEN "world:1"[THEN "≡⇩d⇩fE"], THEN "&E"(1)]].
1666
1667AOT_theorem "rigid-truth-at:3": ‹◇w ⊨ p ≡ □w ⊨ p›
1668 using "lem2:3"[unconstrain s, THEN "→E",
1669 OF PossibleWorld.ψ[THEN "world:1"[THEN "≡⇩d⇩fE"], THEN "&E"(1)]].
1670
1671AOT_theorem "rigid-truth-at:4": ‹❙𝒜w ⊨ p ≡ w ⊨ p›
1672 using "lem2:4"[unconstrain s, THEN "→E",
1673 OF PossibleWorld.ψ[THEN "world:1"[THEN "≡⇩d⇩fE"], THEN "&E"(1)]].
1674
1675AOT_theorem "rigid-truth-at:5": ‹¬w ⊨ p ≡ □¬w ⊨ p›
1676 using "lem2:5"[unconstrain s, THEN "→E",
1677 OF PossibleWorld.ψ[THEN "world:1"[THEN "≡⇩d⇩fE"], THEN "&E"(1)]].
1678
1679AOT_define Maximal :: ‹τ ⇒ φ› (‹Maximal'(_')›)
1680 max: ‹Maximal(s) ≡⇩d⇩f ∀p (s ⊨ p ∨ s ⊨ ¬p)›
1681
1682AOT_theorem "world-max": ‹Maximal(w)›
1683proof(safe intro!: PossibleWorld.ψ[THEN "≡⇩d⇩fE"[OF "world:1"], THEN "&E"(1)]
1684 GEN "≡⇩d⇩fI"[OF max] "&I" )
1685 fix q
1686 AOT_have ‹◇(w ⊨ q ∨ w ⊨ ¬q)›
1687 proof(rule "RM◇"[THEN "→E"]; (rule "→I")?)
1688 AOT_modally_strict {
1689 AOT_assume ‹∀p (w ⊨ p ≡ p)›
1690 AOT_hence ‹w ⊨ q ≡ q› and ‹w ⊨ ¬q ≡ ¬q›
1691 using "∀E"(1)[rotated, OF "log-prop-prop:2"] by blast+
1692 AOT_thus ‹w ⊨ q ∨ w ⊨ ¬q›
1693 by (metis "∨I"(1) "∨I"(2) "≡E"(3) "reductio-aa:1")
1694 }
1695 next
1696 AOT_show ‹◇∀p (w ⊨ p ≡ p)›
1697 using PossibleWorld.ψ[THEN "≡⇩d⇩fE"[OF "world:1"], THEN "&E"(2)].
1698 qed
1699 AOT_hence ‹◇w ⊨ q ∨ ◇w ⊨ ¬q›
1700 using "KBasic2:2"[THEN "≡E"(1)] by blast
1701 AOT_thus ‹w ⊨ q ∨ w ⊨ ¬q›
1702 using "lem2:2"[unconstrain s, THEN "→E", unvarify p,
1703 OF PossibleWorld.ψ[THEN "≡⇩d⇩fE"[OF "world:1"], THEN "&E"(1)],
1704 THEN "≡E"(1), OF "log-prop-prop:2"]
1705 by (metis "∨I"(1) "∨I"(2) "∨E"(3) "raa-cor:2")
1706qed
1707
1708AOT_theorem "world=maxpos:1": ‹Maximal(x) → □Maximal(x)›
1709proof (AOT_subst ‹Maximal(x)› ‹Situation(x) & ∀p (x ⊨ p ∨ x ⊨ ¬p)›;
1710 safe intro!: max "≡Df" "→I"; frule "&E"(1); drule "&E"(2))
1711 AOT_assume sit_x: ‹Situation(x)›
1712 AOT_hence nec_sit_x: ‹□Situation(x)›
1713 by (metis "≡E"(1) "possit-sit:1")
1714 AOT_assume ‹∀p (x ⊨ p ∨ x ⊨ ¬p)›
1715 AOT_hence ‹x ⊨ p ∨ x ⊨ ¬p› for p
1716 using "∀E"(1)[rotated, OF "log-prop-prop:2"] by blast
1717 AOT_hence ‹□x ⊨ p ∨ □x ⊨ ¬p› for p
1718 using "lem2:1"[unconstrain s, THEN "→E", OF sit_x, unvarify p,
1719 OF "log-prop-prop:2", THEN "≡E"(1)]
1720 by (metis "∨I"(1) "∨I"(2) "∨E"(2) "raa-cor:1")
1721 AOT_hence ‹□(x ⊨ p ∨ x ⊨ ¬p)› for p
1722 by (metis "KBasic:15" "→E")
1723 AOT_hence ‹∀p □(x ⊨ p ∨ x ⊨ ¬p)›
1724 by (rule GEN)
1725 AOT_hence ‹□∀p (x ⊨ p ∨ x ⊨ ¬p)›
1726 by (rule BF[THEN "→E"])
1727 AOT_thus ‹□(Situation(x) & ∀p (x ⊨ p ∨ x ⊨ ¬p))›
1728 using nec_sit_x by (metis "KBasic:3" "&I" "≡E"(2))
1729qed
1730
1731AOT_theorem "world=maxpos:2": ‹PossibleWorld(x) ≡ Maximal(x) & Possible(x)›
1732proof(safe intro!: "≡I" "→I" "&I" "world-pos"[unconstrain w, THEN "→E"]
1733 "world-max"[unconstrain w, THEN "→E"];
1734 frule "&E"(2); drule "&E"(1))
1735 AOT_assume pos_x: ‹Possible(x)›
1736 AOT_have ‹◇(Situation(x) & ∀p(x ⊨ p → p))›
1737 apply (AOT_subst (reverse) ‹Situation(x) & ∀p(x ⊨ p → p)› ‹Actual(x)›)
1738 using actual "≡Df" apply presburger
1739 using "≡⇩d⇩fE" "&E"(2) pos pos_x by blast
1740 AOT_hence 0: ‹◇∀p(x ⊨ p → p)›
1741 by (metis "KBasic2:3" "&E"(2) "vdash-properties:6")
1742 AOT_assume max_x: ‹Maximal(x)›
1743 AOT_hence sit_x: ‹Situation(x)› by (metis "≡⇩d⇩fE" max_x "&E"(1) max)
1744 AOT_have ‹□Maximal(x)› using "world=maxpos:1"[THEN "→E", OF max_x] by simp
1745 moreover AOT_have ‹□Maximal(x) → □(∀p(x ⊨ p → p) → ∀p (x ⊨ p ≡ p))›
1746 proof(safe intro!: "→I" RM GEN)
1747 AOT_modally_strict {
1748 fix p
1749 AOT_assume 0: ‹Maximal(x)›
1750 AOT_assume 1: ‹∀p (x ⊨ p → p)›
1751 AOT_show ‹x ⊨ p ≡ p›
1752 proof(safe intro!: "≡I" "→I" 1[THEN "∀E"(2), THEN "→E"]; rule "raa-cor:1")
1753 AOT_assume ‹¬x ⊨ p›
1754 AOT_hence ‹x ⊨ ¬p›
1755 using 0[THEN "≡⇩d⇩fE"[OF max], THEN "&E"(2), THEN "∀E"(2)]
1756 1 by (metis "∨E"(2))
1757 AOT_hence ‹¬p›
1758 using 1[THEN "∀E"(1), OF "log-prop-prop:2", THEN "→E"] by blast
1759 moreover AOT_assume p
1760 ultimately AOT_show ‹p & ¬p› using "&I" by blast
1761 qed
1762 }
1763 qed
1764 ultimately AOT_have ‹□(∀p(x ⊨ p → p) → ∀p (x ⊨ p ≡ p))›
1765 using "→E" by blast
1766 AOT_hence ‹◇∀p(x ⊨ p → p) → ◇∀p(x ⊨ p ≡ p)›
1767 by (metis "KBasic:13"[THEN "→E"])
1768 AOT_hence ‹◇∀p(x ⊨ p ≡ p)›
1769 using 0 "→E" by blast
1770 AOT_thus ‹PossibleWorld(x)›
1771 using "≡⇩d⇩fI"[OF "world:1", OF "&I", OF sit_x] by blast
1772qed
1773
1774AOT_define NecImpl :: ‹φ ⇒ φ ⇒ φ› (infixl ‹⇒› 26)
1775 "nec-impl-p:1": ‹p ⇒ q ≡⇩d⇩f □(p → q)›
1776AOT_define NecEquiv :: ‹φ ⇒ φ ⇒ φ› (infixl ‹⇔› 21)
1777 "nec-impl-p:2": ‹p ⇔ q ≡⇩d⇩f (p ⇒ q) & (q ⇒ p)›
1778
1779AOT_theorem "nec-impl-p:3[rec]": ‹p ⇒ p›
1780 by (safe intro!: "nec-impl-p:1"[THEN "≡⇩d⇩fI"] RN "→I")
1781
1782AOT_theorem "nec-impl-p:3[trans]": ‹((p ⇒ q) & (q ⇒ r)) → p ⇒ r›
1783proof (safe intro!: "nec-impl-p:1"[THEN "≡⇩d⇩fI"] "→I")
1784 AOT_assume ‹(p ⇒ q) & (q ⇒ r)›
1785 AOT_hence ‹□((p → q) & (q → r))›
1786 by (metis "KBasic:3" "≡⇩d⇩fE" "con-dis-i-e:1" "con-dis-i-e:2:a" "con-dis-i-e:2:b" "intro-elim:3:b" "nec-impl-p:1")
1787 moreover AOT_modally_strict {
1788 AOT_have ‹((p → q) & (q → r)) → (p → r)›
1789 by (metis "con-dis-i-e:2:a" "con-dis-i-e:2:b" "deduction-theorem" "vdash-properties:10")
1790 }
1791 ultimately AOT_show ‹□(p → r)›
1792 using "RM:1" "→E" by blast
1793qed
1794
1795AOT_theorem "nec-equiv-nec-im": ‹p ⇔ q ≡ □(p ≡ q)›
1796proof(safe intro!: "≡I" "→I")
1797 AOT_assume ‹p ⇔ q›
1798 AOT_hence ‹(p ⇒ q)› and ‹(q ⇒ p)›
1799 using "nec-impl-p:2"[THEN "≡⇩d⇩fE"] "&E" by blast+
1800 AOT_hence ‹□(p → q)› and ‹□(q → p)›
1801 using "nec-impl-p:1"[THEN "≡⇩d⇩fE"] by blast+
1802 AOT_thus ‹□(p ≡ q)› by (metis "KBasic:4" "&I" "≡E"(2))
1803next
1804 AOT_assume ‹□(p ≡ q)›
1805 AOT_hence ‹□(p → q)› and ‹□(q → p)›
1806 using "KBasic:4" "&E" "≡E"(1) by blast+
1807 AOT_hence ‹(p ⇒ q)› and ‹(q ⇒ p)›
1808 using "nec-impl-p:1"[THEN "≡⇩d⇩fI"] by blast+
1809 AOT_thus ‹p ⇔ q›
1810 using "nec-impl-p:2"[THEN "≡⇩d⇩fI"] "&I" by blast
1811qed
1812
1813
1814AOT_theorem world_closed_lem_1_a:
1815 ‹(s ⊨ (φ & ψ)) → (∀p (s ⊨ p ≡ p) → (s ⊨ φ & s ⊨ ψ))›
1816proof(safe intro!: "→I")
1817 AOT_assume ‹∀ p (s ⊨ p ≡ p)›
1818 AOT_hence ‹s ⊨ (φ & ψ) ≡ (φ & ψ)› and ‹s ⊨ φ ≡ φ› and ‹s ⊨ ψ ≡ ψ›
1819 using "∀E"(1)[rotated, OF "log-prop-prop:2"] by blast+
1820 moreover AOT_assume ‹s ⊨ (φ & ψ)›
1821 ultimately AOT_show ‹s ⊨ φ & s ⊨ ψ›
1822 by (metis "&I" "&E"(1) "&E"(2) "≡E"(1) "≡E"(2))
1823qed
1824
1825AOT_theorem world_closed_lem_1_b:
1826 ‹(s ⊨ φ & (φ → q)) → (∀p (s ⊨ p ≡ p) → s ⊨ q)›
1827proof(safe intro!: "→I")
1828 AOT_assume ‹∀ p (s ⊨ p ≡ p)›
1829 AOT_hence ‹s ⊨ φ ≡ φ› for φ
1830 using "∀E"(1)[rotated, OF "log-prop-prop:2"] by blast
1831 moreover AOT_assume ‹s ⊨ φ & (φ → q)›
1832 ultimately AOT_show ‹s ⊨ q›
1833 by (metis "&E"(1) "&E"(2) "≡E"(1) "≡E"(2) "→E")
1834qed
1835
1836AOT_theorem world_closed_lem_1_c:
1837 ‹(s ⊨ φ & s ⊨ (φ → ψ)) → (∀p (s ⊨ p ≡ p) → s ⊨ ψ)›
1838proof(safe intro!: "→I")
1839 AOT_assume ‹∀ p (s ⊨ p ≡ p)›
1840 AOT_hence ‹s ⊨ φ ≡ φ› for φ
1841 using "∀E"(1)[rotated, OF "log-prop-prop:2"] by blast
1842 moreover AOT_assume ‹s ⊨ φ & s ⊨ (φ → ψ)›
1843 ultimately AOT_show ‹s ⊨ ψ›
1844 by (metis "&E"(1) "&E"(2) "≡E"(1) "≡E"(2) "→E")
1845qed
1846
1847AOT_theorem "world-closed-lem:1[0]":
1848 ‹q → (∀p (s ⊨ p ≡ p) → s ⊨ q)›
1849 by (meson "→I" "≡E"(2) "log-prop-prop:2" "rule-ui:1")
1850
1851AOT_theorem "world-closed-lem:1[1]":
1852 ‹s ⊨ p⇩1 & (p⇩1 → q) → (∀p (s ⊨ p ≡ p) → s ⊨ q)›
1853 using world_closed_lem_1_b.
1854
1855AOT_theorem "world-closed-lem:1[2]":
1856 ‹s ⊨ p⇩1 & s ⊨ p⇩2 & ((p⇩1 & p⇩2) → q) → (∀p (s ⊨ p ≡ p) → s ⊨ q)›
1857 using world_closed_lem_1_b world_closed_lem_1_a
1858 by (metis (full_types) "&I" "&E" "→I" "→E")
1859
1860AOT_theorem "world-closed-lem:1[3]":
1861 ‹s ⊨ p⇩1 & s ⊨ p⇩2 & s ⊨ p⇩3 & ((p⇩1 & p⇩2 & p⇩3) → q) → (∀p (s ⊨ p ≡ p) → s ⊨ q)›
1862 using world_closed_lem_1_b world_closed_lem_1_a
1863 by (metis (full_types) "&I" "&E" "→I" "→E")
1864
1865AOT_theorem "world-closed-lem:1[4]":
1866 ‹s ⊨ p⇩1 & s ⊨ p⇩2 & s ⊨ p⇩3 & s ⊨ p⇩4 & ((p⇩1 & p⇩2 & p⇩3 & p⇩4) → q) →
1867 (∀p (s ⊨ p ≡ p) → s ⊨ q)›
1868 using world_closed_lem_1_b world_closed_lem_1_a
1869 by (metis (full_types) "&I" "&E" "→I" "→E")
1870
1871AOT_theorem "coherent:1": ‹w ⊨ ¬p ≡ ¬w ⊨ p›
1872proof(safe intro!: "≡I" "→I")
1873 AOT_assume 1: ‹w ⊨ ¬p›
1874 AOT_show ‹¬w ⊨ p›
1875 proof(rule "raa-cor:2")
1876 AOT_assume ‹w ⊨ p›
1877 AOT_hence ‹w ⊨ p & w ⊨ ¬p› using 1 "&I" by blast
1878 AOT_hence ‹∃q (w ⊨ q & w ⊨ ¬q)› by (rule "∃I")
1879 moreover AOT_have ‹¬∃q (w ⊨ q & w ⊨ ¬q)›
1880 using "world-cons:1"[THEN "≡⇩d⇩fE"[OF cons], THEN "&E"(2)].
1881 ultimately AOT_show ‹∃q (w ⊨ q & w ⊨ ¬q) & ¬∃q (w ⊨ q & w ⊨ ¬q)›
1882 using "&I" by blast
1883 qed
1884next
1885 AOT_assume ‹¬w ⊨ p›
1886 AOT_thus ‹w ⊨ ¬p›
1887 using "world-max"[THEN "≡⇩d⇩fE"[OF max], THEN "&E"(2)]
1888 by (metis "∨E"(2) "log-prop-prop:2" "rule-ui:1")
1889qed
1890
1891AOT_theorem "coherent:2": ‹w ⊨ p ≡ ¬w ⊨ ¬p›
1892 by (metis "coherent:1" "deduction-theorem" "≡I" "≡E"(1) "≡E"(2) "raa-cor:3")
1893
1894AOT_theorem "act-world:1": ‹∃w ∀p (w ⊨ p ≡ p)›
1895proof -
1896 AOT_obtain s where s_prop: ‹∀p (s ⊨ p ≡ p)›
1897 using "sit-classical:6" "Situation.∃E"[rotated] by meson
1898 AOT_hence ‹◇∀p (s ⊨ p ≡ p)›
1899 by (metis "T◇" "vdash-properties:10")
1900 AOT_hence ‹PossibleWorld(s)›
1901 using "world:1"[THEN "≡⇩d⇩fI"] Situation.ψ "&I" by blast
1902 AOT_hence ‹PossibleWorld(s) & ∀p (s ⊨ p ≡ p)›
1903 using "&I" s_prop by blast
1904 thus ?thesis by (rule "∃I")
1905qed
1906
1907AOT_theorem "act-world:2": ‹∃!w Actual(w)›
1908proof -
1909 AOT_obtain w where w_prop: ‹∀p (w ⊨ p ≡ p)›
1910 using "act-world:1" "PossibleWorld.∃E"[rotated] by meson
1911 AOT_have sit_s: ‹Situation(w)›
1912 using PossibleWorld.ψ "world:1"[THEN "≡⇩d⇩fE", THEN "&E"(1)] by blast
1913 show ?thesis
1914 proof (safe intro!: "uniqueness:1"[THEN "≡⇩d⇩fI"] "∃I"(2) "&I" GEN "→I"
1915 PossibleWorld.ψ actual[THEN "≡⇩d⇩fI"] sit_s
1916 "sit-identity"[unconstrain s, unconstrain s', THEN "→E",
1917 THEN "→E", THEN "≡E"(2)] "≡I"
1918 w_prop[THEN "∀E"(2), THEN "≡E"(1)])
1919 AOT_show ‹PossibleWorld(w)› using PossibleWorld.ψ.
1920 next
1921 AOT_show ‹Situation(w)›
1922 by (simp add: sit_s)
1923 next
1924 fix y p
1925 AOT_assume w_asm: ‹PossibleWorld(y) & Actual(y)›
1926 AOT_assume ‹w ⊨ p›
1927 AOT_hence p: ‹p›
1928 using w_prop[THEN "∀E"(2), THEN "≡E"(1)] by blast
1929 AOT_show ‹y ⊨ p›
1930 proof(rule "raa-cor:1")
1931 AOT_assume ‹¬y ⊨ p›
1932 AOT_hence ‹y ⊨ ¬p›
1933 by (metis "coherent:1"[unconstrain w, THEN "→E"] "&E"(1) "≡E"(2) w_asm)
1934 AOT_hence ‹¬p›
1935 using w_asm[THEN "&E"(2), THEN actual[THEN "≡⇩d⇩fE"], THEN "&E"(2),
1936 THEN "∀E"(1), rotated, OF "log-prop-prop:2"]
1937 "→E" by blast
1938 AOT_thus ‹p & ¬p› using p "&I" by blast
1939 qed
1940 next
1941 AOT_show ‹w ⊨ p› if ‹y ⊨ p› and ‹PossibleWorld(y) & Actual(y)› for p y
1942 using that(2)[THEN "&E"(2), THEN actual[THEN "≡⇩d⇩fE"], THEN "&E"(2),
1943 THEN "∀E"(2), THEN "→E", OF that(1)]
1944 w_prop[THEN "∀E"(2), THEN "≡E"(2)] by blast
1945 next
1946 AOT_show ‹Situation(y)› if ‹PossibleWorld(y) & Actual(y)› for y
1947 using that[THEN "&E"(1)] "world:1"[THEN "≡⇩d⇩fE", THEN "&E"(1)] by blast
1948 next
1949 AOT_show ‹Situation(w)›
1950 using sit_s by blast
1951 qed(simp)
1952qed
1953
1954AOT_theorem "pre-walpha": ‹❙ιw Actual(w)↓›
1955 using "A-Exists:2" "RA[2]" "act-world:2" "≡E"(2) by blast
1956
1957AOT_define TheActualWorld :: ‹κ⇩s› (‹❙w⇩α›)
1958 "w-alpha": ‹❙w⇩α =⇩d⇩f ❙ιw Actual(w)›
1959
1960
1961AOT_theorem true_in_truth_act_true: ‹⊤ ⊨ p ≡ ❙𝒜p›
1962proof(safe intro!: "≡I" "→I")
1963 AOT_have true_def: ‹❙⊢⇩□ ⊤ = ❙ιx (A!x & ∀F (x[F] ≡ ∃p(p & F = [λy p])))›
1964 by (simp add: "A-descriptions" "rule-id-df:1[zero]" "the-true:1")
1965 AOT_hence true_den: ‹❙⊢⇩□ ⊤↓›
1966 using "t=t-proper:1" "vdash-properties:6" by blast
1967 {
1968 AOT_assume ‹⊤ ⊨ p›
1969 AOT_hence ‹⊤[λy p]›
1970 by (metis "≡⇩d⇩fE" "con-dis-i-e:2:b" "prop-enc" "true-in-s")
1971 AOT_hence ‹❙ιx(A!x & ∀F (x[F] ≡ ∃q (q & F = [λy q])))[λy p]›
1972 using "rule=E" true_def true_den by fast
1973 AOT_hence ‹❙𝒜∃q (q & [λy p] = [λy q])›
1974 using "≡E"(1) "desc-nec-encode:1"[unvarify F] "prop-prop2:2" by fast
1975 AOT_hence ‹∃q ❙𝒜(q & [λy p] = [λy q])›
1976 by (metis "Act-Basic:10" "≡E"(1))
1977 then AOT_obtain q where ‹❙𝒜(q & [λy p] = [λy q])›
1978 using "∃E"[rotated] by blast
1979 AOT_hence actq: ‹❙𝒜q› and ‹❙𝒜[λy p] = [λy q]›
1980 using "Act-Basic:2" "intro-elim:3:a" "&E" by blast+
1981 AOT_hence ‹[λy p] = [λy q]›
1982 using "id-act:1"[unvarify α β, THEN "≡E"(2)] "prop-prop2:2" by blast
1983 AOT_hence ‹p = q›
1984 by (metis "intro-elim:3:b" "p-identity-thm2:3")
1985 AOT_thus ‹❙𝒜p›
1986 using actq "rule=E" id_sym by blast
1987 }
1988 {
1989 AOT_assume ‹❙𝒜p›
1990 AOT_hence ‹❙𝒜(p & [λy p] = [λy p])›
1991 by (auto intro!: "Act-Basic:2"[THEN "≡E"(2)] "&I"
1992 intro: "RA[2]" "=I"(1)[OF "prop-prop2:2"])
1993 AOT_hence ‹∃q ❙𝒜(q & [λy p] = [λy q])›
1994 using "∃I" by fast
1995 AOT_hence ‹❙𝒜∃q (q & [λy p] = [λy q])›
1996 by (metis "Act-Basic:10" "≡E"(2))
1997 AOT_hence ‹❙ιx(A!x & ∀F (x[F] ≡ ∃q (q & F = [λy q])))[λy p]›
1998 using "≡E"(2) "desc-nec-encode:1"[unvarify F] "prop-prop2:2" by fast
1999 AOT_hence ‹⊤[λy p]›
2000 using "rule=E" true_def true_den id_sym by fast
2001 AOT_thus ‹⊤ ⊨ p›
2002 by (safe intro!: "true-in-s"[THEN "≡⇩d⇩fI"] "&I" "possit-sit:6"
2003 "prop-enc"[THEN "≡⇩d⇩fI"] true_den)
2004 }
2005qed
2006
2007AOT_theorem "T-world": ‹⊤ = ❙w⇩α›
2008proof -
2009 AOT_have true_den: ‹❙⊢⇩□ ⊤↓›
2010 using "Situation.res-var:3" "possit-sit:6" "→E" by blast
2011 AOT_have ‹❙𝒜∀p (⊤ ⊨ p → p)›
2012 proof (safe intro!: "logic-actual-nec:3"[axiom_inst, THEN "≡E"(2)] GEN
2013 "logic-actual-nec:2"[axiom_inst, THEN "≡E"(2)] "→I")
2014 fix p
2015 AOT_assume ‹❙𝒜⊤ ⊨ p›
2016 AOT_hence ‹⊤ ⊨ p›
2017 using "lem2:4"[unconstrain s, unvarify β, OF true_den,
2018 THEN "→E", OF "possit-sit:6"] "≡E"(1) by blast
2019 AOT_thus ‹❙𝒜p› using true_in_truth_act_true "≡E"(1) by blast
2020 qed
2021 moreover AOT_have ‹❙𝒜(Situation(κ) & ∀p (κ ⊨ p → p)) → ❙𝒜Actual(κ)› for κ
2022 using actual[THEN "≡Df", THEN "conventions:3"[THEN "≡⇩d⇩fE", THEN "&E"(2)],
2023 THEN "RA[2]", THEN "act-cond"[THEN "→E"]].
2024 ultimately AOT_have act_act_true: ‹❙𝒜Actual(⊤)›
2025 using "possit-sit:4"[unvarify x, OF true_den, THEN "≡E"(2), OF "possit-sit:6"]
2026 "Act-Basic:2"[THEN "≡E"(2), OF "&I"] "→E" by blast
2027 AOT_hence ‹◇Actual(⊤)› by (metis "Act-Sub:3" "vdash-properties:10")
2028 AOT_hence ‹Possible(⊤)›
2029 by (safe intro!: pos[THEN "≡⇩d⇩fI"] "&I" "possit-sit:6")
2030 moreover AOT_have ‹Maximal(⊤)›
2031 proof (safe intro!: max[THEN "≡⇩d⇩fI"] "&I" "possit-sit:6" GEN)
2032 fix p
2033 AOT_have ‹❙𝒜p ∨ ❙𝒜¬p›
2034 by (simp add: "Act-Basic:1")
2035 moreover AOT_have ‹⊤ ⊨ p› if ‹❙𝒜p›
2036 using that true_in_truth_act_true[THEN "≡E"(2)] by blast
2037 moreover AOT_have ‹⊤ ⊨ ¬p› if ‹❙𝒜¬p›
2038 using that true_in_truth_act_true[unvarify p, THEN "≡E"(2)]
2039 "log-prop-prop:2" by blast
2040 ultimately AOT_show ‹⊤ ⊨ p ∨ ⊤ ⊨ ¬p›
2041 using "∨I"(3) "→I" by blast
2042 qed
2043 ultimately AOT_have ‹PossibleWorld(⊤)›
2044 by (safe intro!: "world=maxpos:2"[unvarify x, OF true_den, THEN "≡E"(2)] "&I")
2045 AOT_hence ‹❙𝒜PossibleWorld(⊤)›
2046 using "rigid-pw:4"[unvarify x, OF true_den, THEN "≡E"(2)] by blast
2047 AOT_hence 1: ‹❙𝒜(PossibleWorld(⊤) & Actual(⊤))›
2048 using act_act_true "Act-Basic:2" "df-simplify:2" "intro-elim:3:b" by blast
2049 AOT_have ‹❙w⇩α = ❙ιw(Actual(w))›
2050 using "rule-id-df:1[zero]"[OF "w-alpha", OF "pre-walpha"] by simp
2051 moreover AOT_have w_act_den: ‹❙w⇩α↓›
2052 using calculation "t=t-proper:1" "→E" by blast
2053 ultimately AOT_have ‹∀z (❙𝒜(PossibleWorld(z) & Actual(z)) → z = ❙w⇩α)›
2054 using "nec-hintikka-scheme"[unvarify x] "≡E"(1) "&E" by blast
2055 AOT_thus ‹⊤ = ❙w⇩α›
2056 using "∀E"(1)[rotated, OF true_den] 1 "→E" by blast
2057qed
2058
2059AOT_act_theorem "truth-at-alpha:1": ‹p ≡ ❙w⇩α = ❙ιx (ExtensionOf(x, p))›
2060 by (metis "rule=E" "T-world" "deduction-theorem" "ext-p-tv:3" id_sym "≡I"
2061 "≡E"(1) "≡E"(2) "q-True:1")
2062
2063AOT_act_theorem "truth-at-alpha:2": ‹p ≡ ❙w⇩α ⊨ p›
2064proof -
2065 AOT_have ‹PossibleWorld(❙w⇩α)›
2066 using "&E"(1) "pre-walpha" "rule-id-df:2:b[zero]" "→E"
2067 "w-alpha" "y-in:3" by blast
2068 AOT_hence sit_w_alpha: ‹Situation(❙w⇩α)›
2069 by (metis "≡⇩d⇩fE" "&E"(1) "world:1")
2070 AOT_have w_alpha_den: ‹❙w⇩α↓›
2071 using "pre-walpha" "rule-id-df:2:b[zero]" "w-alpha" by blast
2072 AOT_have ‹p ≡ ⊤❙Σp›
2073 using "q-True:3" by force
2074 moreover AOT_have ‹⊤ = ❙w⇩α›
2075 using "T-world" by auto
2076 ultimately AOT_have ‹p ≡ ❙w⇩α❙Σp›
2077 using "rule=E" by fast
2078 moreover AOT_have ‹❙w⇩α ❙Σ p ≡ ❙w⇩α ⊨ p›
2079 using lem1[unvarify x, OF w_alpha_den, THEN "→E", OF sit_w_alpha]
2080 using "≡S"(1) "≡E"(1) "Commutativity of ≡" "≡Df" sit_w_alpha "true-in-s" by blast
2081 ultimately AOT_show ‹p ≡ ❙w⇩α ⊨ p›
2082 by (metis "≡E"(5))
2083qed
2084
2085AOT_theorem "alpha-world:1": ‹PossibleWorld(❙w⇩α)›
2086proof -
2087 AOT_have 0: ‹❙w⇩α = ❙ιw Actual(w)›
2088 using "pre-walpha" "rule-id-df:1[zero]" "w-alpha" by blast
2089 AOT_hence walpha_den: ‹❙w⇩α↓›
2090 by (metis "t=t-proper:1" "vdash-properties:6")
2091 AOT_have ‹❙𝒜(PossibleWorld(❙w⇩α) & Actual(❙w⇩α))›
2092 by (rule "actual-desc:2"[unvarify x, OF walpha_den, THEN "→E"]) (fact 0)
2093 AOT_hence ‹❙𝒜PossibleWorld(❙w⇩α)›
2094 by (metis "Act-Basic:2" "&E"(1) "≡E"(1))
2095 AOT_thus ‹PossibleWorld(❙w⇩α)›
2096 using "rigid-pw:4"[unvarify x, OF walpha_den, THEN "≡E"(1)]
2097 by blast
2098qed
2099
2100AOT_theorem "alpha-world:2": ‹Maximal(❙w⇩α)›
2101proof -
2102 AOT_have ‹❙w⇩α↓›
2103 using "pre-walpha" "rule-id-df:2:b[zero]" "w-alpha" by blast
2104 then AOT_obtain x where x_def: ‹x = ❙w⇩α›
2105 by (metis "instantiation" "rule=I:1" "existential:1" id_sym)
2106 AOT_hence ‹PossibleWorld(x)› using "alpha-world:1" "rule=E" id_sym by fast
2107 AOT_hence ‹Maximal(x)› by (metis "world-max"[unconstrain w, THEN "→E"])
2108 AOT_thus ‹Maximal(❙w⇩α)› using x_def "rule=E" by blast
2109qed
2110
2111AOT_theorem "t-at-alpha-strict": ‹❙w⇩α ⊨ p ≡ ❙𝒜p›
2112proof -
2113 AOT_have 0: ‹❙w⇩α = ❙ιw Actual(w)›
2114 using "pre-walpha" "rule-id-df:1[zero]" "w-alpha" by blast
2115 AOT_hence walpha_den: ‹❙w⇩α↓›
2116 by (metis "t=t-proper:1" "vdash-properties:6")
2117 AOT_have 1: ‹❙𝒜(PossibleWorld(❙w⇩α) & Actual(❙w⇩α))›
2118 by (rule "actual-desc:2"[unvarify x, OF walpha_den, THEN "→E"]) (fact 0)
2119 AOT_have walpha_sit: ‹Situation(❙w⇩α)›
2120 by (meson "≡⇩d⇩fE" "alpha-world:2" "&E"(1) max)
2121 {
2122 fix p
2123 AOT_have 2: ‹Situation(x) → (❙𝒜x ⊨ p ≡ x ⊨ p)› for x
2124 using "lem2:4"[unconstrain s] by blast
2125 AOT_assume ‹❙w⇩α ⊨ p›
2126 AOT_hence θ: ‹❙𝒜❙w⇩α ⊨ p›
2127 using 2[unvarify x, OF walpha_den, THEN "→E", OF walpha_sit, THEN "≡E"(2)]
2128 by argo
2129 AOT_have 3: ‹❙𝒜Actual(❙w⇩α)›
2130 using "1" "Act-Basic:2" "&E"(2) "≡E"(1) by blast
2131 AOT_have ‹❙𝒜(Situation(❙w⇩α) & ∀q(❙w⇩α ⊨ q → q))›
2132 apply (AOT_subst (reverse) ‹Situation(❙w⇩α) & ∀q(❙w⇩α ⊨ q → q)› ‹Actual(❙w⇩α)›)
2133 using actual "≡Df" apply blast
2134 by (fact 3)
2135 AOT_hence ‹❙𝒜∀q(❙w⇩α ⊨ q → q)› by (metis "Act-Basic:2" "&E"(2) "≡E"(1))
2136 AOT_hence ‹∀q ❙𝒜(❙w⇩α ⊨ q → q)›
2137 using "logic-actual-nec:3"[axiom_inst, THEN "≡E"(1)] by blast
2138 AOT_hence ‹❙𝒜(❙w⇩α ⊨ p → p)› using "∀E"(2) by blast
2139 AOT_hence ‹❙𝒜(❙w⇩α ⊨ p) → ❙𝒜p› by (metis "act-cond" "vdash-properties:10")
2140 AOT_hence ‹❙𝒜p› using θ "→E" by blast
2141 }
2142 AOT_hence 2: ‹❙w⇩α ⊨ p → ❙𝒜p› for p by (rule "→I")
2143 AOT_have walpha_sit: ‹Situation(❙w⇩α)›
2144 using "≡⇩d⇩fE" "alpha-world:2" "&E"(1) max by blast
2145 show ?thesis
2146 proof(safe intro!: "≡I" "→I" 2)
2147 AOT_assume actp: ‹❙𝒜p›
2148 AOT_show ‹❙w⇩α ⊨ p›
2149 proof(rule "raa-cor:1")
2150 AOT_assume ‹¬❙w⇩α ⊨ p›
2151 AOT_hence ‹❙w⇩α ⊨ ¬p›
2152 using "alpha-world:2"[THEN max[THEN "≡⇩d⇩fE"], THEN "&E"(2),
2153 THEN "∀E"(1), OF "log-prop-prop:2"]
2154 by (metis "∨E"(2))
2155 AOT_hence ‹❙𝒜¬p›
2156 using 2[unvarify p, OF "log-prop-prop:2", THEN "→E"] by blast
2157 AOT_hence ‹¬❙𝒜p› by (metis "¬¬I" "Act-Sub:1" "≡E"(4))
2158 AOT_thus ‹❙𝒜p & ¬❙𝒜p› using actp "&I" by blast
2159 qed
2160 qed
2161qed
2162
2163AOT_act_theorem "not-act": ‹w ≠ ❙w⇩α → ¬Actual(w)›
2164proof (rule "→I"; rule "raa-cor:2")
2165 AOT_assume ‹w ≠ ❙w⇩α›
2166 AOT_hence 0: ‹¬(w = ❙w⇩α)› by (metis "≡⇩d⇩fE" "=-infix")
2167 AOT_have walpha_den: ‹❙w⇩α↓›
2168 using "pre-walpha" "rule-id-df:2:b[zero]" "w-alpha" by blast
2169 AOT_have walpha_sit: ‹Situation(❙w⇩α)›
2170 using "≡⇩d⇩fE" "alpha-world:2" "&E"(1) max by blast
2171 AOT_assume act_w: ‹Actual(w)›
2172 AOT_hence w_sit: ‹Situation(w)› by (metis "≡⇩d⇩fE" actual "&E"(1))
2173 AOT_have sid: ‹Situation(x') → (w = x' ≡ ∀p (w ⊨ p ≡ x' ⊨ p))› for x'
2174 using "sit-identity"[unconstrain s', unconstrain s, THEN "→E", OF w_sit]
2175 by blast
2176 AOT_have ‹w = ❙w⇩α›
2177 proof(safe intro!: GEN sid[unvarify x', OF walpha_den, THEN "→E",
2178 OF walpha_sit, THEN "≡E"(2)] "≡I" "→I")
2179 fix p
2180 AOT_assume ‹w ⊨ p›
2181 AOT_hence ‹p›
2182 using actual[THEN "≡⇩d⇩fE", OF act_w, THEN "&E"(2), THEN "∀E"(2), THEN "→E"]
2183 by blast
2184 AOT_hence ‹❙𝒜p›
2185 by (metis "RA[1]")
2186 AOT_thus ‹❙w⇩α ⊨ p›
2187 using "t-at-alpha-strict"[THEN "≡E"(2)] by blast
2188 next
2189 fix p
2190 AOT_assume ‹❙w⇩α ⊨ p›
2191 AOT_hence ‹❙𝒜p›
2192 using "t-at-alpha-strict"[THEN "≡E"(1)] by blast
2193 AOT_hence p: ‹p›
2194 using "logic-actual"[act_axiom_inst, THEN "→E"] by blast
2195 AOT_show ‹w ⊨ p›
2196 proof(rule "raa-cor:1")
2197 AOT_assume ‹¬w ⊨ p›
2198 AOT_hence ‹w ⊨ ¬p›
2199 by (metis "coherent:1" "≡E"(2))
2200 AOT_hence ‹¬p›
2201 using actual[THEN "≡⇩d⇩fE", OF act_w, THEN "&E"(2), THEN "∀E"(1),
2202 OF "log-prop-prop:2", THEN "→E"] by blast
2203 AOT_thus ‹p & ¬p› using p "&I" by blast
2204 qed
2205 qed
2206 AOT_thus ‹w = ❙w⇩α & ¬(w = ❙w⇩α)› using 0 "&I" by blast
2207qed
2208
2209AOT_act_theorem "w-alpha-part": ‹Actual(s) ≡ s ⊴ ❙w⇩α›
2210proof(safe intro!: "≡I" "→I" "sit-part-whole"[THEN "≡⇩d⇩fI"] "&I" GEN
2211 dest!: "sit-part-whole"[THEN "≡⇩d⇩fE"])
2212 AOT_show ‹Situation(s)› if ‹Actual(s)›
2213 using "≡⇩d⇩fE" actual "&E"(1) that by blast
2214next
2215 AOT_show ‹Situation(❙w⇩α)›
2216 using "≡⇩d⇩fE" "alpha-world:2" "&E"(1) max by blast
2217next
2218 fix p
2219 AOT_assume ‹Actual(s)›
2220 moreover AOT_assume ‹s ⊨ p›
2221 ultimately AOT_have ‹p›
2222 using actual[THEN "≡⇩d⇩fE", THEN "&E"(2), THEN "∀E"(2), THEN "→E"] by blast
2223 AOT_thus ‹❙w⇩α ⊨ p›
2224 by (metis "≡E"(1) "truth-at-alpha:2")
2225next
2226 AOT_assume 0: ‹Situation(s) & Situation(❙w⇩α) & ∀p (s ⊨ p → ❙w⇩α ⊨ p)›
2227 AOT_hence ‹s ⊨ p → ❙w⇩α ⊨ p› for p
2228 using "&E" "∀E"(2) by blast
2229 AOT_hence ‹s ⊨ p → p› for p
2230 by (metis "→I" "≡E"(2) "truth-at-alpha:2" "→E")
2231 AOT_hence ‹∀p (s ⊨ p → p)› by (rule GEN)
2232 AOT_thus ‹Actual(s)›
2233 using actual[THEN "≡⇩d⇩fI", OF "&I", OF 0[THEN "&E"(1), THEN "&E"(1)]] by blast
2234qed
2235
2236AOT_act_theorem "act-world2:1": ‹❙w⇩α ⊨ p ≡ [λy p]❙w⇩α›
2237 apply (AOT_subst ‹[λy p]❙w⇩α› p)
2238 apply (rule "beta-C-meta"[THEN "→E", OF "prop-prop2:2", unvarify ν⇩1ν⇩n])
2239 using "pre-walpha" "rule-id-df:2:b[zero]" "w-alpha" apply blast
2240 using "≡E"(2) "Commutativity of ≡" "truth-at-alpha:2" by blast
2241
2242AOT_act_theorem "act-world2:2": ‹p ≡ ❙w⇩α ⊨ [λy p]❙w⇩α›
2243proof -
2244 AOT_have ‹p ≡ [λy p]❙w⇩α›
2245 apply (rule "beta-C-meta"[THEN "→E", OF "prop-prop2:2",
2246 unvarify ν⇩1ν⇩n, symmetric])
2247 using "pre-walpha" "rule-id-df:2:b[zero]" "w-alpha" by blast
2248 also AOT_have ‹… ≡ ❙w⇩α ⊨ [λy p]❙w⇩α›
2249 by (meson "log-prop-prop:2" "rule-ui:1" "truth-at-alpha:2" "universal-cor")
2250 finally show ?thesis.
2251qed
2252
2253AOT_theorem "fund-lem:1": ‹◇p → ◇∃w (w ⊨ p)›
2254proof (rule "RM◇"; rule "→I"; rule "raa-cor:1")
2255 AOT_modally_strict {
2256 AOT_obtain w where w_prop: ‹∀q (w ⊨ q ≡ q)›
2257 using "act-world:1" "PossibleWorld.∃E"[rotated] by meson
2258 AOT_assume p: ‹p›
2259 AOT_assume 0: ‹¬∃w (w ⊨ p)›
2260 AOT_have ‹∀w ¬(w ⊨ p)›
2261 apply (AOT_subst ‹PossibleWorld(x) → ¬x ⊨ p›
2262 ‹¬(PossibleWorld(x) & x ⊨ p)› for: x)
2263 apply (metis "&I" "&E"(1) "&E"(2) "→I" "≡I" "modus-tollens:2")
2264 using "0" "cqt-further:4" "vdash-properties:10" by blast
2265 AOT_hence ‹¬(w ⊨ p)›
2266 using PossibleWorld.ψ "rule-ui:3" "→E" by blast
2267 AOT_hence ‹¬p›
2268 using w_prop[THEN "∀E"(2), THEN "≡E"(2)]
2269 by (metis "raa-cor:3")
2270 AOT_thus ‹p & ¬p›
2271 using p "&I" by blast
2272 }
2273qed
2274
2275AOT_theorem "fund-lem:2": ‹◇∃w (w ⊨ p) → ∃w (w ⊨ p)›
2276proof (rule "→I")
2277 AOT_assume ‹◇∃w (w ⊨ p)›
2278 AOT_hence ‹∃w ◇(w ⊨ p)›
2279 using "PossibleWorld.res-var-bound-reas[BF◇]"[THEN "→E"] by auto
2280 then AOT_obtain w where ‹◇(w ⊨ p)›
2281 using "PossibleWorld.∃E"[rotated] by meson
2282 moreover AOT_have ‹Situation(w)›
2283 by (metis "≡⇩d⇩fE" "&E"(1) pos "world-pos")
2284 ultimately AOT_have ‹w ⊨ p›
2285 using "lem2:2"[unconstrain s, THEN "→E"] "≡E" by blast
2286 AOT_thus ‹∃w w ⊨ p›
2287 by (rule "PossibleWorld.∃I")
2288qed
2289
2290AOT_theorem "fund-lem:3": ‹p → ∀s(∀q (s ⊨ q ≡ q) → s ⊨ p)›
2291proof(safe intro!: "→I" Situation.GEN)
2292 fix s
2293 AOT_assume ‹p›
2294 moreover AOT_assume ‹∀q (s ⊨ q ≡ q)›
2295 ultimately AOT_show ‹s ⊨ p›
2296 using "∀E"(2) "≡E"(2) by blast
2297qed
2298
2299AOT_theorem "fund-lem:4": ‹□p → □∀s(∀q (s ⊨ q ≡ q) → s ⊨ p)›
2300 using "fund-lem:3" by (rule RM)
2301
2302AOT_theorem "fund-lem:5": ‹□∀s φ{s} → ∀s □φ{s}›
2303proof(safe intro!: "→I" Situation.GEN)
2304 fix s
2305 AOT_assume ‹□∀s φ{s}›
2306 AOT_hence ‹∀s □φ{s}›
2307 using "Situation.res-var-bound-reas[CBF]"[THEN "→E"] by blast
2308 AOT_thus ‹□φ{s}›
2309 using "Situation.∀E" by fast
2310qed
2311
2312text‹Note: not explicit in PLM.›
2313AOT_theorem "fund-lem:5[world]": ‹□∀w φ{w} → ∀w □φ{w}›
2314proof(safe intro!: "→I" PossibleWorld.GEN)
2315 fix w
2316 AOT_assume ‹□∀w φ{w}›
2317 AOT_hence ‹∀w □φ{w}›
2318 using "PossibleWorld.res-var-bound-reas[CBF]"[THEN "→E"] by blast
2319 AOT_thus ‹□φ{w}›
2320 using "PossibleWorld.∀E" by fast
2321qed
2322
2323AOT_theorem "fund-lem:6": ‹∀w w ⊨ p → □∀w w ⊨ p›
2324proof(rule "→I")
2325 AOT_assume ‹∀w (w ⊨ p)›
2326 AOT_hence 1: ‹PossibleWorld(w) → (w ⊨ p)› for w
2327 using "∀E"(2) by blast
2328 AOT_show ‹□∀w w ⊨ p›
2329 proof(rule "raa-cor:1")
2330 AOT_assume ‹¬□∀w w ⊨ p›
2331 AOT_hence ‹◇¬∀w w ⊨ p›
2332 by (metis "KBasic:11" "≡E"(1))
2333 AOT_hence ‹◇∃x (¬(PossibleWorld(x) → x ⊨ p))›
2334 apply (rule "RM◇"[THEN "→E", rotated])
2335 by (simp add: "cqt-further:2")
2336 AOT_hence ‹∃x ◇(¬(PossibleWorld(x) → x ⊨ p))›
2337 by (metis "BF◇" "vdash-properties:10")
2338 then AOT_obtain x where x_prop: ‹◇¬(PossibleWorld(x) → x ⊨ p)›
2339 using "∃E"[rotated] by blast
2340 AOT_have ‹◇(PossibleWorld(x) & ¬x ⊨ p)›
2341 apply (AOT_subst ‹PossibleWorld(x) & ¬x ⊨ p›
2342 ‹¬(PossibleWorld(x) → x ⊨ p)›)
2343 apply (meson "≡E"(6) "oth-class-taut:1:b" "oth-class-taut:3:a")
2344 by(fact x_prop)
2345 AOT_hence 2: ‹◇PossibleWorld(x) & ◇¬x ⊨ p›
2346 by (metis "KBasic2:3" "vdash-properties:10")
2347 AOT_hence ‹PossibleWorld(x)›
2348 using "&E"(1) "≡E"(1) "rigid-pw:2" by blast
2349 AOT_hence ‹□(x ⊨ p)›
2350 using 2[THEN "&E"(2)] 1[unconstrain w, THEN "→E"] "→E"
2351 "rigid-truth-at:1"[unconstrain w, THEN "→E"]
2352 by (metis "≡E"(1))
2353 moreover AOT_have ‹¬□(x ⊨ p)›
2354 using 2[THEN "&E"(2)] by (metis "¬¬I" "KBasic:12" "≡E"(4))
2355 ultimately AOT_show ‹p & ¬p› for p
2356 by (metis "raa-cor:3")
2357 qed
2358qed
2359
2360AOT_theorem "fund-lem:7": ‹□∀w(w ⊨ p) → □p›
2361proof(rule RM; rule "→I")
2362 AOT_modally_strict {
2363 AOT_obtain w where w_prop: ‹∀p (w ⊨ p ≡ p)›
2364 using "act-world:1" "PossibleWorld.∃E"[rotated] by meson
2365 AOT_assume ‹∀w (w ⊨ p)›
2366 AOT_hence ‹w ⊨ p›
2367 using "PossibleWorld.∀E" by fast
2368 AOT_thus ‹p›
2369 using w_prop[THEN "∀E"(2), THEN "≡E"(1)] by blast
2370 }
2371qed
2372
2373AOT_theorem "fund:1": ‹◇p ≡ ∃w w ⊨ p›
2374proof (rule "≡I"; rule "→I")
2375 AOT_assume ‹◇p›
2376 AOT_thus ‹∃w w ⊨ p›
2377 by (metis "fund-lem:1" "fund-lem:2" "→E")
2378next
2379 AOT_assume ‹∃w w ⊨ p›
2380 then AOT_obtain w where w_prop: ‹w ⊨ p›
2381 using "PossibleWorld.∃E"[rotated] by meson
2382 AOT_hence ‹◇∀p (w ⊨ p ≡ p)›
2383 using "world:1"[THEN "≡⇩d⇩fE", THEN "&E"(2)] PossibleWorld.ψ "&E" by blast
2384 AOT_hence ‹∀p ◇(w ⊨ p ≡ p)›
2385 by (metis "Buridan◇" "→E")
2386 AOT_hence 1: ‹◇(w ⊨ p ≡ p)›
2387 by (metis "log-prop-prop:2" "rule-ui:1")
2388 AOT_have ‹◇((w ⊨ p → p) & (p → w ⊨ p))›
2389 apply (AOT_subst ‹(w ⊨ p → p) & (p → w ⊨ p)› ‹w ⊨ p ≡ p›)
2390 apply (meson "conventions:3" "≡E"(6) "oth-class-taut:3:a" "≡Df")
2391 by (fact 1)
2392 AOT_hence ‹◇(w ⊨ p → p)›
2393 by (metis "RM◇" "Conjunction Simplification"(1) "→E")
2394 moreover AOT_have ‹□(w ⊨ p)›
2395 using w_prop by (metis "≡E"(1) "rigid-truth-at:1")
2396 ultimately AOT_show ‹◇p›
2397 by (metis "KBasic2:4" "≡E"(1) "→E")
2398qed
2399
2400AOT_theorem "fund:2": ‹□p ≡ ∀w (w ⊨ p)›
2401proof -
2402 AOT_have 0: ‹∀w (w ⊨ ¬p ≡ ¬w ⊨ p)›
2403 apply (rule PossibleWorld.GEN)
2404 using "coherent:1" by blast
2405 AOT_have ‹◇¬p ≡ ∃w (w ⊨ ¬p)›
2406 using "fund:1"[unvarify p, OF "log-prop-prop:2"] by blast
2407 also AOT_have ‹… ≡ ∃w ¬(w ⊨ p)›
2408 proof(safe intro!: "≡I" "→I")
2409 AOT_assume ‹∃w w ⊨ ¬p›
2410 then AOT_obtain w where w_prop: ‹w ⊨ ¬p›
2411 using "PossibleWorld.∃E"[rotated] by meson
2412 AOT_hence ‹¬w ⊨ p›
2413 using 0[THEN "PossibleWorld.∀E", THEN "≡E"(1)] "&E" by blast
2414 AOT_thus ‹∃w ¬w ⊨ p›
2415 by (rule "PossibleWorld.∃I")
2416 next
2417 AOT_assume ‹∃w ¬w ⊨ p›
2418 then AOT_obtain w where w_prop: ‹¬w ⊨ p›
2419 using "PossibleWorld.∃E"[rotated] by meson
2420 AOT_hence ‹w ⊨ ¬p›
2421 using 0[THEN "∀E"(2), THEN "→E", THEN "≡E"(1)] "&E"
2422 by (metis "coherent:1" "≡E"(2))
2423 AOT_thus ‹∃w w ⊨ ¬p›
2424 by (rule "PossibleWorld.∃I")
2425 qed
2426 finally AOT_have ‹¬◇¬p ≡ ¬∃w ¬w ⊨ p›
2427 by (meson "≡E"(1) "oth-class-taut:4:b")
2428 AOT_hence ‹□p ≡ ¬∃w ¬w ⊨ p›
2429 by (metis "KBasic:12" "≡E"(5))
2430 also AOT_have ‹… ≡ ∀w w ⊨ p›
2431 proof(safe intro!: "≡I" "→I")
2432 AOT_assume ‹¬∃w ¬w ⊨ p›
2433 AOT_hence 0: ‹∀x (¬(PossibleWorld(x) & ¬x ⊨ p))›
2434 by (metis "cqt-further:4" "→E")
2435 AOT_show ‹∀w w ⊨ p›
2436 apply (AOT_subst ‹PossibleWorld(x) → x ⊨ p›
2437 ‹¬(PossibleWorld(x) & ¬x ⊨ p)› for: x)
2438 using "oth-class-taut:1:a" apply presburger
2439 by (fact 0)
2440 next
2441 AOT_assume 0: ‹∀w w ⊨ p›
2442 AOT_have ‹∀x (¬(PossibleWorld(x) & ¬x ⊨ p))›
2443 by (AOT_subst (reverse) ‹¬(PossibleWorld(x) & ¬x ⊨ p)›
2444 ‹PossibleWorld(x) → x ⊨ p› for: x)
2445 (auto simp: "oth-class-taut:1:a" 0)
2446 AOT_thus ‹¬∃w ¬w ⊨ p›
2447 by (metis "∃E" "raa-cor:3" "rule-ui:3")
2448 qed
2449 finally AOT_show ‹□p ≡ ∀w w ⊨ p›.
2450qed
2451
2452AOT_theorem "fund:3": ‹¬◇p ≡ ¬∃w w ⊨ p›
2453 by (metis (full_types) "contraposition:1[1]" "→I" "fund:1" "≡I" "≡E"(1,2))
2454
2455AOT_theorem "fund:4": ‹¬□p ≡ ∃w ¬w ⊨p›
2456 apply (AOT_subst ‹∃w ¬w ⊨ p› ‹¬ ∀w w ⊨ p›)
2457 apply (AOT_subst ‹PossibleWorld(x) → x ⊨ p›
2458 ‹¬(PossibleWorld(x) & ¬x ⊨ p)› for: x)
2459 by (auto simp add: "oth-class-taut:1:a" "conventions:4" "≡Df" RN
2460 "fund:2" "rule-sub-lem:1:a")
2461
2462AOT_theorem "nec-dia-w:1": ‹□p ≡ ∃w w ⊨ □p›
2463proof -
2464 AOT_have ‹□p ≡ ◇□p›
2465 using "S5Basic:2" by blast
2466 also AOT_have ‹... ≡ ∃w w ⊨ □p›
2467 using "fund:1"[unvarify p, OF "log-prop-prop:2"] by blast
2468 finally show ?thesis.
2469qed
2470
2471AOT_theorem "nec-dia-w:2": ‹□p ≡ ∀w w ⊨ □p›
2472proof -
2473 AOT_have ‹□p ≡ □□p›
2474 using 4 "qml:2"[axiom_inst] "≡I" by blast
2475 also AOT_have ‹... ≡ ∀w w ⊨ □p›
2476 using "fund:2"[unvarify p, OF "log-prop-prop:2"] by blast
2477 finally show ?thesis.
2478qed
2479
2480AOT_theorem "nec-dia-w:3": ‹◇p ≡ ∃w w ⊨ ◇p›
2481proof -
2482 AOT_have ‹◇p ≡ ◇◇p›
2483 by (simp add: "4◇" "T◇" "≡I")
2484 also AOT_have ‹... ≡ ∃w w ⊨ ◇p›
2485 using "fund:1"[unvarify p, OF "log-prop-prop:2"] by blast
2486 finally show ?thesis.
2487qed
2488
2489AOT_theorem "nec-dia-w:4": ‹◇p ≡ ∀w w ⊨ ◇p›
2490proof -
2491 AOT_have ‹◇p ≡ □◇p›
2492 by (simp add: "S5Basic:1")
2493 also AOT_have ‹... ≡ ∀w w ⊨ ◇p›
2494 using "fund:2"[unvarify p, OF "log-prop-prop:2"] by blast
2495 finally show ?thesis.
2496qed
2497
2498AOT_theorem "conj-dist-w:1": ‹w ⊨ (p & q) ≡ ((w ⊨ p) & (w ⊨ q))›
2499proof(safe intro!: "≡I" "→I")
2500 AOT_assume ‹w ⊨ (p & q)›
2501 AOT_hence 0: ‹□w ⊨ (p & q)›
2502 using "rigid-truth-at:1"[unvarify p, THEN "≡E"(1), OF "log-prop-prop:2"]
2503 by blast
2504 AOT_modally_strict {
2505 AOT_have ‹∀p (w ⊨ p ≡ p) → ((w ⊨ (φ & ψ)) → (w ⊨ φ & w ⊨ ψ))› for w φ ψ
2506 proof(safe intro!: "→I")
2507 AOT_assume ‹∀ p (w ⊨ p ≡ p)›
2508 AOT_hence ‹w ⊨ (φ & ψ) ≡ (φ & ψ)› and ‹w ⊨ φ ≡ φ› and ‹w ⊨ ψ ≡ ψ›
2509 using "∀E"(1)[rotated, OF "log-prop-prop:2"] by blast+
2510 moreover AOT_assume ‹w ⊨ (φ & ψ)›
2511 ultimately AOT_show ‹w ⊨ φ & w ⊨ ψ›
2512 by (metis "&I" "&E"(1) "&E"(2) "≡E"(1) "≡E"(2))
2513 qed
2514 }
2515 AOT_hence ‹◇∀p (w ⊨ p ≡ p) → ◇(w ⊨ (φ & ψ) → w ⊨ φ & w ⊨ ψ)› for w φ ψ
2516 by (rule "RM◇")
2517 moreover AOT_have pos: ‹◇∀p (w ⊨ p ≡ p)›
2518 using "world:1"[THEN "≡⇩d⇩fE", OF PossibleWorld.ψ] "&E" by blast
2519 ultimately AOT_have ‹◇(w ⊨ (p & q) → w ⊨ p & w ⊨ q)› using "→E" by blast
2520 AOT_hence ‹◇(w ⊨ p) & ◇(w ⊨ q)›
2521 by (metis 0 "KBasic2:3" "KBasic2:4" "≡E"(1) "vdash-properties:10")
2522 AOT_thus ‹w ⊨ p & w ⊨ q›
2523 using "rigid-truth-at:2"[unvarify p, THEN "≡E"(1), OF "log-prop-prop:2"]
2524 "&E" "&I" by meson
2525next
2526 AOT_assume ‹w ⊨ p & w ⊨ q›
2527 AOT_hence ‹□w ⊨ p & □w ⊨ q›
2528 using "rigid-truth-at:1"[unvarify p, THEN "≡E"(1), OF "log-prop-prop:2"]
2529 "&E" "&I" by blast
2530 AOT_hence 0: ‹□(w ⊨ p & w ⊨ q)›
2531 by (metis "KBasic:3" "≡E"(2))
2532 AOT_modally_strict {
2533 AOT_have ‹∀p (w ⊨ p ≡ p) → ((w ⊨ φ & w ⊨ ψ) → (w ⊨ (φ & ψ)))› for w φ ψ
2534 proof(safe intro!: "→I")
2535 AOT_assume ‹∀ p (w ⊨ p ≡ p)›
2536 AOT_hence ‹w ⊨ (φ & ψ) ≡ (φ & ψ)› and ‹w ⊨ φ ≡ φ› and ‹w ⊨ ψ ≡ ψ›
2537 using "∀E"(1)[rotated, OF "log-prop-prop:2"] by blast+
2538 moreover AOT_assume ‹w ⊨ φ & w ⊨ ψ›
2539 ultimately AOT_show ‹w ⊨ (φ & ψ)›
2540 by (metis "&I" "&E"(1) "&E"(2) "≡E"(1) "≡E"(2))
2541 qed
2542 }
2543 AOT_hence ‹◇∀p (w ⊨ p ≡ p) → ◇((w ⊨ φ & w ⊨ ψ) → w ⊨ (φ & ψ))› for w φ ψ
2544 by (rule "RM◇")
2545 moreover AOT_have pos: ‹◇∀p (w ⊨ p ≡ p)›
2546 using "world:1"[THEN "≡⇩d⇩fE", OF PossibleWorld.ψ] "&E" by blast
2547 ultimately AOT_have ‹◇((w ⊨ p & w ⊨ q) → w ⊨ (p & q))›
2548 using "→E" by blast
2549 AOT_hence ‹◇(w ⊨ (p & q))›
2550 by (metis 0 "KBasic2:4" "≡E"(1) "vdash-properties:10")
2551 AOT_thus ‹w ⊨ (p & q)›
2552 using "rigid-truth-at:2"[unvarify p, THEN "≡E"(1), OF "log-prop-prop:2"]
2553 by blast
2554qed
2555
2556AOT_theorem "conj-dist-w:2": ‹w ⊨ (p → q) ≡ ((w ⊨ p) → (w ⊨ q))›
2557proof(safe intro!: "≡I" "→I")
2558 AOT_assume ‹w ⊨ (p → q)›
2559 AOT_hence 0: ‹□w ⊨ (p → q)›
2560 using "rigid-truth-at:1"[unvarify p, THEN "≡E"(1), OF "log-prop-prop:2"]
2561 by blast
2562 AOT_assume ‹w ⊨ p›
2563 AOT_hence 1: ‹□w ⊨ p›
2564 by (metis "T◇" "≡E"(1) "rigid-truth-at:3" "→E")
2565 AOT_modally_strict {
2566 AOT_have ‹∀p (w ⊨ p ≡ p) → ((w ⊨ (φ → ψ)) → (w ⊨ φ → w ⊨ ψ))› for w φ ψ
2567 proof(safe intro!: "→I")
2568 AOT_assume ‹∀ p (w ⊨ p ≡ p)›
2569 AOT_hence ‹w ⊨ (φ → ψ) ≡ (φ → ψ)› and ‹w ⊨ φ ≡ φ› and ‹w ⊨ ψ ≡ ψ›
2570 using "∀E"(1)[rotated, OF "log-prop-prop:2"] by blast+
2571 moreover AOT_assume ‹w ⊨ (φ → ψ)›
2572 moreover AOT_assume ‹w ⊨ φ›
2573 ultimately AOT_show ‹w ⊨ ψ›
2574 by (metis "≡E"(1) "≡E"(2) "→E")
2575 qed
2576 }
2577 AOT_hence ‹◇∀p (w ⊨ p ≡ p) → ◇(w ⊨ (φ → ψ) → (w ⊨ φ → w ⊨ ψ))› for w φ ψ
2578 by (rule "RM◇")
2579 moreover AOT_have pos: ‹◇∀p (w ⊨ p ≡ p)›
2580 using "world:1"[THEN "≡⇩d⇩fE", OF PossibleWorld.ψ] "&E" by blast
2581 ultimately AOT_have ‹◇(w ⊨ (p → q) → (w ⊨ p → w ⊨ q))›
2582 using "→E" by blast
2583 AOT_hence ‹◇(w ⊨ p → w ⊨ q)›
2584 by (metis 0 "KBasic2:4" "≡E"(1) "→E")
2585 AOT_hence ‹◇w ⊨ q›
2586 by (metis 1 "KBasic2:4" "≡E"(1) "→E")
2587 AOT_thus ‹w ⊨ q›
2588 using "rigid-truth-at:2"[unvarify p, THEN "≡E"(1), OF "log-prop-prop:2"]
2589 "&E" "&I" by meson
2590next
2591 AOT_assume ‹w ⊨ p → w ⊨ q›
2592 AOT_hence ‹¬(w ⊨ p) ∨ w ⊨ q›
2593 by (metis "∨I"(1) "∨I"(2) "reductio-aa:1" "→E")
2594 AOT_hence ‹w ⊨ ¬p ∨ w ⊨ q›
2595 by (metis "coherent:1" "∨I"(1) "∨I"(2) "∨E"(2) "≡E"(2) "reductio-aa:1")
2596 AOT_hence 0: ‹□(w ⊨ ¬p ∨ w ⊨ q)›
2597 using "rigid-truth-at:1"[unvarify p, THEN "≡E"(1), OF "log-prop-prop:2"]
2598 by (metis "KBasic:15" "∨I"(1) "∨I"(2) "∨E"(2) "reductio-aa:1" "→E")
2599 AOT_modally_strict {
2600 AOT_have ‹∀p (w ⊨ p ≡ p) → ((w ⊨ ¬φ ∨ w ⊨ ψ) → (w ⊨ (φ → ψ)))› for w φ ψ
2601 proof(safe intro!: "→I")
2602 AOT_assume ‹∀ p (w ⊨ p ≡ p)›
2603 moreover AOT_assume ‹w ⊨ ¬φ ∨ w ⊨ ψ›
2604 ultimately AOT_show ‹w ⊨ (φ → ψ)›
2605 by (metis "∨E"(2) "→I" "≡E"(1) "≡E"(2) "log-prop-prop:2"
2606 "reductio-aa:1" "rule-ui:1")
2607 qed
2608 }
2609 AOT_hence ‹◇∀p (w ⊨ p ≡ p) → ◇((w ⊨ ¬φ ∨ w ⊨ ψ) → w ⊨ (φ → ψ))› for w φ ψ
2610 by (rule "RM◇")
2611 moreover AOT_have pos: ‹◇∀p (w ⊨ p ≡ p)›
2612 using "world:1"[THEN "≡⇩d⇩fE", OF PossibleWorld.ψ] "&E" by blast
2613 ultimately AOT_have ‹◇((w ⊨ ¬p ∨ w ⊨ q) → w ⊨ (p → q))›
2614 using "→E" by blast
2615 AOT_hence ‹◇(w ⊨ (p → q))›
2616 by (metis 0 "KBasic2:4" "≡E"(1) "→E")
2617 AOT_thus ‹w ⊨ (p → q)›
2618 using "rigid-truth-at:2"[unvarify p, THEN "≡E"(1), OF "log-prop-prop:2"]
2619 by blast
2620qed
2621
2622AOT_theorem "conj-dist-w:3": ‹w ⊨ (p ∨ q) ≡ ((w ⊨ p) ∨ (w ⊨ q))›
2623proof(safe intro!: "≡I" "→I")
2624 AOT_assume ‹w ⊨ (p ∨ q)›
2625 AOT_hence 0: ‹□w ⊨ (p ∨ q)›
2626 using "rigid-truth-at:1"[unvarify p, THEN "≡E"(1), OF "log-prop-prop:2"]
2627 by blast
2628 AOT_modally_strict {
2629 AOT_have ‹∀p (w ⊨ p ≡ p) → ((w ⊨ (φ ∨ ψ)) → (w ⊨ φ ∨ w ⊨ ψ))› for w φ ψ
2630 proof(safe intro!: "→I")
2631 AOT_assume ‹∀ p (w ⊨ p ≡ p)›
2632 AOT_hence ‹w ⊨ (φ ∨ ψ) ≡ (φ ∨ ψ)› and ‹w ⊨ φ ≡ φ› and ‹w ⊨ ψ ≡ ψ›
2633 using "∀E"(1)[rotated, OF "log-prop-prop:2"] by blast+
2634 moreover AOT_assume ‹w ⊨ (φ ∨ ψ)›
2635 ultimately AOT_show ‹w ⊨ φ ∨ w ⊨ ψ›
2636 by (metis "∨I"(1) "∨I"(2) "∨E"(3) "≡E"(1) "≡E"(2) "reductio-aa:1")
2637 qed
2638 }
2639 AOT_hence ‹◇∀p (w ⊨ p ≡ p) → ◇(w ⊨ (φ ∨ ψ) → (w ⊨ φ ∨ w ⊨ ψ))› for w φ ψ
2640 by (rule "RM◇")
2641 moreover AOT_have pos: ‹◇∀p (w ⊨ p ≡ p)›
2642 using "world:1"[THEN "≡⇩d⇩fE", OF PossibleWorld.ψ] "&E" by blast
2643 ultimately AOT_have ‹◇(w ⊨ (p ∨ q) → (w ⊨ p ∨ w ⊨ q))› using "→E" by blast
2644 AOT_hence ‹◇(w ⊨ p ∨ w ⊨ q)›
2645 by (metis 0 "KBasic2:4" "≡E"(1) "vdash-properties:10")
2646 AOT_hence ‹◇w ⊨ p ∨ ◇w ⊨ q›
2647 using "KBasic2:2"[THEN "≡E"(1)] by blast
2648 AOT_thus ‹w ⊨ p ∨ w ⊨ q›
2649 using "rigid-truth-at:2"[unvarify p, THEN "≡E"(1), OF "log-prop-prop:2"]
2650 by (metis "∨I"(1) "∨I"(2) "∨E"(2) "reductio-aa:1")
2651next
2652 AOT_assume ‹w ⊨ p ∨ w ⊨ q›
2653 AOT_hence 0: ‹□(w ⊨ p ∨ w ⊨ q)›
2654 using "rigid-truth-at:1"[unvarify p, THEN "≡E"(1), OF "log-prop-prop:2"]
2655 by (metis "KBasic:15" "∨I"(1) "∨I"(2) "∨E"(2) "reductio-aa:1" "→E")
2656 AOT_modally_strict {
2657 AOT_have ‹∀p (w ⊨ p ≡ p) → ((w ⊨ φ ∨ w ⊨ ψ) → (w ⊨ (φ ∨ ψ)))› for w φ ψ
2658 proof(safe intro!: "→I")
2659 AOT_assume ‹∀ p (w ⊨ p ≡ p)›
2660 moreover AOT_assume ‹w ⊨ φ ∨ w ⊨ ψ›
2661 ultimately AOT_show ‹w ⊨ (φ ∨ ψ)›
2662 by (metis "∨I"(1) "∨I"(2) "∨E"(2) "≡E"(1) "≡E"(2)
2663 "log-prop-prop:2" "reductio-aa:1" "rule-ui:1")
2664 qed
2665 }
2666 AOT_hence ‹◇∀p (w ⊨ p ≡ p) → ◇((w ⊨ φ ∨ w ⊨ ψ) → w ⊨ (φ ∨ ψ))› for w φ ψ
2667 by (rule "RM◇")
2668 moreover AOT_have pos: ‹◇∀p (w ⊨ p ≡ p)›
2669 using "world:1"[THEN "≡⇩d⇩fE", OF PossibleWorld.ψ] "&E" by blast
2670 ultimately AOT_have ‹◇((w ⊨ p ∨ w ⊨ q) → w ⊨ (p ∨ q))›
2671 using "→E" by blast
2672 AOT_hence ‹◇(w ⊨ (p ∨ q))›
2673 by (metis 0 "KBasic2:4" "≡E"(1) "→E")
2674 AOT_thus ‹w ⊨ (p ∨ q)›
2675 using "rigid-truth-at:2"[unvarify p, THEN "≡E"(1), OF "log-prop-prop:2"]
2676 by blast
2677qed
2678
2679AOT_theorem "conj-dist-w:4": ‹w ⊨ (p ≡ q) ≡ ((w ⊨ p) ≡ (w ⊨ q))›
2680proof(rule "≡I"; rule "→I")
2681 AOT_assume ‹w ⊨ (p ≡ q)›
2682 AOT_hence 0: ‹□w ⊨ (p ≡ q)›
2683 using "rigid-truth-at:1"[unvarify p, THEN "≡E"(1), OF "log-prop-prop:2"]
2684 by blast
2685 AOT_modally_strict {
2686 AOT_have ‹∀p (w ⊨ p ≡ p) → ((w ⊨ (φ ≡ ψ)) → (w ⊨ φ ≡ w ⊨ ψ))› for w φ ψ
2687 proof(safe intro!: "→I")
2688 AOT_assume ‹∀ p (w ⊨ p ≡ p)›
2689 AOT_hence ‹w ⊨ (φ ≡ ψ) ≡ (φ ≡ ψ)› and ‹w ⊨ φ ≡ φ› and ‹w ⊨ ψ ≡ ψ›
2690 using "∀E"(1)[rotated, OF "log-prop-prop:2"] by blast+
2691 moreover AOT_assume ‹w ⊨ (φ ≡ ψ)›
2692 ultimately AOT_show ‹w ⊨ φ ≡ w ⊨ ψ›
2693 by (metis "≡E"(2) "≡E"(5) "Commutativity of ≡")
2694 qed
2695 }
2696 AOT_hence ‹◇∀p (w ⊨ p ≡ p) → ◇(w ⊨ (φ ≡ ψ) → (w ⊨ φ ≡ w ⊨ ψ))› for w φ ψ
2697 by (rule "RM◇")
2698 moreover AOT_have pos: ‹◇∀p (w ⊨ p ≡ p)›
2699 using "world:1"[THEN "≡⇩d⇩fE", OF PossibleWorld.ψ] "&E" by blast
2700 ultimately AOT_have ‹◇(w ⊨ (p ≡ q) → (w ⊨ p ≡ w ⊨ q))›
2701 using "→E" by blast
2702 AOT_hence 1: ‹◇(w ⊨ p ≡ w ⊨ q)›
2703 by (metis 0 "KBasic2:4" "≡E"(1) "vdash-properties:10")
2704 AOT_have ‹◇((w ⊨ p → w ⊨ q) & (w ⊨ q → w ⊨ p))›
2705 apply (AOT_subst ‹(w ⊨ p → w ⊨ q) & (w ⊨ q → w ⊨ p)› ‹w ⊨ p ≡ w ⊨ q›)
2706 apply (meson "≡⇩d⇩fE" "conventions:3" "→I" "df-rules-formulas[4]" "≡I")
2707 by (fact 1)
2708 AOT_hence 2: ‹◇(w ⊨ p → w ⊨ q) & ◇(w ⊨ q → w ⊨ p)›
2709 by (metis "KBasic2:3" "vdash-properties:10")
2710 AOT_have ‹◇(¬w ⊨ p ∨ w ⊨ q)› and ‹◇(¬w ⊨ q ∨ w ⊨ p)›
2711 apply (AOT_subst (reverse) ‹¬w ⊨ p ∨ w ⊨ q› ‹w ⊨ p → w ⊨ q›)
2712 apply (simp add: "oth-class-taut:1:c")
2713 apply (fact 2[THEN "&E"(1)])
2714 apply (AOT_subst (reverse) ‹¬w ⊨ q ∨ w ⊨ p› ‹w ⊨ q → w ⊨ p›)
2715 apply (simp add: "oth-class-taut:1:c")
2716 by (fact 2[THEN "&E"(2)])
2717 AOT_hence ‹◇(¬w ⊨ p) ∨ ◇w ⊨ q› and ‹◇¬w ⊨ q ∨ ◇w ⊨ p›
2718 using "KBasic2:2" "≡E"(1) by blast+
2719 AOT_hence ‹¬□w ⊨ p ∨ ◇w ⊨ q› and ‹¬□w ⊨ q ∨ ◇w ⊨ p›
2720 by (metis "KBasic:11" "∨I"(1) "∨I"(2) "∨E"(2) "≡E"(2) "raa-cor:1")+
2721 AOT_thus ‹w ⊨ p ≡ w ⊨ q›
2722 using "rigid-truth-at:2"[unvarify p, THEN "≡E"(1), OF "log-prop-prop:2"]
2723 by (metis "¬¬I" "T◇" "∨E"(2) "→I" "≡I" "≡E"(1) "rigid-truth-at:3")
2724next
2725 AOT_have ‹□PossibleWorld(w)›
2726 using "≡E"(1) "rigid-pw:1" PossibleWorld.ψ by blast
2727 moreover {
2728 fix p
2729 AOT_modally_strict {
2730 AOT_have ‹PossibleWorld(w) → (w ⊨ p → □w ⊨ p)›
2731 using "rigid-truth-at:1" "→I"
2732 by (metis "≡E"(1))
2733 }
2734 AOT_hence ‹□PossibleWorld(w) → □(w ⊨ p → □w ⊨ p)›
2735 by (rule RM)
2736 }
2737 ultimately AOT_have 1: ‹□(w ⊨ p → □w ⊨ p)› for p
2738 by (metis "→E")
2739 AOT_assume ‹w ⊨ p ≡ w ⊨ q›
2740 AOT_hence 0: ‹□(w ⊨ p ≡ w ⊨ q)›
2741 using "sc-eq-box-box:5"[THEN "→E", THEN "qml:2"[axiom_inst, THEN "→E"],
2742 THEN "→E", OF "&I"]
2743 by (metis "1")
2744 AOT_modally_strict {
2745 AOT_have ‹∀p (w ⊨ p ≡ p) → ((w ⊨ φ ≡ w ⊨ ψ) → (w ⊨ (φ ≡ ψ)))› for w φ ψ
2746 proof(safe intro!: "→I")
2747 AOT_assume ‹∀ p (w ⊨ p ≡ p)›
2748 moreover AOT_assume ‹w ⊨ φ ≡ w ⊨ ψ›
2749 ultimately AOT_show ‹w ⊨ (φ ≡ ψ)›
2750 by (metis "≡E"(2) "≡E"(6) "log-prop-prop:2" "rule-ui:1")
2751 qed
2752 }
2753 AOT_hence ‹◇∀p (w ⊨ p ≡ p) → ◇((w ⊨ φ ≡ w ⊨ ψ) → w ⊨ (φ ≡ ψ))› for w φ ψ
2754 by (rule "RM◇")
2755 moreover AOT_have pos: ‹◇∀p (w ⊨ p ≡ p)›
2756 using "world:1"[THEN "≡⇩d⇩fE", OF PossibleWorld.ψ] "&E" by blast
2757 ultimately AOT_have ‹◇((w ⊨ p ≡ w ⊨ q) → w ⊨ (p ≡ q))›
2758 using "→E" by blast
2759 AOT_hence ‹◇(w ⊨ (p ≡ q))›
2760 by (metis 0 "KBasic2:4" "≡E"(1) "→E")
2761 AOT_thus ‹w ⊨ (p ≡ q)›
2762 using "rigid-truth-at:2"[unvarify p, THEN "≡E"(1), OF "log-prop-prop:2"]
2763 by blast
2764qed
2765
2766AOT_theorem "conj-dist-w:5": ‹w ⊨ (∀α φ{α}) ≡ (∀ α (w ⊨ φ{α}))›
2767proof(safe intro!: "≡I" "→I" GEN)
2768 AOT_assume ‹w ⊨ (∀α φ{α})›
2769 AOT_hence 0: ‹□w ⊨ (∀α φ{α})›
2770 using "rigid-truth-at:1"[unvarify p, THEN "≡E"(1), OF "log-prop-prop:2"]
2771 by blast
2772 AOT_modally_strict {
2773 AOT_have ‹∀p (w ⊨ p ≡ p) → ((w ⊨ (∀α φ{α})) → (∀α w ⊨ φ{α}))› for w
2774 proof(safe intro!: "→I" GEN)
2775 AOT_assume ‹∀p (w ⊨ p ≡ p)›
2776 moreover AOT_assume ‹w ⊨ (∀α φ{α})›
2777 ultimately AOT_show ‹w ⊨ φ{α}› for α
2778 by (metis "≡E"(1) "≡E"(2) "log-prop-prop:2" "rule-ui:1" "rule-ui:3")
2779 qed
2780 }
2781 AOT_hence ‹◇∀p (w ⊨ p ≡ p) → ◇(w ⊨ (∀α φ{α}) → (∀α w ⊨ φ{α}))› for w
2782 by (rule "RM◇")
2783 moreover AOT_have pos: ‹◇∀p (w ⊨ p ≡ p)›
2784 using "world:1"[THEN "≡⇩d⇩fE", OF PossibleWorld.ψ] "&E" by blast
2785 ultimately AOT_have ‹◇(w ⊨ (∀α φ{α}) → (∀α w ⊨ φ{α}))› using "→E" by blast
2786 AOT_hence ‹◇(∀α w ⊨ φ{α})›
2787 by (metis 0 "KBasic2:4" "≡E"(1) "→E")
2788 AOT_hence ‹∀α ◇w ⊨ φ{α}›
2789 by (metis "Buridan◇" "→E")
2790 AOT_thus ‹w ⊨ φ{α}› for α
2791 using "rigid-truth-at:2"[unvarify p, THEN "≡E"(1), OF "log-prop-prop:2"]
2792 "∀E"(2) by blast
2793next
2794 AOT_assume ‹∀α w ⊨ φ{α}›
2795 AOT_hence ‹w ⊨ φ{α}› for α using "∀E"(2) by blast
2796 AOT_hence ‹□w ⊨ φ{α}› for α
2797 using "rigid-truth-at:1"[unvarify p, THEN "≡E"(1), OF "log-prop-prop:2"]
2798 "&E" "&I" by blast
2799 AOT_hence ‹∀α □w ⊨ φ{α}› by (rule GEN)
2800 AOT_hence 0: ‹□∀α w ⊨ φ{α}› by (rule BF[THEN "→E"])
2801 AOT_modally_strict {
2802 AOT_have ‹∀p (w ⊨ p ≡ p) → ((∀α w ⊨ φ{α}) → (w ⊨ (∀α φ{α})))› for w
2803 proof(safe intro!: "→I")
2804 AOT_assume ‹∀ p (w ⊨ p ≡ p)›
2805 moreover AOT_assume ‹∀α w ⊨ φ{α}›
2806 ultimately AOT_show ‹w ⊨ (∀α φ{α})›
2807 by (metis "≡E"(1) "≡E"(2) "log-prop-prop:2" "rule-ui:1"
2808 "rule-ui:3" "universal-cor")
2809 qed
2810 }
2811 AOT_hence ‹◇∀p (w ⊨ p ≡ p) → ◇((∀α w ⊨ φ{α}) → w ⊨ (∀α φ{α}))› for w
2812 by (rule "RM◇")
2813 moreover AOT_have pos: ‹◇∀p (w ⊨ p ≡ p)›
2814 using "world:1"[THEN "≡⇩d⇩fE", OF PossibleWorld.ψ] "&E" by blast
2815 ultimately AOT_have ‹◇((∀α w ⊨ φ{α}) → w ⊨ (∀α φ{α}))›
2816 using "→E" by blast
2817 AOT_hence ‹◇(w ⊨ (∀α φ{α}))›
2818 by (metis 0 "KBasic2:4" "≡E"(1) "→E")
2819 AOT_thus ‹w ⊨ (∀α φ{α})›
2820 using "rigid-truth-at:2"[unvarify p, THEN "≡E"(1), OF "log-prop-prop:2"]
2821 by blast
2822qed
2823
2824AOT_theorem "conj-dist-w:6": ‹w ⊨ (∃α φ{α}) ≡ (∃ α (w ⊨ φ{α}))›
2825proof(safe intro!: "≡I" "→I" GEN)
2826 AOT_assume ‹w ⊨ (∃α φ{α})›
2827 AOT_hence 0: ‹□w ⊨ (∃α φ{α})›
2828 using "rigid-truth-at:1"[unvarify p, THEN "≡E"(1), OF "log-prop-prop:2"]
2829 by blast
2830 AOT_modally_strict {
2831 AOT_have ‹∀p (w ⊨ p ≡ p) → ((w ⊨ (∃α φ{α})) → (∃α w ⊨ φ{α}))› for w
2832 proof(safe intro!: "→I" GEN)
2833 AOT_assume ‹∀p (w ⊨ p ≡ p)›
2834 moreover AOT_assume ‹w ⊨ (∃α φ{α})›
2835 ultimately AOT_show ‹∃ α (w ⊨ φ{α})›
2836 by (metis "∃E" "∃I"(2) "≡E"(1,2) "log-prop-prop:2" "rule-ui:1")
2837 qed
2838 }
2839 AOT_hence ‹◇∀p (w ⊨ p ≡ p) → ◇(w ⊨ (∃α φ{α}) → (∃α w ⊨ φ{α}))› for w
2840 by (rule "RM◇")
2841 moreover AOT_have pos: ‹◇∀p (w ⊨ p ≡ p)›
2842 using "world:1"[THEN "≡⇩d⇩fE", OF PossibleWorld.ψ] "&E" by blast
2843 ultimately AOT_have ‹◇(w ⊨ (∃α φ{α}) → (∃α w ⊨ φ{α}))› using "→E" by blast
2844 AOT_hence ‹◇(∃α w ⊨ φ{α})›
2845 by (metis 0 "KBasic2:4" "≡E"(1) "→E")
2846 AOT_hence ‹∃α ◇w ⊨ φ{α}›
2847 by (metis "BF◇" "→E")
2848 then AOT_obtain α where ‹◇w ⊨ φ{α}›
2849 using "∃E"[rotated] by blast
2850 AOT_hence ‹w ⊨ φ{α}›
2851 using "rigid-truth-at:2"[unvarify p, THEN "≡E"(1), OF "log-prop-prop:2"] by blast
2852 AOT_thus ‹∃ α w ⊨ φ{α}› by (rule "∃I")
2853next
2854 AOT_assume ‹∃α w ⊨ φ{α}›
2855 then AOT_obtain α where ‹w ⊨ φ{α}› using "∃E"[rotated] by blast
2856 AOT_hence ‹□w ⊨ φ{α}›
2857 using "rigid-truth-at:1"[unvarify p, THEN "≡E"(1), OF "log-prop-prop:2"]
2858 "&E" "&I" by blast
2859 AOT_hence ‹∃α □w ⊨ φ{α}›
2860 by (rule "∃I")
2861 AOT_hence 0: ‹□∃α w ⊨ φ{α}›
2862 by (metis Buridan "→E")
2863 AOT_modally_strict {
2864 AOT_have ‹∀p (w ⊨ p ≡ p) → ((∃α w ⊨ φ{α}) → (w ⊨ (∃α φ{α})))› for w
2865 proof(safe intro!: "→I")
2866 AOT_assume ‹∀ p (w ⊨ p ≡ p)›
2867 moreover AOT_assume ‹∃α w ⊨ φ{α}›
2868 then AOT_obtain α where ‹w ⊨ φ{α}›
2869 using "∃E"[rotated] by blast
2870 ultimately AOT_show ‹w ⊨ (∃α φ{α})›
2871 by (metis "∃I"(2) "≡E"(1,2) "log-prop-prop:2" "rule-ui:1")
2872 qed
2873 }
2874 AOT_hence ‹◇∀p (w ⊨ p ≡ p) → ◇((∃α w ⊨ φ{α}) → w ⊨ (∃α φ{α}))› for w
2875 by (rule "RM◇")
2876 moreover AOT_have pos: ‹◇∀p (w ⊨ p ≡ p)›
2877 using "world:1"[THEN "≡⇩d⇩fE", OF PossibleWorld.ψ] "&E" by blast
2878 ultimately AOT_have ‹◇((∃α w ⊨ φ{α}) → w ⊨ (∃α φ{α}))›
2879 using "→E" by blast
2880 AOT_hence ‹◇(w ⊨ (∃α φ{α}))›
2881 by (metis 0 "KBasic2:4" "≡E"(1) "→E")
2882 AOT_thus ‹w ⊨ (∃α φ{α})›
2883 using "rigid-truth-at:2"[unvarify p, THEN "≡E"(1), OF "log-prop-prop:2"]
2884 by blast
2885qed
2886
2887AOT_theorem "conj-dist-w:7": ‹(w ⊨ □p) → □w ⊨ p›
2888proof(rule "→I")
2889 AOT_assume ‹w ⊨ □p›
2890 AOT_hence ‹∃w w ⊨ □p› by (rule "PossibleWorld.∃I")
2891 AOT_hence ‹◇□p› using "fund:1"[unvarify p, OF "log-prop-prop:2", THEN "≡E"(2)]
2892 by blast
2893 AOT_hence ‹□p›
2894 by (metis "5◇" "→E")
2895 AOT_hence 1: ‹□□p›
2896 by (metis "S5Basic:6" "≡E"(1))
2897 AOT_have ‹□∀w w ⊨ p›
2898 by (AOT_subst (reverse) ‹∀w w ⊨ p› ‹□p›)
2899 (auto simp add: "fund:2" 1)
2900 AOT_hence ‹∀w □w ⊨ p›
2901 using "fund-lem:5[world]"[THEN "→E"] by simp
2902 AOT_thus ‹□w ⊨ p›
2903 using "→E" "PossibleWorld.∀E" by fast
2904qed
2905
2906AOT_theorem "conj-dist-w:8": ‹∃w∃p((□w ⊨ p) & ¬w ⊨ □p)›
2907proof -
2908 AOT_obtain r where A: r and ‹◇¬r›
2909 by (metis "&E"(1) "&E"(2) "≡⇩d⇩fE" "∃E" "cont-tf:1" "cont-tf-thm:1")
2910 AOT_hence B: ‹¬□r›
2911 by (metis "KBasic:11" "≡E"(2))
2912 AOT_have ‹◇r›
2913 using A "T◇"[THEN "→E"] by simp
2914 AOT_hence ‹∃w w ⊨ r›
2915 using "fund:1"[THEN "≡E"(1)] by blast
2916 then AOT_obtain w where w: ‹w ⊨ r›
2917 using "PossibleWorld.∃E"[rotated] by meson
2918 AOT_hence ‹□w ⊨ r›
2919 by (metis "T◇" "≡E"(1) "rigid-truth-at:3" "vdash-properties:10")
2920 moreover AOT_have ‹¬w ⊨ □r›
2921 proof(rule "raa-cor:2")
2922 AOT_assume ‹w ⊨ □r›
2923 AOT_hence ‹∃w w ⊨ □r›
2924 by (rule "PossibleWorld.∃I")
2925 AOT_hence ‹□r›
2926 by (metis "≡E"(2) "nec-dia-w:1")
2927 AOT_thus ‹□r & ¬□r›
2928 using B "&I" by blast
2929 qed
2930 ultimately AOT_have ‹□w ⊨ r & ¬w ⊨ □r›
2931 by (rule "&I")
2932 AOT_hence ‹∃p (□w ⊨ p & ¬w ⊨ □p)›
2933 by (rule "∃I")
2934 thus ?thesis
2935 by (rule "PossibleWorld.∃I")
2936qed
2937
2938AOT_theorem "conj-dist-w:9": ‹(◇w ⊨ p) → w ⊨ ◇p›
2939proof(rule "→I"; rule "raa-cor:1")
2940 AOT_assume ‹◇w ⊨ p›
2941 AOT_hence 0: ‹w ⊨ p›
2942 by (metis "≡E"(1) "rigid-truth-at:2")
2943 AOT_assume ‹¬w ⊨ ◇p›
2944 AOT_hence 1: ‹w ⊨ ¬◇p›
2945 using "coherent:1"[unvarify p, THEN "≡E"(2), OF "log-prop-prop:2"] by blast
2946 moreover AOT_have ‹w ⊨ (¬◇p → ¬p)›
2947 using "T◇"[THEN "contraposition:1[1]", THEN RN]
2948 "fund:2"[unvarify p, OF "log-prop-prop:2", THEN "≡E"(1), THEN "∀E"(2),
2949 THEN "→E", rotated, OF PossibleWorld.ψ]
2950 by blast
2951 ultimately AOT_have ‹w ⊨ ¬p›
2952 using "conj-dist-w:2"[unvarify p q, OF "log-prop-prop:2", OF "log-prop-prop:2",
2953 THEN "≡E"(1), THEN "→E"]
2954 by blast
2955 AOT_hence ‹w ⊨ p & w ⊨ ¬p› using 0 "&I" by blast
2956 AOT_thus ‹p & ¬p›
2957 by (metis "coherent:1" "Conjunction Simplification"(1,2) "≡E"(4)
2958 "modus-tollens:1" "raa-cor:3")
2959qed
2960
2961AOT_theorem "conj-dist-w:10": ‹∃w∃p((w ⊨ ◇p) & ¬◇w ⊨ p)›
2962proof -
2963 AOT_obtain w where w: ‹∀p (w ⊨ p ≡ p)›
2964 using "act-world:1" "PossibleWorld.∃E"[rotated] by meson
2965 AOT_obtain r where ‹¬r› and ‹◇r›
2966 using "cont-tf-thm:2" "cont-tf:2"[THEN "≡⇩d⇩fE"] "&E" "∃E"[rotated] by metis
2967 AOT_hence ‹w ⊨ ¬r› and 0: ‹w ⊨ ◇r›
2968 using w[THEN "∀E"(1), OF "log-prop-prop:2", THEN "≡E"(2)] by blast+
2969 AOT_hence ‹¬w ⊨ r› using "coherent:1"[THEN "≡E"(1)] by blast
2970 AOT_hence ‹¬◇w ⊨ r› by (metis "≡E"(4) "rigid-truth-at:2")
2971 AOT_hence ‹w ⊨ ◇r & ¬◇w ⊨ r› using 0 "&I" by blast
2972 AOT_hence ‹∃p (w ⊨ ◇p & ¬◇w ⊨ p)› by (rule "∃I")
2973 thus ?thesis by (rule "PossibleWorld.∃I")
2974qed
2975
2976AOT_theorem "two-worlds-exist:1": ‹∃p(ContingentlyTrue(p)) → ∃w (¬Actual(w))›
2977proof(rule "→I")
2978 AOT_assume ‹∃p ContingentlyTrue(p)›
2979 then AOT_obtain p where ‹ContingentlyTrue(p)›
2980 using "∃E"[rotated] by blast
2981 AOT_hence p: ‹p & ◇¬p›
2982 by (metis "≡⇩d⇩fE" "cont-tf:1")
2983 AOT_hence ‹∃w w ⊨ ¬p›
2984 using "fund:1"[unvarify p, OF "log-prop-prop:2", THEN "≡E"(1)] "&E" by blast
2985 then AOT_obtain w where w: ‹w ⊨ ¬p›
2986 using "PossibleWorld.∃E"[rotated] by meson
2987 AOT_have ‹¬Actual(w)›
2988 proof(rule "raa-cor:2")
2989 AOT_assume ‹Actual(w)›
2990 AOT_hence ‹w ⊨ p›
2991 using p[THEN "&E"(1)] actual[THEN "≡⇩d⇩fE", THEN "&E"(2)]
2992 by (metis "log-prop-prop:2" "raa-cor:3" "rule-ui:1" "→E" w)
2993 moreover AOT_have ‹¬(w ⊨ p)›
2994 by (metis "coherent:1" "≡E"(4) "reductio-aa:2" w)
2995 ultimately AOT_show ‹w ⊨ p & ¬(w ⊨ p)›
2996 using "&I" by blast
2997 qed
2998 AOT_thus ‹∃w ¬Actual(w)›
2999 by (rule "PossibleWorld.∃I")
3000qed
3001
3002
3003AOT_theorem "two-worlds-exist:2": ‹∃p(ContingentlyFalse(p)) → ∃w (¬Actual(w))›
3004proof(rule "→I")
3005 AOT_assume ‹∃p ContingentlyFalse(p)›
3006 then AOT_obtain p where ‹ContingentlyFalse(p)›
3007 using "∃E"[rotated] by blast
3008 AOT_hence p: ‹¬p & ◇p›
3009 by (metis "≡⇩d⇩fE" "cont-tf:2")
3010 AOT_hence ‹∃w w ⊨ p›
3011 using "fund:1"[unvarify p, OF "log-prop-prop:2", THEN "≡E"(1)] "&E" by blast
3012 then AOT_obtain w where w: ‹w ⊨ p›
3013 using "PossibleWorld.∃E"[rotated] by meson
3014 moreover AOT_have ‹¬Actual(w)›
3015 proof(rule "raa-cor:2")
3016 AOT_assume ‹Actual(w)›
3017 AOT_hence ‹w ⊨ ¬p›
3018 using p[THEN "&E"(1)] actual[THEN "≡⇩d⇩fE", THEN "&E"(2)]
3019 by (metis "log-prop-prop:2" "raa-cor:3" "rule-ui:1" "→E" w)
3020 moreover AOT_have ‹¬(w ⊨ p)›
3021 using calculation by (metis "coherent:1" "≡E"(4) "reductio-aa:2")
3022 AOT_thus ‹w ⊨ p & ¬(w ⊨ p)›
3023 using "&I" w by metis
3024 qed
3025 AOT_thus ‹∃w ¬Actual(w)›
3026 by (rule "PossibleWorld.∃I")
3027qed
3028
3029AOT_theorem "two-worlds-exist:3": ‹∃w ¬Actual(w)›
3030 using "cont-tf-thm:1" "two-worlds-exist:1" "→E" by blast
3031
3032AOT_theorem "two-worlds-exist:4": ‹∃w∃w'(w ≠ w')›
3033proof -
3034 AOT_obtain w where w: ‹Actual(w)›
3035 using "act-world:2"[THEN "uniqueness:1"[THEN "≡⇩d⇩fE"],
3036 THEN "cqt-further:5"[THEN "→E"]]
3037 "PossibleWorld.∃E"[rotated] "&E"
3038 by blast
3039 moreover AOT_obtain w' where w': ‹¬Actual(w')›
3040 using "two-worlds-exist:3" "PossibleWorld.∃E"[rotated] by meson
3041 AOT_have ‹¬(w = w')›
3042 proof(rule "raa-cor:2")
3043 AOT_assume ‹w = w'›
3044 AOT_thus ‹p & ¬p› for p
3045 using w w' "&E" by (metis "rule=E" "raa-cor:3")
3046 qed
3047 AOT_hence ‹w ≠ w'›
3048 by (metis "≡⇩d⇩fI" "=-infix")
3049 AOT_hence ‹∃w' w ≠ w'›
3050 by (rule "PossibleWorld.∃I")
3051 thus ?thesis
3052 by (rule "PossibleWorld.∃I")
3053qed
3054
3055
3056
3057AOT_theorem "w-rel:1": ‹[λx φ{x}]↓ → [λx w ⊨ φ{x}]↓›
3058proof(rule "→I")
3059 AOT_assume ‹[λx φ{x}]↓›
3060 AOT_hence ‹□[λx φ{x}]↓›
3061 by (metis "exist-nec" "→E")
3062 moreover AOT_have
3063 ‹□[λx φ{x}]↓ → □∀x∀y(∀F([F]x ≡ [F]y) → ((w ⊨ φ{x}) ≡ ( w ⊨ φ{y})))›
3064 proof (rule RM; rule "→I"; rule GEN; rule GEN; rule "→I")
3065 AOT_modally_strict {
3066 fix x y
3067 AOT_assume ‹[λx φ{x}]↓›
3068 AOT_hence ‹∀x∀y (∀F ([F]x ≡ [F]y) → □(φ{x} ≡ φ{y}))›
3069 using "&E" "kirchner-thm-cor:1"[THEN "→E"] by blast
3070 AOT_hence ‹∀F ([F]x ≡ [F]y) → □(φ{x} ≡ φ{y})›
3071 using "∀E"(2) by blast
3072 moreover AOT_assume ‹∀F ([F]x ≡ [F]y)›
3073 ultimately AOT_have ‹□(φ{x} ≡ φ{y})›
3074 using "→E" by blast
3075 AOT_hence ‹∀w (w ⊨ (φ{x} ≡ φ{y}))›
3076 using "fund:2"[unvarify p, OF "log-prop-prop:2", THEN "≡E"(1)] by blast
3077 AOT_hence ‹w ⊨ (φ{x} ≡ φ{y})›
3078 using "∀E"(2) using PossibleWorld.ψ "→E" by blast
3079 AOT_thus ‹(w ⊨ φ{x}) ≡ (w ⊨ φ{y})›
3080 using "conj-dist-w:4"[unvarify p q, OF "log-prop-prop:2",
3081 OF "log-prop-prop:2", THEN "≡E"(1)] by blast
3082 }
3083 qed
3084 ultimately AOT_have ‹□∀x∀y(∀F([F]x ≡ [F]y) → ((w ⊨ φ{x}) ≡ ( w ⊨ φ{y})))›
3085 using "→E" by blast
3086 AOT_thus ‹[λx w ⊨ φ{x}]↓›
3087 using "kirchner-thm:1"[THEN "≡E"(2)] by fast
3088qed
3089
3090AOT_theorem "w-rel:2": ‹[λx⇩1...x⇩n φ{x⇩1...x⇩n}]↓ → [λx⇩1...x⇩n w ⊨ φ{x⇩1...x⇩n}]↓›
3091proof(rule "→I")
3092 AOT_assume ‹[λx⇩1...x⇩n φ{x⇩1...x⇩n}]↓›
3093 AOT_hence ‹□[λx⇩1...x⇩n φ{x⇩1...x⇩n}]↓›
3094 by (metis "exist-nec" "→E")
3095 moreover AOT_have ‹□[λx⇩1...x⇩n φ{x⇩1...x⇩n}]↓ → □∀x⇩1...∀x⇩n∀y⇩1...∀y⇩n(
3096 ∀F([F]x⇩1...x⇩n ≡ [F]y⇩1...y⇩n) → ((w ⊨ φ{x⇩1...x⇩n}) ≡ ( w ⊨ φ{y⇩1...y⇩n})))›
3097 proof (rule RM; rule "→I"; rule GEN; rule GEN; rule "→I")
3098 AOT_modally_strict {
3099 fix x⇩1x⇩n y⇩1y⇩n
3100 AOT_assume ‹[λx⇩1...x⇩n φ{x⇩1...x⇩n}]↓›
3101 AOT_hence ‹∀x⇩1...∀x⇩n∀y⇩1...∀y⇩n (
3102 ∀F ([F]x⇩1...x⇩n ≡ [F]y⇩1...y⇩n) → □(φ{x⇩1...x⇩n} ≡ φ{y⇩1...y⇩n}))›
3103 using "&E" "kirchner-thm-cor:2"[THEN "→E"] by blast
3104 AOT_hence ‹∀F ([F]x⇩1...x⇩n ≡ [F]y⇩1...y⇩n) → □(φ{x⇩1...x⇩n} ≡ φ{y⇩1...y⇩n})›
3105 using "∀E"(2) by blast
3106 moreover AOT_assume ‹∀F ([F]x⇩1...x⇩n ≡ [F]y⇩1...y⇩n)›
3107 ultimately AOT_have ‹□(φ{x⇩1...x⇩n} ≡ φ{y⇩1...y⇩n})›
3108 using "→E" by blast
3109 AOT_hence ‹∀w (w ⊨ (φ{x⇩1...x⇩n} ≡ φ{y⇩1...y⇩n}))›
3110 using "fund:2"[unvarify p, OF "log-prop-prop:2", THEN "≡E"(1)] by blast
3111 AOT_hence ‹w ⊨ (φ{x⇩1...x⇩n} ≡ φ{y⇩1...y⇩n})›
3112 using "∀E"(2) using PossibleWorld.ψ "→E" by blast
3113 AOT_thus ‹(w ⊨ φ{x⇩1...x⇩n}) ≡ (w ⊨ φ{y⇩1...y⇩n})›
3114 using "conj-dist-w:4"[unvarify p q, OF "log-prop-prop:2",
3115 OF "log-prop-prop:2", THEN "≡E"(1)] by blast
3116 }
3117 qed
3118 ultimately AOT_have ‹□∀x⇩1...∀x⇩n∀y⇩1...∀y⇩n(
3119 ∀F([F]x⇩1...x⇩n ≡ [F]y⇩1...y⇩n) → ((w ⊨ φ{x⇩1...x⇩n}) ≡ ( w ⊨ φ{y⇩1...y⇩n})))›
3120 using "→E" by blast
3121 AOT_thus ‹[λx⇩1...x⇩n w ⊨ φ{x⇩1...x⇩n}]↓›
3122 using "kirchner-thm:2"[THEN "≡E"(2)] by fast
3123qed
3124
3125AOT_theorem "w-rel:3": ‹[λx⇩1...x⇩n w ⊨ [F]x⇩1...x⇩n]↓›
3126 by (rule "w-rel:2"[THEN "→E"]) "cqt:2[lambda]"
3127
3128AOT_define WorldIndexedRelation :: ‹Π ⇒ τ ⇒ Π› (‹_⇩_›)
3129 "w-index": ‹[F]⇩w =⇩d⇩f [λx⇩1...x⇩n w ⊨ [F]x⇩1...x⇩n]›
3130
3131AOT_define Rigid :: ‹τ ⇒ φ› (‹Rigid'(_')›)
3132 "df-rigid-rel:1":
3133‹Rigid(F) ≡⇩d⇩f F↓ & □∀x⇩1...∀x⇩n([F]x⇩1...x⇩n → □[F]x⇩1...x⇩n)›
3134
3135AOT_define Rigidifies :: ‹τ ⇒ τ ⇒ φ› (‹Rigidifies'(_,_')›)
3136 "df-rigid-rel:2":
3137‹Rigidifies(F, G) ≡⇩d⇩f Rigid(F) & ∀x⇩1...∀x⇩n([F]x⇩1...x⇩n ≡ [G]x⇩1...x⇩n)›
3138
3139AOT_theorem "rigid-der:1": ‹[[F]⇩w]x⇩1...x⇩n ≡ w ⊨ [F]x⇩1...x⇩n›
3140 apply (rule "rule-id-df:2:b[2]"[where τ="λ (Π, κ). «[Π]⇩κ»" and
3141 σ="λ(Π, κ). «[λx⇩1...x⇩n κ ⊨ [Π]x⇩1...x⇩n]»",
3142 simplified, OF "w-index"])
3143 apply (fact "w-rel:3")
3144 apply (rule "beta-C-meta"[THEN "→E"])
3145 by (fact "w-rel:3")
3146
3147AOT_theorem "rigid-der:2": ‹Rigid([G]⇩w)›
3148proof(safe intro!: "≡⇩d⇩fI"[OF "df-rigid-rel:1"] "&I")
3149 AOT_show ‹[G]⇩w↓›
3150 by (rule "rule-id-df:2:b[2]"[where τ="λ (Π, κ). «[Π]⇩κ»" and
3151 σ="λ(Π, κ). «[λx⇩1...x⇩n κ ⊨ [Π]x⇩1...x⇩n]»",
3152 simplified, OF "w-index"])
3153 (fact "w-rel:3")+
3154next
3155 AOT_have ‹□∀x⇩1...∀x⇩n ([[G]⇩w]x⇩1...x⇩n → □[[G]⇩w]x⇩1...x⇩n)›
3156 proof(rule RN; safe intro!: "→I" GEN)
3157 AOT_modally_strict {
3158 AOT_have assms: ‹PossibleWorld(w)› using PossibleWorld.ψ.
3159 AOT_hence nec_pw_w: ‹□PossibleWorld(w)›
3160 using "≡E"(1) "rigid-pw:1" by blast
3161 fix x⇩1x⇩n
3162 AOT_assume ‹[[G]⇩w]x⇩1...x⇩n›
3163 AOT_hence ‹[λx⇩1...x⇩n w ⊨ [G]x⇩1...x⇩n]x⇩1...x⇩n›
3164 using "rule-id-df:2:a[2]"[where τ="λ (Π, κ). «[Π]⇩κ»" and
3165 σ="λ(Π, κ). «[λx⇩1...x⇩n κ ⊨ [Π]x⇩1...x⇩n]»",
3166 simplified, OF "w-index", OF "w-rel:3"]
3167 by fast
3168 AOT_hence ‹w ⊨ [G]x⇩1...x⇩n›
3169 by (metis "β→C"(1))
3170 AOT_hence ‹□w ⊨ [G]x⇩1...x⇩n›
3171 using "rigid-truth-at:1"[unvarify p, OF "log-prop-prop:2", THEN "≡E"(1)]
3172 by blast
3173 moreover AOT_have ‹□w ⊨ [G]x⇩1...x⇩n → □[λx⇩1...x⇩n w ⊨ [G]x⇩1...x⇩n]x⇩1...x⇩n›
3174 proof (rule RM; rule "→I")
3175 AOT_modally_strict {
3176 AOT_assume ‹w ⊨ [G]x⇩1...x⇩n›
3177 AOT_thus ‹[λx⇩1...x⇩n w ⊨ [G]x⇩1...x⇩n]x⇩1...x⇩n›
3178 by (auto intro!: "β←C"(1) simp: "w-rel:3" "cqt:2")
3179 }
3180 qed
3181 ultimately AOT_have 1: ‹□[λx⇩1...x⇩n w ⊨ [G]x⇩1...x⇩n]x⇩1...x⇩n›
3182 using "→E" by blast
3183 AOT_show ‹□[[G]⇩w]x⇩1...x⇩n›
3184 by (rule "rule-id-df:2:b[2]"[where τ="λ (Π, κ). «[Π]⇩κ»" and
3185 σ="λ(Π, κ). «[λx⇩1...x⇩n κ ⊨ [Π]x⇩1...x⇩n]»",
3186 simplified, OF "w-index"])
3187 (auto simp: 1 "w-rel:3")
3188 }
3189 qed
3190 AOT_thus ‹□∀x⇩1...∀x⇩n ([[G]⇩w]x⇩1...x⇩n → □[[G]⇩w]x⇩1...x⇩n)›
3191 using "→E" by blast
3192qed
3193
3194AOT_theorem "rigid-der:3": ‹∃F Rigidifies(F, G)›
3195proof -
3196 AOT_obtain w where w: ‹∀p (w ⊨ p ≡ p)›
3197 using "act-world:1" "PossibleWorld.∃E"[rotated] by meson
3198 show ?thesis
3199 proof (rule "∃I"(1)[where τ=‹«[G]⇩w»›])
3200 AOT_show ‹Rigidifies([G]⇩w, [G])›
3201 proof(safe intro!: "≡⇩d⇩fI"[OF "df-rigid-rel:2"] "&I" GEN)
3202 AOT_show ‹Rigid([G]⇩w)›
3203 using "rigid-der:2" by blast
3204 next
3205 fix x⇩1x⇩n
3206 AOT_have ‹[[G]⇩w]x⇩1...x⇩n ≡ [λx⇩1...x⇩n w ⊨ [G]x⇩1...x⇩n]x⇩1...x⇩n›
3207 proof(rule "≡I"; rule "→I")
3208 AOT_assume ‹[[G]⇩w]x⇩1...x⇩n›
3209 AOT_thus ‹[λx⇩1...x⇩n w ⊨ [G]x⇩1...x⇩n]x⇩1...x⇩n›
3210 by (rule "rule-id-df:2:a[2]"
3211 [where τ="λ (Π, κ). «[Π]⇩κ»" and
3212 σ="λ(Π, κ). «[λx⇩1...x⇩n κ ⊨ [Π]x⇩1...x⇩n]»",
3213 simplified, OF "w-index", OF "w-rel:3"])
3214 next
3215 AOT_assume ‹[λx⇩1...x⇩n w ⊨ [G]x⇩1...x⇩n]x⇩1...x⇩n›
3216 AOT_thus ‹[[G]⇩w]x⇩1...x⇩n›
3217 by (rule "rule-id-df:2:b[2]"
3218 [where τ="λ (Π, κ). «[Π]⇩κ»" and
3219 σ="λ(Π, κ). «[λx⇩1...x⇩n κ ⊨ [Π]x⇩1...x⇩n]»",
3220 simplified, OF "w-index", OF "w-rel:3"])
3221 qed
3222 also AOT_have ‹… ≡ w ⊨ [G]x⇩1...x⇩n›
3223 by (rule "beta-C-meta"[THEN "→E"])
3224 (fact "w-rel:3")
3225 also AOT_have ‹… ≡ [G]x⇩1...x⇩n›
3226 using w[THEN "∀E"(1), OF "log-prop-prop:2"] by blast
3227 finally AOT_show ‹[[G]⇩w]x⇩1...x⇩n ≡ [G]x⇩1...x⇩n›.
3228 qed
3229 next
3230 AOT_show ‹[G]⇩w↓›
3231 by (rule "rule-id-df:2:b[2]"[where τ="λ (Π, κ). «[Π]⇩κ»"
3232 and σ="λ(Π, κ). «[λx⇩1...x⇩n κ ⊨ [Π]x⇩1...x⇩n]»",
3233 simplified, OF "w-index"])
3234 (auto simp: "w-rel:3")
3235 qed
3236qed
3237
3238AOT_theorem "rigid-rel-thms:1":
3239 ‹□(∀x⇩1...∀x⇩n ([F]x⇩1...x⇩n → □[F]x⇩1...x⇩n)) ≡ ∀x⇩1...∀x⇩n(◇[F]x⇩1...x⇩n → □[F]x⇩1...x⇩n)›
3240proof(safe intro!: "≡I" "→I" GEN)
3241 fix x⇩1x⇩n
3242 AOT_assume ‹□∀x⇩1...∀x⇩n ([F]x⇩1...x⇩n → □[F]x⇩1...x⇩n)›
3243 AOT_hence ‹∀x⇩1...∀x⇩n □([F]x⇩1...x⇩n → □[F]x⇩1...x⇩n)›
3244 by (metis "→E" GEN RM "cqt-orig:3")
3245 AOT_hence ‹□([F]x⇩1...x⇩n → □[F]x⇩1...x⇩n)›
3246 using "∀E"(2) by blast
3247 AOT_hence ‹◇[F]x⇩1...x⇩n → □[F]x⇩1...x⇩n›
3248 by (metis "≡E"(1) "sc-eq-box-box:1")
3249 moreover AOT_assume ‹◇[F]x⇩1...x⇩n›
3250 ultimately AOT_show ‹□[F]x⇩1...x⇩n›
3251 using "→E" by blast
3252next
3253 AOT_assume ‹∀x⇩1...∀x⇩n (◇[F]x⇩1...x⇩n → □[F]x⇩1...x⇩n)›
3254 AOT_hence ‹◇[F]x⇩1...x⇩n → □[F]x⇩1...x⇩n› for x⇩1x⇩n
3255 using "∀E"(2) by blast
3256 AOT_hence ‹□([F]x⇩1...x⇩n → □[F]x⇩1...x⇩n)› for x⇩1x⇩n
3257 by (metis "≡E"(2) "sc-eq-box-box:1")
3258 AOT_hence 0: ‹∀x⇩1...∀x⇩n □([F]x⇩1...x⇩n → □[F]x⇩1...x⇩n)›
3259 by (rule GEN)
3260 AOT_thus ‹□(∀x⇩1...∀x⇩n ([F]x⇩1...x⇩n → □[F]x⇩1...x⇩n))›
3261 using "BF" "vdash-properties:10" by blast
3262qed
3263
3264AOT_theorem "rigid-rel-thms:2":
3265 ‹□(∀x⇩1...∀x⇩n ([F]x⇩1...x⇩n → □[F]x⇩1...x⇩n)) ≡ ∀x⇩1...∀x⇩n(□[F]x⇩1...x⇩n ∨ □¬[F]x⇩1...x⇩n)›
3266proof(safe intro!: "≡I" "→I")
3267 AOT_assume ‹□(∀x⇩1...∀x⇩n ([F]x⇩1...x⇩n → □[F]x⇩1...x⇩n))›
3268 AOT_hence 0: ‹∀x⇩1...∀x⇩n □([F]x⇩1...x⇩n → □[F]x⇩1...x⇩n)›
3269 using CBF[THEN "→E"] by blast
3270 AOT_show ‹∀x⇩1...∀x⇩n(□[F]x⇩1...x⇩n ∨ □¬[F]x⇩1...x⇩n)›
3271 proof(rule GEN)
3272 fix x⇩1x⇩n
3273 AOT_have 1: ‹□([F]x⇩1...x⇩n → □[F]x⇩1...x⇩n)›
3274 using 0[THEN "∀E"(2)].
3275 AOT_hence 2: ‹◇[F]x⇩1...x⇩n → [F]x⇩1...x⇩n›
3276 using "B◇" "Hypothetical Syllogism" "K◇" "vdash-properties:10" by blast
3277 AOT_have ‹[F]x⇩1...x⇩n ∨ ¬[F]x⇩1...x⇩n›
3278 using "exc-mid".
3279 moreover {
3280 AOT_assume ‹[F]x⇩1...x⇩n›
3281 AOT_hence ‹□[F]x⇩1...x⇩n›
3282 using 1[THEN "qml:2"[axiom_inst, THEN "→E"], THEN "→E"] by blast
3283 }
3284 moreover {
3285 AOT_assume 3: ‹¬[F]x⇩1...x⇩n›
3286 AOT_have ‹□¬[F]x⇩1...x⇩n›
3287 proof(rule "raa-cor:1")
3288 AOT_assume ‹¬□¬[F]x⇩1...x⇩n›
3289 AOT_hence ‹◇[F]x⇩1...x⇩n›
3290 by (AOT_subst_def "conventions:5")
3291 AOT_hence ‹[F]x⇩1...x⇩n› using 2[THEN "→E"] by blast
3292 AOT_thus ‹[F]x⇩1...x⇩n & ¬[F]x⇩1...x⇩n›
3293 using 3 "&I" by blast
3294 qed
3295 }
3296 ultimately AOT_show ‹□[F]x⇩1...x⇩n ∨ □¬[F]x⇩1...x⇩n›
3297 by (metis "∨I"(1,2) "raa-cor:1")
3298 qed
3299next
3300 AOT_assume 0: ‹∀x⇩1...∀x⇩n(□[F]x⇩1...x⇩n ∨ □¬[F]x⇩1...x⇩n)›
3301 {
3302 fix x⇩1x⇩n
3303 AOT_have ‹□[F]x⇩1...x⇩n ∨ □¬[F]x⇩1...x⇩n› using 0[THEN "∀E"(2)] by blast
3304 moreover {
3305 AOT_assume ‹□[F]x⇩1...x⇩n›
3306 AOT_hence ‹□□[F]x⇩1...x⇩n›
3307 using "S5Basic:6"[THEN "≡E"(1)] by blast
3308 AOT_hence ‹□([F]x⇩1...x⇩n → □[F]x⇩1...x⇩n)›
3309 using "KBasic:1"[THEN "→E"] by blast
3310 }
3311 moreover {
3312 AOT_assume ‹□¬[F]x⇩1...x⇩n›
3313 AOT_hence ‹□([F]x⇩1...x⇩n → □[F]x⇩1...x⇩n)›
3314 using "KBasic:2"[THEN "→E"] by blast
3315 }
3316 ultimately AOT_have ‹□([F]x⇩1...x⇩n → □[F]x⇩1...x⇩n)›
3317 using "con-dis-i-e:4:b" "raa-cor:1" by blast
3318 }
3319 AOT_hence ‹∀x⇩1...∀x⇩n □([F]x⇩1...x⇩n → □[F]x⇩1...x⇩n)›
3320 by (rule GEN)
3321 AOT_thus ‹□(∀x⇩1...∀x⇩n ([F]x⇩1...x⇩n → □[F]x⇩1...x⇩n))›
3322 using BF[THEN "→E"] by fast
3323qed
3324
3325AOT_theorem "rigid-rel-thms:3": ‹Rigid(F) ≡ ∀x⇩1...∀x⇩n (□[F]x⇩1...x⇩n ∨ □¬[F]x⇩1...x⇩n)›
3326 by (AOT_subst_thm "df-rigid-rel:1"[THEN "≡Df", THEN "≡S"(1), OF "cqt:2"(1)];
3327 AOT_subst_thm "rigid-rel-thms:2")
3328 (simp add: "oth-class-taut:3:a")
3329
3330AOT_theorem "poss-sit-part-w:1": ‹Possible(s) ≡ ∃w(s ⊴ w)›
3331proof(safe intro!: "≡I" "→I")
3332 AOT_assume ‹Possible(s)›
3333 AOT_hence ‹◇Actual(s)›
3334 using "≡⇩d⇩fE" "con-dis-i-e:2:b" pos by blast
3335 AOT_hence ‹◇∀p (s ⊨ p → p)›
3336 apply (AOT_subst (reverse) ‹∀p (s ⊨ p → p)› ‹Actual(s)›)
3337 using "df-simplify:1" "rule-eq-df:1" Situation.restricted_var_condition actual apply blast
3338 by auto
3339 AOT_hence ‹∃w w ⊨ ∀p (s ⊨ p → p)›
3340 by (safe intro!: "fund:1"[unvarify p, THEN "≡E"(1)] "log-prop-prop:2")
3341 then AOT_obtain w where ‹w ⊨ ∀p (s ⊨ p → p)›
3342 using PossibleWorld.instantiation by meson
3343 AOT_hence 1: ‹∀p w ⊨ (s ⊨ p → p)›
3344 using "conj-dist-w:5"
3345 using "intro-elim:3:a" by blast
3346 AOT_have ‹s ⊴ w›
3347 proof(safe intro!: "sit-part-whole"[THEN "≡⇩d⇩fI"] "&I" "Situation.ψ" GEN "→I")
3348 AOT_show ‹Situation(w)›
3349 using "≡⇩d⇩fE" "con-dis-i-e:2:a" "world-pos" pos by blast
3350 next
3351 fix p
3352 AOT_assume ‹s ⊨ p›
3353 AOT_hence ‹□s ⊨ p›
3354 using "intro-elim:3:a" "lem2:1" by blast
3355 AOT_hence ‹∀w w ⊨ s ⊨ p›
3356 by (safe intro!: "fund:2"[unvarify p, THEN "≡E"(1)] "log-prop-prop:2")
3357 AOT_hence ‹w ⊨ s ⊨ p›
3358 using "rule-ui:3" "vdash-properties:10" PossibleWorld.restricted_var_condition by blast
3359 moreover AOT_have ‹w ⊨ (s ⊨ p → p)›
3360 using 1 "∀E" by blast
3361 ultimately AOT_show ‹w ⊨ p›
3362 using "conj-dist-w:2"[unvarify p, THEN "≡E"(1)] "log-prop-prop:2" "→E" by blast
3363 qed
3364 AOT_thus ‹∃w(s ⊴ w)›
3365 using "PossibleWorld.∃I" by blast
3366next
3367 AOT_assume ‹∃w(s ⊴ w)›
3368 then AOT_obtain w where ‹s ⊴ w›
3369 using "PossibleWorld.∃E" by meson
3370 AOT_hence 1: ‹∀p (s ⊨ p → w ⊨ p)›
3371 using "sit-part-whole"[THEN "≡⇩d⇩fE"] "&E" by blast
3372 AOT_have ‹∀p (w ⊨ (s ⊨ p → p))›
3373 proof (safe intro!: GEN "conj-dist-w:2"[unvarify p, THEN "≡E"(2)] "log-prop-prop:2" "→I")
3374 fix p
3375 AOT_assume ‹w ⊨ s ⊨ p›
3376 AOT_hence ‹◇s ⊨ p›
3377 by (auto intro!: "fund:1"[unvarify p, THEN "≡E"(2)] "log-prop-prop:2" "PossibleWorld.∃I")
3378 AOT_hence ‹s ⊨ p›
3379 using "intro-elim:3:a" "lem2:2" by blast
3380 AOT_thus ‹w ⊨ p›
3381 using 1 "log-prop-prop:2" "rule-ui:1" "vdash-properties:10" by blast
3382 qed
3383 AOT_hence ‹w ⊨ ∀p (s ⊨ p → p)›
3384 by (metis "≡E"(2) "conj-dist-w:5")
3385 AOT_hence ‹◇∀p (s ⊨ p → p)›
3386 by (safe intro!: "fund:1"[unvarify p, THEN "≡E"(2)] "log-prop-prop:2" PossibleWorld.existential)
3387 AOT_hence ‹◇Actual(s)›
3388 by (AOT_subst_def actual)
3389 (metis "KBasic:16" "&I" "→E" RN "Situation.ψ")
3390 AOT_thus ‹Possible(s)›
3391 by(safe intro!: "pos"[THEN "≡⇩d⇩fI"] "&I" "Situation.ψ")
3392qed
3393
3394AOT_define GapOn :: ‹τ ⇒ φ ⇒ φ› (‹GapOn'(_,_')›)
3395 "routley-star:5": ‹GapOn(s,p) ≡⇩d⇩f ¬s ⊨ p & ¬s ⊨ ¬p›
3396
3397
3398end
3399
3400