Theory AOT_ExtendedRelationComprehension
1theory AOT_ExtendedRelationComprehension
2 imports AOT_RestrictedVariables
3begin
4
5section‹Extended Relation Comprehension›
6
7text‹This theory depends on choosing extended models.›
8interpretation AOT_ExtendedModel by (standard; auto)
9
10text‹Auxiliary lemma: negations of denoting relations denote.›
11AOT_theorem negation_denotes: ‹[λx φ{x}]↓ → [λx ¬φ{x}]↓›
12proof(rule "→I")
13 AOT_assume 0: ‹[λx φ{x}]↓›
14 AOT_show ‹[λx ¬φ{x}]↓›
15 proof (rule "safe-ext"[axiom_inst, THEN "→E", OF "&I"])
16 AOT_show ‹[λx ¬[λx φ{x}]x]↓› by "cqt:2"
17 next
18 AOT_have ‹□[λx φ{x}]↓›
19 using 0 "exist-nec"[THEN "→E"] by blast
20 moreover AOT_have ‹□[λx φ{x}]↓ → □∀x (¬[λx φ{x}]x ≡ ¬φ{x})›
21 by(rule RM; safe intro!: GEN "≡I" "→I" "β→C"(2) "β←C"(2) "cqt:2")
22 ultimately AOT_show ‹□∀x (¬[λx φ{x}]x ≡ ¬φ{x})›
23 using "→E" by blast
24 qed
25qed
26
27text‹Auxiliary lemma: conjunctions of denoting relations denote.›
28AOT_theorem conjunction_denotes: ‹[λx φ{x}]↓ & [λx ψ{x}]↓ → [λx φ{x} & ψ{x}]↓›
29proof(rule "→I")
30 AOT_assume 0: ‹[λx φ{x}]↓ & [λx ψ{x}]↓›
31 AOT_show ‹[λx φ{x} & ψ{x}]↓›
32 proof (rule "safe-ext"[axiom_inst, THEN "→E", OF "&I"])
33 AOT_show ‹[λx [λx φ{x}]x & [λx ψ{x}]x]↓› by "cqt:2"
34 next
35 AOT_have ‹□([λx φ{x}]↓ & [λx ψ{x}]↓)›
36 using 0 "exist-nec"[THEN "→E"] "&E"
37 "KBasic:3" "df-simplify:2" "intro-elim:3:b" by blast
38 moreover AOT_have
39 ‹□([λx φ{x}]↓ & [λx ψ{x}]↓) → □∀x ([λx φ{x}]x & [λx ψ{x}]x ≡ φ{x} & ψ{x})›
40 by(rule RM; auto intro!: GEN "≡I" "→I" "cqt:2" "&I"
41 intro: "β←C"
42 dest: "&E" "β→C")
43 ultimately AOT_show ‹□∀x ([λx φ{x}]x & [λx ψ{x}]x ≡ φ{x} & ψ{x})›
44 using "→E" by blast
45 qed
46qed
47
48AOT_register_rigid_restricted_type
49 Ordinary: ‹O!κ›
50proof
51 AOT_modally_strict {
52 AOT_show ‹∃x O!x›
53 by (meson "B◇" "T◇" "o-objects-exist:1" "→E")
54 }
55next
56 AOT_modally_strict {
57 AOT_show ‹O!κ → κ↓› for κ
58 by (simp add: "→I" "cqt:5:a[1]"[axiom_inst, THEN "→E", THEN "&E"(2)])
59 }
60next
61 AOT_modally_strict {
62 AOT_show ‹∀α(O!α → □O!α)›
63 by (simp add: GEN "oa-facts:1")
64 }
65qed
66
67AOT_register_variable_names
68 Ordinary: u v r t s
69
70text‹In PLM this is defined in the Natural Numbers chapter,
71 but since it is helpful for stating the comprehension principles,
72 we already define it here.›
73AOT_define eqE :: ‹τ ⇒ τ ⇒ φ› (infixl ‹≡⇩E› 50)
74 eqE: ‹F ≡⇩E G ≡⇩d⇩f F↓ & G↓ & ∀u ([F]u ≡ [G]u)›
75
76text‹Derive existence claims about relations from the axioms.›
77AOT_theorem denotes_all: ‹[λx ∀G (□G ≡⇩E F → x[G])]↓›
78 and denotes_all_neg: ‹[λx ∀G (□G ≡⇩E F → ¬x[G])]↓›
79proof -
80 AOT_have Aux: ‹∀F (□F ≡⇩E G → (x[F] ≡ x[G])), ¬(x[G] ≡ y[G])
81 ❙⊢⇩□ ∃F([F]x & ¬[F]y)› for x y G
82 proof -
83 AOT_modally_strict {
84 AOT_assume 0: ‹∀F (□F ≡⇩E G → (x[F] ≡ x[G]))›
85 AOT_assume G_prop: ‹¬(x[G] ≡ y[G])›
86 {
87 AOT_assume ‹¬∃F([F]x & ¬[F]y)›
88 AOT_hence 0: ‹∀F ¬([F]x & ¬[F]y)›
89 by (metis "cqt-further:4" "→E")
90 AOT_have ‹∀F ([F]x ≡ [F]y)›
91 proof (rule GEN; rule "≡I"; rule "→I")
92 fix F
93 AOT_assume ‹[F]x›
94 moreover AOT_have ‹¬([F]x & ¬[F]y)›
95 using 0[THEN "∀E"(2)] by blast
96 ultimately AOT_show ‹[F]y›
97 by (metis "&I" "raa-cor:1")
98 next
99 fix F
100 AOT_assume ‹[F]y›
101 AOT_hence ‹¬[λx ¬[F]x]y›
102 by (metis "¬¬I" "β→C"(2))
103 moreover AOT_have ‹¬([λx ¬[F]x]x & ¬[λx ¬[F]x]y)›
104 apply (rule 0[THEN "∀E"(1)]) by "cqt:2[lambda]"
105 ultimately AOT_have 1: ‹¬[λx ¬[F]x]x›
106 by (metis "&I" "raa-cor:3")
107 {
108 AOT_assume ‹¬[F]x›
109 AOT_hence ‹[λx ¬[F]x]x›
110 by (auto intro!: "β←C"(1) "cqt:2")
111 AOT_hence ‹p & ¬p› for p
112 using 1 by (metis "raa-cor:3")
113 }
114 AOT_thus ‹[F]x› by (metis "raa-cor:1")
115 qed
116 AOT_hence ‹□∀F ([F]x ≡ [F]y)›
117 using "ind-nec"[THEN "→E"] by blast
118 AOT_hence ‹∀F □([F]x ≡ [F]y)›
119 by (metis "CBF" "→E")
120 } note indistI = this
121 {
122 AOT_assume G_prop: ‹x[G] & ¬y[G]›
123 AOT_hence Ax: ‹A!x›
124 using "&E"(1) "∃I"(2) "→E" "encoders-are-abstract" by blast
125
126 {
127 AOT_assume Ay: ‹A!y›
128 {
129 fix F
130 {
131 AOT_assume ‹∀u□([F]u ≡ [G]u)›
132 AOT_hence ‹□∀u([F]u ≡ [G]u)›
133 using "Ordinary.res-var-bound-reas[BF]"[THEN "→E"] by simp
134 AOT_hence ‹□F ≡⇩E G›
135 by (AOT_subst ‹F ≡⇩E G› ‹∀u ([F]u ≡ [G]u)›)
136 (auto intro!: "eqE"[THEN "≡Df", THEN "≡S"(1), OF "&I"] "cqt:2")
137 AOT_hence ‹x[F] ≡ x[G]›
138 using 0[THEN "∀E"(2)] "≡E" "→E" by meson
139 AOT_hence ‹x[F]›
140 using G_prop "&E" "≡E" by blast
141 }
142 AOT_hence ‹∀u□([F]u ≡ [G]u) → x[F]›
143 by (rule "→I")
144 }
145 AOT_hence xprop: ‹∀F(∀u□([F]u ≡ [G]u) → x[F])›
146 by (rule GEN)
147 moreover AOT_have yprop: ‹¬∀F(∀u□([F]u ≡ [G]u) → y[F])›
148 proof (rule "raa-cor:2")
149 AOT_assume ‹∀F(∀u□([F]u ≡ [G]u) → y[F])›
150 AOT_hence ‹∀F(□∀u([F]u ≡ [G]u) → y[F])›
151 apply (AOT_subst ‹□∀u([F]u ≡ [G]u)› ‹∀u□([F]u ≡ [G]u)› for: F)
152 using "Ordinary.res-var-bound-reas[BF]"
153 "Ordinary.res-var-bound-reas[CBF]"
154 "intro-elim:2" apply presburger
155 by simp
156 AOT_hence A: ‹∀F(□F ≡⇩E G → y[F])›
157 by (AOT_subst ‹F ≡⇩E G› ‹∀u ([F]u ≡ [G]u)› for: F)
158 (auto intro!: "eqE"[THEN "≡Df", THEN "≡S"(1), OF "&I"] "cqt:2")
159 moreover AOT_have ‹□G ≡⇩E G›
160 by (auto intro!: "eqE"[THEN "≡⇩d⇩fI"] "cqt:2" RN "&I" GEN "→I" "≡I")
161 ultimately AOT_have ‹y[G]› using "∀E"(2) "→E" by blast
162 AOT_thus ‹p & ¬p› for p using G_prop "&E" by (metis "raa-cor:3")
163 qed
164 AOT_have ‹∃F([F]x & ¬[F]y)›
165 proof(rule "raa-cor:1")
166 AOT_assume ‹¬∃F([F]x & ¬[F]y)›
167 AOT_hence indist: ‹∀F □([F]x ≡ [F]y)› using indistI by blast
168 AOT_have ‹∀F(∀u□([F]u ≡ [G]u) → y[F])›
169 using indistinguishable_ord_enc_all[axiom_inst, THEN "→E", OF "&I",
170 OF "&I", OF "&I", OF "cqt:2[const_var]"[axiom_inst],
171 OF Ax, OF Ay, OF indist, THEN "≡E"(1), OF xprop].
172 AOT_thus ‹∀F(∀u□([F]u ≡ [G]u) → y[F]) & ¬∀F(∀u□([F]u ≡ [G]u) → y[F])›
173 using yprop "&I" by blast
174 qed
175 }
176 moreover {
177 AOT_assume notAy: ‹¬A!y›
178 AOT_have ‹∃F([F]x & ¬[F]y)›
179 apply (rule "∃I"(1)[where τ=‹«A!»›])
180 using Ax notAy "&I" apply blast
181 by (simp add: "oa-exist:2")
182 }
183 ultimately AOT_have ‹∃F([F]x & ¬[F]y)›
184 by (metis "raa-cor:1")
185 }
186 moreover {
187 AOT_assume G_prop: ‹¬x[G] & y[G]›
188 AOT_hence Ay: ‹A!y›
189 by (meson "&E"(2) "encoders-are-abstract" "existential:2[const_var]" "→E")
190 AOT_hence notOy: ‹¬O!y›
191 using "≡E"(1) "oa-contingent:3" by blast
192 {
193 AOT_assume Ax: ‹A!x›
194 {
195 fix F
196 {
197 AOT_assume ‹□∀u([F]u ≡ [G]u)›
198 AOT_hence ‹□F ≡⇩E G›
199 by (AOT_subst ‹F ≡⇩E G› ‹∀u([F]u ≡ [G]u)›)
200 (auto intro!: "eqE"[THEN "≡Df", THEN "≡S"(1), OF "&I"] "cqt:2")
201 AOT_hence ‹x[F] ≡ x[G]›
202 using 0[THEN "∀E"(2)] "≡E" "→E" by meson
203 AOT_hence ‹¬x[F]›
204 using G_prop "&E" "≡E" by blast
205 }
206 AOT_hence ‹□∀u([F]u ≡ [G]u) → ¬x[F]›
207 by (rule "→I")
208 }
209 AOT_hence x_prop: ‹∀F(□∀u([F]u ≡ [G]u) → ¬x[F])›
210 by (rule GEN)
211 AOT_have x_prop: ‹¬∃F(∀u□([F]u ≡ [G]u) & x[F])›
212 proof (rule "raa-cor:2")
213 AOT_assume ‹∃F(∀u □([F]u ≡ [G]u) & x[F])›
214 then AOT_obtain F where F_prop: ‹∀u □([F]u ≡ [G]u) & x[F]›
215 using "∃E"[rotated] by blast
216 AOT_have ‹□([F]u ≡ [G]u)› for u
217 using F_prop[THEN "&E"(1), THEN "Ordinary.∀E"].
218 AOT_hence ‹∀u □([F]u ≡ [G]u)›
219 by (rule Ordinary.GEN)
220 AOT_hence ‹□∀u([F]u ≡ [G]u)›
221 by (metis "Ordinary.res-var-bound-reas[BF]" "→E")
222 AOT_hence ‹¬x[F]›
223 using x_prop[THEN "∀E"(2), THEN "→E"] by blast
224 AOT_thus ‹p & ¬p› for p
225 using F_prop[THEN "&E"(2)] by (metis "raa-cor:3")
226 qed
227 AOT_have y_prop: ‹∃F(∀u □([F]u ≡ [G]u) & y[F])›
228 proof (rule "raa-cor:1")
229 AOT_assume ‹¬∃F (∀u □([F]u ≡ [G]u) & y[F])›
230 AOT_hence 0: ‹∀F ¬(∀u □([F]u ≡ [G]u) & y[F])›
231 using "cqt-further:4"[THEN "→E"] by blast
232 {
233 fix F
234 {
235 AOT_assume ‹∀u □([F]u ≡ [G]u)›
236 AOT_hence ‹¬y[F]›
237 using 0[THEN "∀E"(2)] "&I" "raa-cor:1" by meson
238 }
239 AOT_hence ‹(∀u □([F]u ≡ [G]u) → ¬y[F])›
240 by (rule "→I")
241 }
242 AOT_hence A: ‹∀F(∀u □([F]u ≡ [G]u) → ¬y[F])›
243 by (rule GEN)
244 moreover AOT_have ‹∀u □([G]u ≡ [G]u)›
245 by (simp add: RN "oth-class-taut:3:a" "universal-cor" "→I")
246 ultimately AOT_have ‹¬y[G]›
247 using "∀E"(2) "→E" by blast
248 AOT_thus ‹p & ¬p› for p
249 using G_prop "&E" by (metis "raa-cor:3")
250 qed
251 AOT_have ‹∃F([F]x & ¬[F]y)›
252 proof(rule "raa-cor:1")
253 AOT_assume ‹¬∃F([F]x & ¬[F]y)›
254 AOT_hence indist: ‹∀F □([F]x ≡ [F]y)›
255 using indistI by blast
256 AOT_thus ‹∃F(∀u □([F]u ≡ [G]u) & x[F]) & ¬∃F(∀u □([F]u ≡ [G]u) & x[F])›
257 using indistinguishable_ord_enc_ex[axiom_inst, THEN "→E", OF "&I",
258 OF "&I", OF "&I", OF "cqt:2[const_var]"[axiom_inst],
259 OF Ax, OF Ay, OF indist, THEN "≡E"(2), OF y_prop]
260 x_prop "&I" by blast
261 qed
262 }
263 moreover {
264 AOT_assume notAx: ‹¬A!x›
265 AOT_hence Ox: ‹O!x›
266 using "∨E"(3) "oa-exist:3" by blast
267 AOT_have ‹∃F([F]x & ¬[F]y)›
268 apply (rule "∃I"(1)[where τ=‹«O!»›])
269 using Ox notOy "&I" apply blast
270 by (simp add: "oa-exist:1")
271 }
272 ultimately AOT_have ‹∃F([F]x & ¬[F]y)›
273 by (metis "raa-cor:1")
274 }
275 ultimately AOT_show ‹∃F([F]x & ¬[F]y)›
276 using G_prop by (metis "&I" "→I" "≡I" "raa-cor:1")
277 }
278 qed
279
280 AOT_modally_strict {
281 fix x y
282 AOT_assume indist: ‹∀F ([F]x ≡ [F]y)›
283 AOT_hence nec_indist: ‹□∀F ([F]x ≡ [F]y)›
284 using "ind-nec" "vdash-properties:10" by blast
285 AOT_hence indist_nec: ‹∀F □([F]x ≡ [F]y)›
286 using "CBF" "vdash-properties:10" by blast
287 AOT_assume 0: ‹∀G (□G ≡⇩E F → x[G])›
288 AOT_hence 1: ‹∀G (□∀u ([G]u ≡ [F]u) → x[G])›
289 by (AOT_subst (reverse) ‹∀u ([G]u ≡ [F]u)› ‹G ≡⇩E F› for: G)
290 (auto intro!: "eqE"[THEN "≡Df", THEN "≡S"(1), OF "&I"] "cqt:2")
291 AOT_have ‹x[F]›
292 by (safe intro!: 1[THEN "∀E"(2), THEN "→E"] GEN "→I" RN "≡I")
293 AOT_have ‹∀G (□G ≡⇩E F → y[G])›
294 proof(rule "raa-cor:1")
295 AOT_assume ‹¬∀G (□G ≡⇩E F → y[G])›
296 AOT_hence ‹∃G ¬(□G ≡⇩E F → y[G])›
297 using "cqt-further:2" "→E" by blast
298 then AOT_obtain G where G_prop: ‹¬(□G ≡⇩E F → y[G])›
299 using "∃E"[rotated] by blast
300 AOT_hence 1: ‹□G ≡⇩E F & ¬y[G]›
301 by (metis "≡E"(1) "oth-class-taut:1:b")
302 AOT_have xG: ‹x[G]›
303 using 0[THEN "∀E"(2), THEN "→E"] 1[THEN "&E"(1)] by blast
304 AOT_hence ‹x[G] & ¬y[G]›
305 using 1[THEN "&E"(2)] "&I" by blast
306 AOT_hence B: ‹¬(x[G] ≡ y[G])›
307 using "&E"(2) "≡E"(1) "reductio-aa:1" xG by blast
308 {
309 fix H
310 {
311 AOT_assume ‹□H ≡⇩E G›
312 AOT_hence ‹□(H ≡⇩E G & G ≡⇩E F)›
313 using 1 by (metis "KBasic:3" "con-dis-i-e:1" "con-dis-i-e:2:a"
314 "intro-elim:3:b")
315 moreover AOT_have ‹□(H ≡⇩E G & G ≡⇩E F) → □(H ≡⇩E F)›
316 proof(rule RM)
317 AOT_modally_strict {
318 AOT_show ‹H ≡⇩E G & G ≡⇩E F → H ≡⇩E F›
319 proof (safe intro!: "→I" "eqE"[THEN "≡⇩d⇩fI"] "&I" "cqt:2" Ordinary.GEN)
320 fix u
321 AOT_assume ‹H ≡⇩E G & G ≡⇩E F›
322 AOT_hence ‹∀u ([H]u ≡ [G]u)› and ‹∀u ([G]u ≡ [F]u)›
323 using "eqE"[THEN "≡⇩d⇩fE"] "&E" by blast+
324 AOT_thus ‹[H]u ≡ [F]u›
325 by (auto dest!: "Ordinary.∀E" dest: "≡E")
326 qed
327 }
328 qed
329 ultimately AOT_have ‹□(H ≡⇩E F)›
330 using "→E" by blast
331 AOT_hence ‹x[H]›
332 using 0[THEN "∀E"(2)] "→E" by blast
333 AOT_hence ‹x[H] ≡ x[G]›
334 using xG "≡I" "→I" by blast
335 }
336 AOT_hence ‹□H ≡⇩E G → (x[H] ≡ x[G])› by (rule "→I")
337 }
338 AOT_hence A: ‹∀H(□H ≡⇩E G → (x[H] ≡ x[G]))›
339 by (rule GEN)
340 then AOT_obtain F where F_prop: ‹[F]x & ¬[F]y›
341 using Aux[OF A, OF B] "∃E"[rotated] by blast
342 moreover AOT_have ‹[F]y›
343 using indist[THEN "∀E"(2), THEN "≡E"(1), OF F_prop[THEN "&E"(1)]].
344 AOT_thus ‹p & ¬p› for p
345 using F_prop[THEN "&E"(2)] by (metis "raa-cor:3")
346 qed
347 } note 0 = this
348 AOT_modally_strict {
349 fix x y
350 AOT_assume ‹∀F ([F]x ≡ [F]y)›
351 moreover AOT_have ‹∀F ([F]y ≡ [F]x)›
352 by (metis calculation "cqt-basic:11" "≡E"(2))
353 ultimately AOT_have ‹∀G (□G ≡⇩E F → x[G]) ≡ ∀G (□G ≡⇩E F → y[G])›
354 using 0 "≡I" "→I" by auto
355 } note 1 = this
356 AOT_show ‹[λx ∀G (□G ≡⇩E F → x[G])]↓›
357 by (safe intro!: RN GEN "→I" 1 "kirchner-thm:2"[THEN "≡E"(2)])
358
359 AOT_modally_strict {
360 fix x y
361 AOT_assume indist: ‹∀F ([F]x ≡ [F]y)›
362 AOT_hence nec_indist: ‹□∀F ([F]x ≡ [F]y)›
363 using "ind-nec" "vdash-properties:10" by blast
364 AOT_hence indist_nec: ‹∀F □([F]x ≡ [F]y)›
365 using "CBF" "vdash-properties:10" by blast
366 AOT_assume 0: ‹∀G (□G ≡⇩E F → ¬x[G])›
367 AOT_hence 1: ‹∀G (□∀u ([G]u ≡ [F]u) → ¬x[G])›
368 by (AOT_subst (reverse) ‹∀u ([G]u ≡ [F]u)› ‹G ≡⇩E F› for: G)
369 (auto intro!: "eqE"[THEN "≡Df", THEN "≡S"(1), OF "&I"] "cqt:2")
370 AOT_have ‹¬x[F]›
371 by (safe intro!: 1[THEN "∀E"(2), THEN "→E"] GEN "→I" RN "≡I")
372 AOT_have ‹∀G (□G ≡⇩E F → ¬y[G])›
373 proof(rule "raa-cor:1")
374 AOT_assume ‹¬∀G (□G ≡⇩E F → ¬y[G])›
375 AOT_hence ‹∃G ¬(□G ≡⇩E F → ¬y[G])›
376 using "cqt-further:2" "→E" by blast
377 then AOT_obtain G where G_prop: ‹¬(□G ≡⇩E F → ¬y[G])›
378 using "∃E"[rotated] by blast
379 AOT_hence 1: ‹□G ≡⇩E F & ¬¬y[G]›
380 by (metis "≡E"(1) "oth-class-taut:1:b")
381 AOT_hence yG: ‹y[G]›
382 using G_prop "→I" "raa-cor:3" by blast
383 moreover AOT_hence 12: ‹¬x[G]›
384 using 0[THEN "∀E"(2), THEN "→E"] 1[THEN "&E"(1)] by blast
385 ultimately AOT_have ‹¬x[G] & y[G]›
386 using "&I" by blast
387 AOT_hence B: ‹¬(x[G] ≡ y[G])›
388 by (metis "12" "≡E"(3) "raa-cor:3" yG)
389 {
390 fix H
391 {
392 AOT_assume 3: ‹□H ≡⇩E G›
393 AOT_hence ‹□(H ≡⇩E G & G ≡⇩E F)›
394 using 1
395 by (metis "KBasic:3" "con-dis-i-e:1" "→I" "intro-elim:3:b"
396 "reductio-aa:1" G_prop)
397 moreover AOT_have ‹□(H ≡⇩E G & G ≡⇩E F) → □(H ≡⇩E F)›
398 proof (rule RM)
399 AOT_modally_strict {
400 AOT_show ‹H ≡⇩E G & G ≡⇩E F → H ≡⇩E F›
401 proof (safe intro!: "→I" "eqE"[THEN "≡⇩d⇩fI"] "&I" "cqt:2" Ordinary.GEN)
402 fix u
403 AOT_assume ‹H ≡⇩E G & G ≡⇩E F›
404 AOT_hence ‹∀u ([H]u ≡ [G]u)› and ‹∀u ([G]u ≡ [F]u)›
405 using "eqE"[THEN "≡⇩d⇩fE"] "&E" by blast+
406 AOT_thus ‹[H]u ≡ [F]u›
407 by (auto dest!: "Ordinary.∀E" dest: "≡E")
408 qed
409 }
410 qed
411 ultimately AOT_have ‹□(H ≡⇩E F)›
412 using "→E" by blast
413 AOT_hence ‹¬x[H]›
414 using 0[THEN "∀E"(2)] "→E" by blast
415 AOT_hence ‹x[H] ≡ x[G]›
416 using 12 "≡I" "→I" by (metis "raa-cor:3")
417 }
418 AOT_hence ‹□H ≡⇩E G → (x[H] ≡ x[G])›
419 by (rule "→I")
420 }
421 AOT_hence A: ‹∀H(□H ≡⇩E G → (x[H] ≡ x[G]))›
422 by (rule GEN)
423 then AOT_obtain F where F_prop: ‹[F]x & ¬[F]y›
424 using Aux[OF A, OF B] "∃E"[rotated] by blast
425 moreover AOT_have ‹[F]y›
426 using indist[THEN "∀E"(2), THEN "≡E"(1), OF F_prop[THEN "&E"(1)]].
427 AOT_thus ‹p & ¬p› for p
428 using F_prop[THEN "&E"(2)] by (metis "raa-cor:3")
429 qed
430 } note 0 = this
431 AOT_modally_strict {
432 fix x y
433 AOT_assume ‹∀F ([F]x ≡ [F]y)›
434 moreover AOT_have ‹∀F ([F]y ≡ [F]x)›
435 by (metis calculation "cqt-basic:11" "≡E"(2))
436 ultimately AOT_have ‹∀G (□G ≡⇩E F → ¬x[G]) ≡ ∀G (□G ≡⇩E F → ¬y[G])›
437 using 0 "≡I" "→I" by auto
438 } note 1 = this
439 AOT_show ‹[λx ∀G (□G ≡⇩E F → ¬x[G])]↓›
440 by (safe intro!: RN GEN "→I" 1 "kirchner-thm:2"[THEN "≡E"(2)])
441qed
442
443text‹Reformulate the existence claims in terms of their negations.›
444
445AOT_theorem denotes_ex: ‹[λx ∃G (□G ≡⇩E F & x[G])]↓›
446proof (rule "safe-ext"[axiom_inst, THEN "→E", OF "&I"])
447 AOT_show ‹[λx ¬∀G (□G ≡⇩E F → ¬x[G])]↓›
448 using denotes_all_neg[THEN negation_denotes[THEN "→E"]].
449next
450 AOT_show ‹□∀x (¬∀G (□G ≡⇩E F → ¬x[G]) ≡ ∃G (□G ≡⇩E F & x[G]))›
451 by (AOT_subst ‹□G ≡⇩E F & x[G]› ‹¬(□G ≡⇩E F → ¬x[G])› for: G x)
452 (auto simp: "conventions:1" "rule-eq-df:1"
453 intro: "oth-class-taut:4:b"[THEN "≡E"(2)]
454 "intro-elim:3:f"[OF "cqt-further:3", OF "oth-class-taut:3:b"]
455 intro!: RN GEN)
456qed
457
458AOT_theorem denotes_ex_neg: ‹[λx ∃G (□G ≡⇩E F & ¬x[G])]↓›
459proof (rule "safe-ext"[axiom_inst, THEN "→E", OF "&I"])
460 AOT_show ‹[λx ¬∀G (□G ≡⇩E F → x[G])]↓›
461 using denotes_all[THEN negation_denotes[THEN "→E"]].
462next
463 AOT_show ‹□∀x (¬∀G (□G ≡⇩E F → x[G]) ≡ ∃G (□G ≡⇩E F & ¬x[G]))›
464 by (AOT_subst (reverse) ‹□G ≡⇩E F & ¬x[G]› ‹¬(□G ≡⇩E F → x[G])› for: G x)
465 (auto simp: "oth-class-taut:1:b"
466 intro: "oth-class-taut:4:b"[THEN "≡E"(2)]
467 "intro-elim:3:f"[OF "cqt-further:3", OF "oth-class-taut:3:b"]
468 intro!: RN GEN)
469qed
470
471text‹Derive comprehension principles.›
472
473AOT_theorem Comprehension_1:
474 shows ‹□∀F∀G(□G ≡⇩E F → (φ{F} ≡ φ{G})) → [λx ∃F (φ{F} & x[F])]↓›
475proof(rule "→I")
476 AOT_assume assm: ‹□∀F∀G(□G ≡⇩E F → (φ{F} ≡ φ{G}))›
477 AOT_modally_strict {
478 fix x y
479 AOT_assume 0: ‹∀F∀G (□G ≡⇩E F → (φ{F} ≡ φ{G}))›
480 AOT_assume indist: ‹∀F ([F]x ≡ [F]y)›
481 AOT_assume x_prop: ‹∃F (φ{F} & x[F])›
482 then AOT_obtain F where F_prop: ‹φ{F} & x[F]›
483 using "∃E"[rotated] by blast
484 AOT_hence ‹□F ≡⇩E F & x[F]›
485 by (auto intro!: RN eqE[THEN "≡⇩d⇩fI"] "&I" "cqt:2" GEN "≡I" "→I" dest: "&E")
486 AOT_hence ‹∃G(□G ≡⇩E F & x[G])›
487 by (rule "∃I")
488 AOT_hence ‹[λx ∃G(□G ≡⇩E F & x[G])]x›
489 by (safe intro!: "β←C" denotes_ex "cqt:2")
490 AOT_hence ‹[λx ∃G(□G ≡⇩E F & x[G])]y›
491 using indist[THEN "∀E"(1), OF denotes_ex, THEN "≡E"(1)] by blast
492 AOT_hence ‹∃G(□G ≡⇩E F & y[G])›
493 using "β→C" by blast
494 then AOT_obtain G where ‹□G ≡⇩E F & y[G]›
495 using "∃E"[rotated] by blast
496 AOT_hence ‹φ{G} & y[G]›
497 using 0[THEN "∀E"(2), THEN "∀E"(2), THEN "→E", THEN "≡E"(1)]
498 F_prop[THEN "&E"(1)] "&E" "&I" by blast
499 AOT_hence ‹∃F (φ{F} & y[F])›
500 by (rule "∃I")
501 } note 1 = this
502 AOT_modally_strict {
503 AOT_assume 0: ‹∀F∀G (□G ≡⇩E F → (φ{F} ≡ φ{G}))›
504 {
505 fix x y
506 {
507 AOT_assume ‹∀F ([F]x ≡ [F]y)›
508 moreover AOT_have ‹∀F ([F]y ≡ [F]x)›
509 by (metis calculation "cqt-basic:11" "≡E"(1))
510 ultimately AOT_have ‹∃F (φ{F} & x[F]) ≡ ∃F (φ{F} & y[F])›
511 using 0 1[OF 0] "≡I" "→I" by simp
512 }
513 AOT_hence ‹∀F ([F]x ≡ [F]y) → (∃F (φ{F} & x[F]) ≡ ∃F (φ{F} & y[F]))›
514 using "→I" by blast
515 }
516 AOT_hence ‹∀x∀y(∀F ([F]x ≡ [F]y) → (∃F (φ{F} & x[F]) ≡ ∃F (φ{F} & y[F])))›
517 by (auto intro!: GEN)
518 } note 1 = this
519 AOT_hence ‹❙⊢⇩□ ∀F∀G (□G ≡⇩E F → (φ{F} ≡ φ{G})) →
520 ∀x∀y(∀F ([F]x ≡ [F]y) → (∃F (φ{F} & x[F]) ≡ ∃F (φ{F} & y[F])))›
521 by (rule "→I")
522 AOT_hence ‹□∀F∀G (□G ≡⇩E F → (φ{F} ≡ φ{G})) →
523 □∀x∀y(∀F ([F]x ≡ [F]y) → (∃F (φ{F} & x[F]) ≡ ∃F (φ{F} & y[F])))›
524 by (rule RM)
525 AOT_hence ‹□∀x∀y(∀F ([F]x ≡ [F]y) → (∃F (φ{F} & x[F]) ≡ ∃F (φ{F} & y[F])))›
526 using "→E" assm by blast
527 AOT_thus ‹[λx ∃F (φ{F} & x[F])]↓›
528 by (safe intro!: "kirchner-thm:2"[THEN "≡E"(2)])
529qed
530
531AOT_theorem Comprehension_2:
532 shows ‹□∀F∀G(□G ≡⇩E F → (φ{F} ≡ φ{G})) → [λx ∃F (φ{F} & ¬x[F])]↓›
533proof(rule "→I")
534 AOT_assume assm: ‹□∀F∀G(□G ≡⇩E F → (φ{F} ≡ φ{G}))›
535 AOT_modally_strict {
536 fix x y
537 AOT_assume 0: ‹∀F∀G (□G ≡⇩E F → (φ{F} ≡ φ{G}))›
538 AOT_assume indist: ‹∀F ([F]x ≡ [F]y)›
539 AOT_assume x_prop: ‹∃F (φ{F} & ¬x[F])›
540 then AOT_obtain F where F_prop: ‹φ{F} & ¬x[F]›
541 using "∃E"[rotated] by blast
542 AOT_hence ‹□F ≡⇩E F & ¬x[F]›
543 by (auto intro!: RN eqE[THEN "≡⇩d⇩fI"] "&I" "cqt:2" GEN "≡I" "→I" dest: "&E")
544 AOT_hence ‹∃G(□G ≡⇩E F & ¬x[G])›
545 by (rule "∃I")
546 AOT_hence ‹[λx ∃G(□G ≡⇩E F & ¬x[G])]x›
547 by (safe intro!: "β←C" denotes_ex_neg "cqt:2")
548 AOT_hence ‹[λx ∃G(□G ≡⇩E F & ¬x[G])]y›
549 using indist[THEN "∀E"(1), OF denotes_ex_neg, THEN "≡E"(1)] by blast
550 AOT_hence ‹∃G(□G ≡⇩E F & ¬y[G])›
551 using "β→C" by blast
552 then AOT_obtain G where ‹□G ≡⇩E F & ¬y[G]›
553 using "∃E"[rotated] by blast
554 AOT_hence ‹φ{G} & ¬y[G]›
555 using 0[THEN "∀E"(2), THEN "∀E"(2), THEN "→E", THEN "≡E"(1)]
556 F_prop[THEN "&E"(1)] "&E" "&I" by blast
557 AOT_hence ‹∃F (φ{F} & ¬y[F])›
558 by (rule "∃I")
559 } note 1 = this
560 AOT_modally_strict {
561 AOT_assume 0: ‹∀F∀G (□G ≡⇩E F → (φ{F} ≡ φ{G}))›
562 {
563 fix x y
564 {
565 AOT_assume ‹∀F ([F]x ≡ [F]y)›
566 moreover AOT_have ‹∀F ([F]y ≡ [F]x)›
567 by (metis calculation "cqt-basic:11" "≡E"(1))
568 ultimately AOT_have ‹∃F (φ{F} & ¬x[F]) ≡ ∃F (φ{F} & ¬y[F])›
569 using 0 1[OF 0] "≡I" "→I" by simp
570 }
571 AOT_hence ‹∀F ([F]x ≡ [F]y) → (∃F (φ{F} & ¬x[F]) ≡ ∃F (φ{F} & ¬y[F]))›
572 using "→I" by blast
573 }
574 AOT_hence ‹∀x∀y(∀F ([F]x ≡ [F]y) → (∃F (φ{F} & ¬x[F]) ≡ ∃F (φ{F} & ¬y[F])))›
575 by (auto intro!: GEN)
576 } note 1 = this
577 AOT_hence ‹❙⊢⇩□ ∀F∀G (□G ≡⇩E F → (φ{F} ≡ φ{G})) →
578 ∀x∀y(∀F ([F]x ≡ [F]y) → (∃F (φ{F} & ¬x[F]) ≡ ∃F (φ{F} & ¬y[F])))›
579 by (rule "→I")
580 AOT_hence ‹□∀F∀G (□G ≡⇩E F → (φ{F} ≡ φ{G})) →
581 □∀x∀y(∀F ([F]x ≡ [F]y) → (∃F (φ{F} & ¬x[F]) ≡ ∃F (φ{F} & ¬y[F])))›
582 by (rule RM)
583 AOT_hence ‹□∀x∀y(∀F ([F]x ≡ [F]y) → (∃F (φ{F} & ¬x[F]) ≡ ∃F (φ{F} & ¬y[F])))›
584 using "→E" assm by blast
585 AOT_thus ‹[λx ∃F (φ{F} & ¬x[F])]↓›
586 by (safe intro!: "kirchner-thm:2"[THEN "≡E"(2)])
587qed
588
589text‹Derived variants of the comprehension principles above.›
590
591AOT_theorem Comprehension_1':
592 shows ‹□∀F∀G(□G ≡⇩E F → (φ{F} ≡ φ{G})) → [λx ∀F (x[F] → φ{F})]↓›
593proof(rule "→I")
594 AOT_assume ‹□∀F∀G(□G ≡⇩E F → (φ{F} ≡ φ{G}))›
595 AOT_hence 0: ‹□∀F∀G(□G ≡⇩E F → (¬φ{F} ≡ ¬φ{G}))›
596 by (AOT_subst (reverse) ‹¬φ{F} ≡ ¬φ{G}› ‹φ{F} ≡ φ{G}› for: F G)
597 (auto simp: "oth-class-taut:4:b")
598 AOT_show ‹[λx ∀F (x[F] → φ{F})]↓›
599 proof(rule "safe-ext"[axiom_inst, THEN "→E", OF "&I"])
600 AOT_show ‹[λx ¬∃F(¬φ{F} & x[F])]↓›
601 using Comprehension_1[THEN "→E", OF 0, THEN negation_denotes[THEN "→E"]].
602 next
603 AOT_show ‹□∀x (¬∃F (¬φ{F} & x[F]) ≡ ∀F (x[F] → φ{F}))›
604 by (AOT_subst (reverse) ‹¬φ{F} & x[F]› ‹¬(x[F] → φ{F})› for: F x)
605 (auto simp: "oth-class-taut:1:b"[THEN "intro-elim:3:e",
606 OF "oth-class-taut:2:a"]
607 intro: "intro-elim:3:f"[OF "cqt-further:3", OF "oth-class-taut:3:a",
608 symmetric]
609 intro!: RN GEN)
610 qed
611qed
612
613AOT_theorem Comprehension_2':
614 shows ‹□∀F∀G(□G ≡⇩E F → (φ{F} ≡ φ{G})) → [λx ∀F (φ{F} → x[F])]↓›
615proof(rule "→I")
616 AOT_assume 0: ‹□∀F∀G(□G ≡⇩E F → (φ{F} ≡ φ{G}))›
617 AOT_show ‹[λx ∀F (φ{F} → x[F])]↓›
618 proof(rule "safe-ext"[axiom_inst, THEN "→E", OF "&I"])
619 AOT_show ‹[λx ¬∃F(φ{F} & ¬x[F])]↓›
620 using Comprehension_2[THEN "→E", OF 0, THEN negation_denotes[THEN "→E"]].
621 next
622 AOT_show ‹□∀x (¬∃F (φ{F} & ¬x[F]) ≡ ∀F (φ{F} → x[F]))›
623 by (AOT_subst (reverse) ‹φ{F} & ¬x[F]› ‹¬(φ{F} → x[F])› for: F x)
624 (auto simp: "oth-class-taut:1:b"
625 intro: "intro-elim:3:f"[OF "cqt-further:3", OF "oth-class-taut:3:a",
626 symmetric]
627 intro!: RN GEN)
628 qed
629qed
630
631text‹Derive a combined comprehension principles.›
632
633AOT_theorem Comprehension_3:
634 ‹□∀F∀G(□G ≡⇩E F → (φ{F} ≡ φ{G})) → [λx ∀F (x[F] ≡ φ{F})]↓›
635proof(rule "→I")
636 AOT_assume 0: ‹□∀F∀G(□G ≡⇩E F → (φ{F} ≡ φ{G}))›
637 AOT_show ‹[λx ∀F (x[F] ≡ φ{F})]↓›
638 proof(rule "safe-ext"[axiom_inst, THEN "→E", OF "&I"])
639 AOT_show ‹[λx ∀F (x[F] → φ{F}) & ∀F (φ{F} → x[F])]↓›
640 by (safe intro!: conjunction_denotes[THEN "→E", OF "&I"]
641 Comprehension_1'[THEN "→E"]
642 Comprehension_2'[THEN "→E"] 0)
643 next
644 AOT_show ‹□∀x (∀F (x[F] → φ{F}) & ∀F (φ{F} → x[F]) ≡ ∀F (x[F] ≡ φ{F}))›
645 by (auto intro!: RN GEN "≡I" "→I" "&I" dest: "&E" "∀E"(2) "→E" "≡E"(1,2))
646 qed
647qed
648
649notepad
650begin
651text‹Verify that the original axioms are equivalent to @{thm denotes_ex}
652 and @{thm denotes_ex_neg}.›
653AOT_modally_strict {
654 fix x y H
655 AOT_have ‹A!x & A!y & ∀F □([F]x ≡ [F]y) →
656 (∀G (∀z (O!z → □([G]z ≡ [H]z)) → x[G]) ≡
657 ∀G (∀z (O!z → □([G]z ≡ [H]z)) → y[G]))›
658 proof(rule "→I")
659 {
660 fix x y
661 AOT_assume ‹A!x›
662 AOT_assume ‹A!y›
663 AOT_assume indist: ‹∀F □([F]x ≡ [F]y)›
664 AOT_assume ‹∀G (∀u □([G]u ≡ [H]u) → x[G])›
665 AOT_hence ‹∀G (□∀u ([G]u ≡ [H]u) → x[G])›
666 using "Ordinary.res-var-bound-reas[BF]" "Ordinary.res-var-bound-reas[CBF]"
667 "intro-elim:2"
668 by (AOT_subst ‹□∀u ([G]u ≡ [H]u)› ‹∀u □([G]u ≡ [H]u)› for: G) auto
669 AOT_hence ‹∀G (□G ≡⇩E H → x[G])›
670 by (AOT_subst ‹G ≡⇩E H› ‹∀u ([G]u ≡ [H]u)› for: G)
671 (safe intro!: "eqE"[THEN "≡Df", THEN "≡S"(1), OF "&I"] "cqt:2")
672 AOT_hence ‹¬∃G (□G ≡⇩E H & ¬x[G])›
673 by (AOT_subst (reverse) ‹(□G ≡⇩E H & ¬x[G])› ‹¬(□G ≡⇩E H → x[G])› for: G)
674 (auto simp: "oth-class-taut:1:b" "cqt-further:3"[THEN "≡E"(1)])
675 AOT_hence ‹¬[λx ∃G (□G ≡⇩E H & ¬x[G])]x›
676 by (auto intro: "β→C")
677 AOT_hence ‹¬[λx ∃G (□G ≡⇩E H & ¬x[G])]y›
678 using indist[THEN "∀E"(1), OF denotes_ex_neg,
679 THEN "qml:2"[axiom_inst, THEN "→E"],
680 THEN "≡E"(3)] by blast
681 AOT_hence ‹¬∃G (□G ≡⇩E H & ¬y[G])›
682 by (safe intro!: "β←C" denotes_ex_neg "cqt:2")
683 AOT_hence ‹∀G ¬(□G ≡⇩E H & ¬y[G])›
684 using "cqt-further:4"[THEN "→E"] by blast
685 AOT_hence ‹∀G(□G ≡⇩E H → y[G])›
686 by (AOT_subst ‹□G ≡⇩E H → y[G]› ‹¬(□G ≡⇩E H & ¬y[G])› for: G)
687 (auto simp: "oth-class-taut:1:a")
688 AOT_hence ‹∀G (□∀u([G]u ≡ [H]u) → y[G])›
689 by (AOT_subst (reverse) ‹∀u ([G]u ≡ [H]u)› ‹G ≡⇩E H› for: G)
690 (safe intro!: "eqE"[THEN "≡Df", THEN "≡S"(1), OF "&I"] "cqt:2")
691 AOT_hence ‹∀G (∀u □([G]u ≡ [H]u) → y[G])›
692 using "Ordinary.res-var-bound-reas[BF]" "Ordinary.res-var-bound-reas[CBF]"
693 "intro-elim:2"
694 by (AOT_subst ‹∀u □([G]u ≡ [H]u)› ‹□∀u ([G]u ≡ [H]u)› for: G) auto
695 } note 0 = this
696 AOT_assume ‹A!x & A!y & ∀F □([F]x ≡ [F]y)›
697 AOT_hence ‹A!x› and ‹A!y› and ‹∀F □([F]x ≡ [F]y)›
698 using "&E" by blast+
699 moreover AOT_have ‹∀F □([F]y ≡ [F]x)›
700 using calculation(3)
701 apply (safe intro!: CBF[THEN "→E"] dest!: BF[THEN "→E"])
702 using "RM:3" "cqt-basic:11" "intro-elim:3:b" by fast
703 ultimately AOT_show ‹∀G (∀u □([G]u ≡ [H]u) → x[G]) ≡
704 ∀G (∀u □([G]u ≡ [H]u) → y[G])›
705 using 0 by (auto intro!: "≡I" "→I")
706 qed
707
708 AOT_have ‹A!x & A!y & ∀F □([F]x ≡ [F]y) →
709 (∃G (∀z (O!z → □([G]z ≡ [H]z)) & x[G]) ≡ ∃G (∀z (O!z → □([G]z ≡ [H]z)) & y[G]))›
710 proof(rule "→I")
711 {
712 fix x y
713 AOT_assume ‹A!x›
714 AOT_assume ‹A!y›
715 AOT_assume indist: ‹∀F □([F]x ≡ [F]y)›
716 AOT_assume x_prop: ‹∃G (∀u □([G]u ≡ [H]u) & x[G])›
717 AOT_hence ‹∃G (□∀u ([G]u ≡ [H]u) & x[G])›
718 using "Ordinary.res-var-bound-reas[BF]" "Ordinary.res-var-bound-reas[CBF]"
719 "intro-elim:2"
720 by (AOT_subst ‹□∀u ([G]u ≡ [H]u)› ‹∀u □([G]u ≡ [H]u)› for: G) auto
721 AOT_hence ‹∃G (□G ≡⇩E H & x[G])›
722 by (AOT_subst ‹G ≡⇩E H› ‹∀u ([G]u ≡ [H]u)› for: G)
723 (safe intro!: "eqE"[THEN "≡Df", THEN "≡S"(1), OF "&I"] "cqt:2")
724 AOT_hence ‹[λx ∃G (□G ≡⇩E H & x[G])]x›
725 by (safe intro!: "β←C" denotes_ex "cqt:2")
726 AOT_hence ‹[λx ∃G (□G ≡⇩E H & x[G])]y›
727 using indist[THEN "∀E"(1), OF denotes_ex,
728 THEN "qml:2"[axiom_inst, THEN "→E"],
729 THEN "≡E"(1)] by blast
730 AOT_hence ‹∃G (□G ≡⇩E H & y[G])›
731 by (rule "β→C")
732 AOT_hence ‹∃G (□∀u ([G]u ≡ [H]u) & y[G])›
733 by (AOT_subst (reverse) ‹∀u ([G]u ≡ [H]u)› ‹G ≡⇩E H› for: G)
734 (safe intro!: "eqE"[THEN "≡Df", THEN "≡S"(1), OF "&I"] "cqt:2")
735 AOT_hence ‹∃G (∀u □([G]u ≡ [H]u) & y[G])›
736 using "Ordinary.res-var-bound-reas[BF]"
737 "Ordinary.res-var-bound-reas[CBF]"
738 "intro-elim:2"
739 by (AOT_subst ‹∀u □([G]u ≡ [H]u)› ‹□∀u ([G]u ≡ [H]u)› for: G) auto
740 } note 0 = this
741 AOT_assume ‹A!x & A!y & ∀F □([F]x ≡ [F]y)›
742 AOT_hence ‹A!x› and ‹A!y› and ‹∀F □([F]x ≡ [F]y)›
743 using "&E" by blast+
744 moreover AOT_have ‹∀F □([F]y ≡ [F]x)›
745 using calculation(3)
746 apply (safe intro!: CBF[THEN "→E"] dest!: BF[THEN "→E"])
747 using "RM:3" "cqt-basic:11" "intro-elim:3:b" by fast
748 ultimately AOT_show ‹∃G (∀u □([G]u ≡ [H]u) & x[G]) ≡
749 ∃G (∀u □([G]u ≡ [H]u) & y[G])›
750 using 0 by (auto intro!: "≡I" "→I")
751 qed
752}
753end
754end