Theory AOT_BasicLogicalObjects

1(*<*)
2theory AOT_BasicLogicalObjects
3  imports AOT_PLM
4begin
5(*>*)
6
7sectionBasic Logical Objects
8(* Note: so far only the parts required for possible world theory are implemented *)
9
10AOT_define TruthValueOf :: τ  φ  φ (TruthValueOf'(_,_'))
11  "tv-p": TruthValueOf(x,p) df A!x & F (x[F]  q((q  p) & F = y q]))
12
13AOT_theorem "p-has-!tv:1": x TruthValueOf(x,p)
14  using  "tv-p"[THEN "≡Df"]
15  by (AOT_subst TruthValueOf(x,p)
16                A!x & F (x[F]  q((q  p) & F = y q])) for: x)
17     (simp add: "A-objects"[axiom_inst])
18
19
20AOT_theorem "p-has-!tv:2": ∃!x TruthValueOf(x,p)
21  using  "tv-p"[THEN "≡Df"]
22  by (AOT_subst TruthValueOf(x,p)
23                A!x & F (x[F]  q((q  p) & F = y q])) for: x)
24     (simp add: "A-objects!")
25
26
27AOT_theorem "uni-tv": ιx TruthValueOf(x,p)
28  using "A-Exists:2" "RA[2]" "≡E"(2) "p-has-!tv:2" by blast
29
30AOT_define TheTruthValueOf :: φ  κs (_ [100] 100)
31  "the-tv-p": p =df ιx TruthValueOf(x,p)
32
33AOT_define PropEnc :: τ  φ  φ (infixl Σ 40)
34  "prop-enc": xΣp df x & xy p]
35
36AOT_theorem "tv-id:1": p = ιx (A!x & F (x[F]  q((q  p) & F = y q])))
37proof -
38  AOT_have x(TruthValueOf(x,p)   A!x & F (x[F]  q((q  p) & F = y q])))
39    by (rule RN; rule GEN; rule "tv-p"[THEN "≡Df"])
40  AOT_hence ιx TruthValueOf(x,p) = ιx (A!x & F (x[F]  q((q  p) & F = y q])))
41    using "equiv-desc-eq:3"[THEN "→E", OF "&I", OF "uni-tv"] by simp
42  thus ?thesis
43    using "=dfI"(1)[OF "the-tv-p", OF "uni-tv"] by fast
44qed
45
46AOT_theorem "tv-id:2": pΣp
47proof -
48  AOT_modally_strict {
49    AOT_have (p  p) & y p] = y p]
50      by (auto simp: "prop-prop2:2" "rule=I:1" intro!: "≡I" "→I" "&I")
51    AOT_hence q ((q  p) & y p] = y q])
52      using "∃I" by fast
53  }
54  AOT_hence 𝒜q ((q  p) & y p] = y q])
55    using "RA[2]" by blast
56  AOT_hence ιx(A!x & F (x[F]  q ((q  p) & F = y q])))y p]
57    by (safe intro!: "desc-nec-encode:1"[unvarify F, THEN "≡E"(2)] "cqt:2")
58  AOT_hence ιx(A!x & F (x[F]  q ((q  p) & F = y q])))Σp
59    by (safe intro!: "prop-enc"[THEN "dfI"] "&I" "A-descriptions")
60  AOT_thus pΣp
61    by (rule "rule=E"[rotated, OF "tv-id:1"[symmetric]])
62qed
63
64(* TODO more theorems *)
65
66AOT_theorem "TV-lem1:1":
67  p  F(q (q & F = y q])  q((q  p) & F = y q]))
68proof(safe intro!: "≡I" "→I" GEN)
69  fix F
70  AOT_assume q (q & F = y q])
71  then AOT_obtain q where q & F = y q] using "∃E"[rotated] by blast
72  moreover AOT_assume p
73  ultimately AOT_have (q  p) & F = y q]
74    by (metis "&I" "&E"(1) "&E"(2) "deduction-theorem" "≡I")
75  AOT_thus q ((q  p) & F = y q]) by (rule "∃I")
76next
77  fix F
78  AOT_assume q ((q  p) & F = y q])
79  then AOT_obtain q where (q  p) & F = y q] using "∃E"[rotated] by blast
80  moreover AOT_assume p
81  ultimately AOT_have q & F = y q]
82    by (metis "&I" "&E"(1) "&E"(2) "≡E"(2))
83  AOT_thus q (q & F = y q]) by (rule "∃I")
84next
85  AOT_assume F (q (q & F = y q])  q ((q  p) & F = y q]))
86  AOT_hence q (q & y p] = y q])  q ((q  p) & y p] = y q])
87    using "∀E"(1)[rotated, OF "prop-prop2:2"] by blast
88  moreover AOT_have q ((q  p) & y p] = y q])
89    by (rule "∃I"(2)[where β=p])
90       (simp add: "rule=I:1" "&I" "oth-class-taut:3:a" "prop-prop2:2")
91  ultimately AOT_have q (q & y p] = y q]) using "≡E"(2) by blast
92  then AOT_obtain q where q & y p] = y q] using "∃E"[rotated] by blast
93  AOT_thus p
94    using "rule=E" "&E"(1) "&E"(2) id_sym "≡E"(2) "p-identity-thm2:3" by fast
95qed
96
97AOT_theorem "TV-lem1:2":
98  ¬p  F(q (¬q & F = y q])  q((q  p) & F = y q]))
99proof(safe intro!: "≡I" "→I" GEN)
100  fix F
101  AOT_assume q (¬q & F = y q])
102  then AOT_obtain q where ¬q & F = y q] using "∃E"[rotated] by blast
103  moreover AOT_assume ¬p
104  ultimately AOT_have (q  p) & F = y q]
105    by (metis "&I" "&E"(1) "&E"(2) "deduction-theorem" "≡I" "raa-cor:3")
106  AOT_thus q ((q  p) & F = y q]) by (rule "∃I")
107next
108  fix F
109  AOT_assume q ((q  p) & F = y q])
110  then AOT_obtain q where (q  p) & F = y q] using "∃E"[rotated] by blast
111  moreover AOT_assume ¬p
112  ultimately AOT_have ¬q & F = y q]
113    by (metis "&I" "&E"(1) "&E"(2) "≡E"(1) "raa-cor:3")
114  AOT_thus q (¬q & F = y q]) by (rule "∃I")
115next
116  AOT_assume F (q (¬q & F = y q])  q ((q  p) & F = y q]))
117  AOT_hence q (¬q & y p] = y q])  q ((q  p) & y p] = y q])
118    using "∀E"(1)[rotated, OF "prop-prop2:2"] by blast
119  moreover AOT_have q ((q  p) & y p] = y q])
120    by (rule "∃I"(2)[where β=p])
121       (simp add: "rule=I:1" "&I" "oth-class-taut:3:a" "prop-prop2:2")
122  ultimately AOT_have q (¬q & y p] = y q]) using "≡E"(2) by blast
123  then AOT_obtain q where ¬q & y p] = y q] using "∃E"[rotated] by blast
124  AOT_thus ¬p
125    using "rule=E" "&E"(1) "&E"(2) id_sym "≡E"(2) "p-identity-thm2:3" by fast
126qed
127
128
129AOT_define TruthValue :: τ  φ (TruthValue'(_'))
130  "T-value": TruthValue(x) df p (TruthValueOf(x,p))
131
132(* TODO more theorems *)
133
134AOT_act_theorem "T-lem:1": TruthValueOf(p, p)
135proof -
136  AOT_have θ: p = ιx TruthValueOf(x, p)
137    using "rule-id-df:1" "the-tv-p" "uni-tv" by blast
138  moreover AOT_have p
139    using "t=t-proper:1" calculation "vdash-properties:10" by blast
140  ultimately show ?thesis by (metis "rule=E" id_sym "vdash-properties:10" "y-in:3")
141qed
142
143AOT_act_theorem "T-lem:2": F (p[F]  q((q  p) & F = y q]))
144  using "T-lem:1"[THEN "tv-p"[THEN "dfE"], THEN "&E"(2)].
145
146AOT_act_theorem "T-lem:3": pΣr  (r  p)
147proof -
148  AOT_have θ: py r]  q ((q  p) & y r] = y q])
149    using "T-lem:2"[THEN "∀E"(1), OF "prop-prop2:2"].
150  show ?thesis
151  proof(rule "≡I"; rule "→I")
152    AOT_assume pΣr
153    AOT_hence py r] by (metis "dfE" "&E"(2) "prop-enc")
154    AOT_hence q ((q  p) & y r] = y q]) using θ "≡E"(1) by blast
155    then AOT_obtain q where (q  p) & y r] = y q] using "∃E"[rotated] by blast
156    moreover AOT_have r = q using calculation
157      using "&E"(2) "≡E"(2) "p-identity-thm2:3" by blast
158    ultimately AOT_show r  p
159      by (metis "rule=E" "&E"(1) "≡E"(6) "oth-class-taut:3:a")
160  next
161    AOT_assume r  p
162    moreover AOT_have y r] = y r]
163      by (simp add: "rule=I:1" "prop-prop2:2")
164    ultimately AOT_have (r  p) & y r] = y r] using "&I" by blast
165    AOT_hence q ((q  p) & y r] = y q]) by (rule "∃I"(2)[where β=r])
166    AOT_hence py r] using θ "≡E"(2) by blast
167    AOT_thus pΣr
168      by (metis "dfI" "&I" "prop-enc" "russell-axiom[enc,1].ψ_denotes_asm")
169  qed
170qed
171
172AOT_act_theorem "T-lem:4": TruthValueOf(x, p)  x = p
173proof -
174  AOT_have x (x = ιx TruthValueOf(x, p)  z (TruthValueOf(z, p)  z = x))
175    by (simp add: "fund-cont-desc" GEN)
176  moreover AOT_have p
177    using "dfE" "tv-id:2" "&E"(1) "prop-enc" by blast
178  ultimately AOT_have
179    (p = ιx TruthValueOf(x, p))  z (TruthValueOf(z, p)  z = p)
180    using "∀E"(1) by blast
181  AOT_hence z (TruthValueOf(z, p)  z = p)
182    using "≡E"(1) "rule-id-df:1" "the-tv-p" "uni-tv" by blast
183  AOT_thus TruthValueOf(x, p)  x = p using "∀E"(2) by blast
184qed
185
186
187(* TODO more theorems *)
188
189AOT_theorem "TV-lem2:1":
190  (A!x & F (x[F]  q (q & F = y q])))  TruthValue(x)
191proof(safe intro!: "→I" "T-value"[THEN "dfI"] "tv-p"[THEN "dfI"]
192                   "∃I"(1)[rotated, OF "log-prop-prop:2"])
193  AOT_assume [A!]x & F (x[F]  q (q & F = y q]))
194  AOT_thus [A!]x & F (x[F]  q ((q  (p (p  p))) & F = y q]))
195    apply (AOT_subst q ((q  (p (p  p))) & F = y q])
196                     q (q & F = y q]) for: F :: <κ>)
197     apply (AOT_subst q  p (p p) q for: q)
198    apply (metis (no_types, lifting) "→I" "≡I" "≡E"(2) GEN)
199    by (auto simp: "cqt-further:7")
200qed
201
202AOT_theorem "TV-lem2:2":
203  (A!x & F (x[F]  q (¬q & F = y q])))  TruthValue(x)
204proof(safe intro!: "→I" "T-value"[THEN "dfI"] "tv-p"[THEN "dfI"]
205                   "∃I"(1)[rotated, OF "log-prop-prop:2"])
206  AOT_assume [A!]x & F (x[F]  q (¬q & F = y q]))
207  AOT_thus [A!]x & F (x[F]  q ((q  (p (p & ¬p))) & F = y q]))
208    apply (AOT_subst q ((q  (p (p & ¬p))) & F = y q])
209                     q (¬q & F = y q]) for: F :: <κ>)
210     apply (AOT_subst q  p (p & ¬p) ¬q for: q)
211      apply (metis (no_types, lifting)
212        "→I" "∃E" "≡E"(1) "≡I" "raa-cor:1" "raa-cor:3")
213    by (auto simp add: "cqt-further:7")
214qed
215
216AOT_define TheTrue :: κs ()
217  "the-true:1":  =df ιx (A!x & F (x[F]  p(p & F = y p])))
218AOT_define TheFalse :: κs ()
219  "the-true:2":  =df ιx (A!x & F (x[F]  p(¬p & F = y p])))
220
221
222AOT_theorem "the-true:3":   
223proof(safe intro!: "ab-obey:2"[unvarify x y, THEN "→E", rotated 2, OF "∨I"(1)]
224                   "∃I"(1)[where τ=«x q(q  q)]»] "&I" "prop-prop2:2")
225  AOT_have false_def:  = ιx (A!x & F (x[F]  p(¬p & F = y p])))
226    by (simp add: "A-descriptions" "rule-id-df:1[zero]" "the-true:2")
227  moreover AOT_show false_den: 
228    by (meson "→E" "t=t-proper:1" "A-descriptions"
229              "rule-id-df:1[zero]" "the-true:2")
230  ultimately AOT_have false_prop: 𝒜(A! & F ([F]  p(¬p & F = y p])))
231    using "nec-hintikka-scheme"[unvarify x, THEN "≡E"(1), THEN "&E"(1)] by blast
232  AOT_hence 𝒜F ([F]  p(¬p & F = y p]))
233    using "Act-Basic:2" "&E"(2) "≡E"(1) by blast
234  AOT_hence F 𝒜([F]  p(¬p & F = y p]))
235    using "≡E"(1) "logic-actual-nec:3"[axiom_inst] by blast
236  AOT_hence false_enc_cond:
237    𝒜(x q(q  q)]  p(¬p & x q(q  q)] = y p]))
238    using "∀E"(1)[rotated, OF "prop-prop2:2"] by blast
239
240  AOT_have true_def:  = ιx (A!x & F (x[F]  p(p & F = y p])))
241    by (simp add: "A-descriptions" "rule-id-df:1[zero]" "the-true:1")
242  moreover AOT_show true_den: 
243    by (meson "t=t-proper:1" "A-descriptions" "rule-id-df:1[zero]" "the-true:1" "→E")
244  ultimately AOT_have true_prop: 𝒜(A! & F ([F]  p(p & F = y p])))
245    using "nec-hintikka-scheme"[unvarify x, THEN "≡E"(1), THEN "&E"(1)]  by blast
246  AOT_hence 𝒜F ([F]  p(p & F = y p]))
247    using "Act-Basic:2" "&E"(2) "≡E"(1) by blast
248  AOT_hence F 𝒜([F]  p(p & F = y p]))
249    using "≡E"(1) "logic-actual-nec:3"[axiom_inst] by blast
250  AOT_hence 𝒜(x q(q  q)]  p(p & x q(q  q)] = y p]))
251    using "∀E"(1)[rotated, OF "prop-prop2:2"] by blast
252  moreover AOT_have 𝒜p(p & x q(q  q)] = y p])
253    by (safe intro!: "nec-imp-act"[THEN "→E"] RN "∃I"(1)[where τ="«q(q  q)»"] "&I"
254                     GEN "→I" "log-prop-prop:2" "rule=I:1" "prop-prop2:2")
255  ultimately AOT_have 𝒜(x q(q  q)])
256    using "Act-Basic:5" "≡E"(1,2) by blast
257  AOT_thus x q(q  q)]
258    using "en-eq:10[1]"[unvarify x1 F, THEN "≡E"(1)] true_den "prop-prop2:2" by blast
259
260  AOT_show ¬x q(q  q)]
261  proof(rule "raa-cor:2")
262    AOT_assume x q(q  q)]
263    AOT_hence 𝒜x q(q  q)]
264      using "en-eq:10[1]"[unvarify x1 F, THEN "≡E"(2)]
265            false_den "prop-prop2:2" by blast
266    AOT_hence 𝒜p(¬p & x q(q  q)] = y p])
267      using false_enc_cond "Act-Basic:5" "≡E"(1) by blast
268    AOT_hence p 𝒜(¬p & x q(q  q)] = y p])
269      using "Act-Basic:10" "≡E"(1) by blast
270    then AOT_obtain p where p_prop: 𝒜(¬p & x q(q  q)] = y p])
271      using "∃E"[rotated] by blast
272    AOT_hence 𝒜x q(q  q)] = y p]
273      by (metis "Act-Basic:2" "&E"(2) "≡E"(1))
274    AOT_hence x q(q  q)] = y p]
275      using "id-act:1"[unvarify α β, THEN "≡E"(2)] "prop-prop2:2" by blast
276    AOT_hence (q(q  q)) = p
277      using "p-identity-thm2:3"[unvarify p, THEN "≡E"(2)]
278            "log-prop-prop:2" by blast
279    moreover AOT_have 𝒜¬p using p_prop
280      using "Act-Basic:2" "&E"(1) "≡E"(1) by blast
281    ultimately AOT_have 𝒜¬q(q  q)
282      by (metis "Act-Sub:1" "≡E"(1,2) "raa-cor:3" "rule=E")
283    moreover AOT_have ¬𝒜¬q(q  q)
284      by (meson "Act-Sub:1" "RA[2]" "if-p-then-p" "≡E"(1) "universal-cor")
285    ultimately AOT_show 𝒜¬q(q  q) & ¬𝒜¬q(q  q)
286      using "&I" by blast
287  qed
288qed
289
290AOT_act_theorem "T-T-value:1": TruthValue()
291proof -
292  AOT_have true_def:  = ιx (A!x & F (x[F]  p(p & F = y p])))
293    by (simp add: "A-descriptions" "rule-id-df:1[zero]" "the-true:1")
294  AOT_hence true_den: 
295    using "t=t-proper:1" "vdash-properties:6" by blast
296  AOT_show TruthValue()
297    using "y-in:2"[unvarify z, OF true_den, THEN "→E", OF true_def]
298          "TV-lem2:1"[unvarify x, OF true_den, THEN "→E"] by blast
299qed
300
301AOT_act_theorem "T-T-value:2": TruthValue()
302proof -
303  AOT_have false_def:  = ιx (A!x & F (x[F]  p(¬p & F = y p])))
304    by (simp add: "A-descriptions" "rule-id-df:1[zero]" "the-true:2")
305  AOT_hence false_den: 
306    using "t=t-proper:1" "vdash-properties:6" by blast
307  AOT_show TruthValue()
308    using "y-in:2"[unvarify z, OF false_den, THEN "→E", OF false_def]
309          "TV-lem2:2"[unvarify x, OF false_den, THEN "→E"] by blast
310qed
311
312AOT_theorem "two-T": xy(TruthValue(x) & TruthValue(y) & x  y &
313                           z (TruthValue(z)  z = x  z = y))
314proof -
315  AOT_obtain a where a_prop: A!a & F (a[F]  p (p & F = y p]))
316    using "A-objects"[axiom_inst] "∃E"[rotated] by fast
317  AOT_obtain b where b_prop: A!b & F (b[F]  p (¬p & F = y p]))
318    using "A-objects"[axiom_inst] "∃E"[rotated] by fast
319  AOT_obtain p where p: p
320    by (metis "log-prop-prop:2" "raa-cor:3" "rule-ui:1" "universal-cor")
321  show ?thesis
322  proof(rule "∃I"(2)[where β=a]; rule "∃I"(2)[where β=b];
323        safe intro!: "&I" GEN "→I")
324    AOT_show TruthValue(a)
325      using "TV-lem2:1" a_prop "vdash-properties:10" by blast
326  next
327    AOT_show TruthValue(b)
328      using "TV-lem2:2" b_prop "vdash-properties:10" by blast
329  next
330    AOT_show a  b
331    proof(rule "ab-obey:2"[THEN "→E", OF "∨I"(1)])
332      AOT_show F (a[F] & ¬b[F])
333      proof(rule "∃I"(1)[where τ="«y p]»"]; rule "&I" "prop-prop2:2")
334        AOT_show ay p]
335          by(safe intro!: "∃I"(2)[where β=p] "&I" p "rule=I:1"[OF "prop-prop2:2"]
336              a_prop[THEN "&E"(2), THEN "∀E"(1), THEN "≡E"(2), OF "prop-prop2:2"])
337      next
338        AOT_show ¬by p]
339        proof (rule "raa-cor:2")
340          AOT_assume by p]
341          AOT_hence q (¬q & y p] = y q])
342            using "∀E"(1)[rotated, OF "prop-prop2:2", THEN "≡E"(1)]
343                  b_prop[THEN "&E"(2)] by fast
344          then AOT_obtain q where ¬q & y p] = y q]
345            using "∃E"[rotated] by blast
346          AOT_hence ¬p
347            by (metis "rule=E" "&E"(1) "&E"(2) "deduction-theorem" "≡I"
348                      "≡E"(2) "p-identity-thm2:3" "raa-cor:3")
349          AOT_thus p & ¬p using p "&I" by blast
350        qed
351      qed
352    qed
353  next
354    fix z
355    AOT_assume TruthValue(z)
356    AOT_hence p (TruthValueOf(z, p))
357      by (metis "dfE" "T-value")
358    then AOT_obtain p where TruthValueOf(z, p) using "∃E"[rotated] by blast
359    AOT_hence z_prop: A!z & F (z[F]  q ((q  p) & F = y q]))
360      using "dfE" "tv-p" by blast
361    {
362      AOT_assume p: p
363      AOT_have z = a
364      proof(rule "ab-obey:1"[THEN "→E", THEN "→E", OF "&I",
365                             OF z_prop[THEN "&E"(1)], OF a_prop[THEN "&E"(1)]];
366            rule GEN)
367        fix G
368        AOT_have z[G]  q ((q  p) & G = y q])
369          using z_prop[THEN "&E"(2)] "∀E"(2) by blast
370        also AOT_have q ((q  p) & G = y q])  q (q & G = y q])
371          using "TV-lem1:1"[THEN "≡E"(1), OF p, THEN "∀E"(2)[where β=G], symmetric].
372        also AOT_have   a[G]
373          using a_prop[THEN "&E"(2), THEN "∀E"(2)[where β=G], symmetric].
374        finally AOT_show z[G]  a[G].
375      qed
376      AOT_hence z = a  z = b by (rule "∨I")
377    }
378    moreover {
379      AOT_assume notp: ¬p
380      AOT_have z = b
381      proof(rule "ab-obey:1"[THEN "→E", THEN "→E", OF "&I",
382                             OF z_prop[THEN "&E"(1)], OF b_prop[THEN "&E"(1)]];
383            rule GEN)
384        fix G
385        AOT_have z[G]  q ((q  p) & G = y q])
386          using z_prop[THEN "&E"(2)] "∀E"(2) by blast
387        also AOT_have q ((q  p) & G = y q])  q (¬q & G = y q])
388          using "TV-lem1:2"[THEN "≡E"(1), OF notp, THEN "∀E"(2), symmetric].
389        also AOT_have   b[G]
390          using b_prop[THEN "&E"(2), THEN "∀E"(2), symmetric].
391        finally AOT_show z[G]  b[G].
392      qed
393      AOT_hence z = a  z = b by (rule "∨I")
394    }
395    ultimately AOT_show z = a  z = b
396      by (metis "reductio-aa:1")
397  qed
398qed
399
400AOT_act_theorem "valueof-facts:1": TruthValueOf(x, p)  (p  x = )
401proof(safe intro!: "→I" dest!: "tv-p"[THEN "dfE"])
402  AOT_assume θ: [A!]x & F (x[F]  q ((q  p) & F = y q]))
403  AOT_have a: A!
404    using "∃E" "T-T-value:1" "T-value" "&E"(1) "dfE" "tv-p" by blast
405  AOT_have true_def:  = ιx (A!x & F (x[F]  p(p & F = y p])))
406    by (simp add: "A-descriptions" "rule-id-df:1[zero]" "the-true:1")
407  AOT_hence true_den: 
408    using "t=t-proper:1" "vdash-properties:6" by blast
409  AOT_have b: F ([F]  q (q & F = y q]))
410    using "y-in:2"[unvarify z, OF true_den, THEN "→E", OF true_def] "&E" by blast
411  AOT_show p  x = 
412  proof(safe intro!: "≡I" "→I")
413    AOT_assume p
414    AOT_hence F (q (q & F = y q])  q ((q  p) & F = y q]))
415      using "TV-lem1:1"[THEN "≡E"(1)] by blast
416    AOT_hence F([F]  q ((q  p) & F = y q]))
417      using b "cqt-basic:10"[THEN "→E", OF "&I", OF b] by fast
418    AOT_hence c: F(q((q  p) & F = y q])  [F])
419      using "cqt-basic:11"[THEN "≡E"(1)] by fast
420    AOT_hence F (x[F]  [F])
421      using "cqt-basic:10"[THEN "→E", OF "&I", OF θ[THEN "&E"(2)]] by fast
422    AOT_thus x = 
423      by (rule "ab-obey:1"[unvarify y, OF true_den, THEN "→E", THEN "→E",
424                           OF "&I", OF θ[THEN "&E"(1)], OF a])
425  next
426    AOT_assume x = 
427    AOT_hence d: F ([F]  q ((q  p) & F = y q]))
428      using "rule=E" θ[THEN "&E"(2)] by fast
429    AOT_have F (q (q & F = y q])  q ((q  p) & F = y q]))
430      using "cqt-basic:10"[THEN "→E", OF "&I",
431              OF b[THEN "cqt-basic:11"[THEN "≡E"(1)]], OF d].
432    AOT_thus p using "TV-lem1:1"[THEN "≡E"(2)] by blast
433  qed
434qed
435
436AOT_act_theorem "valueof-facts:2": TruthValueOf(x, p)  (¬p  x = )
437proof(safe intro!: "→I" dest!: "tv-p"[THEN "dfE"])
438  AOT_assume θ: [A!]x & F (x[F]  q ((q  p) & F = y q]))
439  AOT_have a: A!
440    using "∃E" "T-T-value:2" "T-value" "&E"(1) "dfE" "tv-p" by blast
441  AOT_have false_def:  = ιx (A!x & F (x[F]  p(¬p & F = y p])))
442    by (simp add: "A-descriptions" "rule-id-df:1[zero]" "the-true:2")
443  AOT_hence false_den: 
444    using "t=t-proper:1" "vdash-properties:6" by blast
445  AOT_have b: F ([F]  q (¬q & F = y q]))
446    using "y-in:2"[unvarify z, OF false_den, THEN "→E", OF false_def] "&E" by blast
447  AOT_show ¬p  x = 
448  proof(safe intro!: "≡I" "→I")
449    AOT_assume ¬p
450    AOT_hence F (q (¬q & F = y q])  q ((q  p) & F = y q]))
451      using "TV-lem1:2"[THEN "≡E"(1)] by blast
452    AOT_hence F([F]  q ((q  p) & F = y q]))
453      using b "cqt-basic:10"[THEN "→E", OF "&I", OF b] by fast
454    AOT_hence c: F(q((q  p) & F = y q])  [F])
455      using "cqt-basic:11"[THEN "≡E"(1)] by fast
456    AOT_hence F (x[F]  [F])
457      using "cqt-basic:10"[THEN "→E", OF "&I", OF θ[THEN "&E"(2)]] by fast
458    AOT_thus x = 
459      by (rule "ab-obey:1"[unvarify y, OF false_den, THEN "→E", THEN "→E",
460                           OF "&I", OF θ[THEN "&E"(1)], OF a])
461  next
462    AOT_assume x = 
463    AOT_hence d: F ([F]  q ((q  p) & F = y q]))
464      using "rule=E" θ[THEN "&E"(2)] by fast
465    AOT_have F (q (¬q & F = y q])  q ((q  p) & F = y q]))
466      using "cqt-basic:10"[THEN "→E", OF "&I",
467                OF b[THEN "cqt-basic:11"[THEN "≡E"(1)]], OF d].
468    AOT_thus ¬p using "TV-lem1:2"[THEN "≡E"(2)] by blast
469  qed
470qed
471
472AOT_act_theorem "q-True:1": p  (p = )
473  apply (rule "valueof-facts:1"[unvarify x, THEN "→E", rotated, OF "T-lem:1"])
474  using "dfE" "tv-id:2" "&E"(1) "prop-enc" by blast
475
476AOT_act_theorem "q-True:2": ¬p  (p = )
477  apply (rule "valueof-facts:2"[unvarify x, THEN "→E", rotated, OF "T-lem:1"])
478  using "dfE" "tv-id:2" "&E"(1) "prop-enc" by blast
479
480AOT_act_theorem "q-True:3": p  Σp
481proof(safe intro!: "≡I" "→I")
482  AOT_assume p
483  AOT_hence p =  by (metis "≡E"(1) "q-True:1")
484  moreover AOT_have pΣp
485    by (simp add: "tv-id:2")
486  ultimately AOT_show Σp
487    using "rule=E" "T-lem:4" by fast
488next
489  AOT_have true_def:  = ιx (A!x & F (x[F]  p(p & F = y p])))
490    by (simp add: "A-descriptions" "rule-id-df:1[zero]" "the-true:1")
491  AOT_hence true_den: 
492    using "t=t-proper:1" "vdash-properties:6" by blast
493  AOT_have b: F ([F]  q (q & F = y q]))
494    using "y-in:2"[unvarify z, OF true_den, THEN "→E", OF true_def] "&E" by blast
495
496  AOT_assume Σp
497  AOT_hence y p] by (metis "dfE" "&E"(2) "prop-enc")
498  AOT_hence q (q & y p] = y q])
499    using b[THEN "∀E"(1), OF "prop-prop2:2", THEN "≡E"(1)] by blast
500  then AOT_obtain q where q & y p] = y q] using "∃E"[rotated] by blast
501  AOT_thus p
502    using "rule=E" "&E"(1) "&E"(2) id_sym "≡E"(2) "p-identity-thm2:3" by fast
503qed
504
505
506AOT_act_theorem "q-True:5": ¬p  Σp
507proof(safe intro!: "≡I" "→I")
508  AOT_assume ¬p
509  AOT_hence p =  by (metis "≡E"(1) "q-True:2")
510  moreover AOT_have pΣp
511    by (simp add: "tv-id:2")
512  ultimately AOT_show Σp
513    using "rule=E" "T-lem:4" by fast
514next
515  AOT_have false_def:  = ιx (A!x & F (x[F]  p(¬p & F = y p])))
516    by (simp add: "A-descriptions" "rule-id-df:1[zero]" "the-true:2")
517  AOT_hence false_den: 
518    using "t=t-proper:1" "vdash-properties:6" by blast
519  AOT_have b: F ([F]  q (¬q & F = y q]))
520    using "y-in:2"[unvarify z, OF false_den, THEN "→E", OF false_def] "&E" by blast
521
522  AOT_assume Σp
523  AOT_hence y p] by (metis "dfE" "&E"(2) "prop-enc")
524  AOT_hence q (¬q & y p] = y q])
525    using b[THEN "∀E"(1), OF "prop-prop2:2", THEN "≡E"(1)] by blast
526  then AOT_obtain q where ¬q & y p] = y q] using "∃E"[rotated] by blast
527  AOT_thus ¬p
528    using "rule=E" "&E"(1) "&E"(2) id_sym "≡E"(2) "p-identity-thm2:3" by fast
529qed
530
531AOT_act_theorem "q-True:4": p  ¬(Σp)
532  using "q-True:5"
533  by (metis "deduction-theorem" "≡I" "≡E"(2) "≡E"(4) "raa-cor:3")
534
535AOT_act_theorem "q-True:6": ¬p  ¬(Σp)
536  using "≡E"(1) "oth-class-taut:4:b" "q-True:3" by blast
537
538AOT_define ExtensionOf :: τ  φ  φ (ExtensionOf'(_,_'))
539  "exten-p": ExtensionOf(x,p) df A!x &
540                                   F (x[F]  Propositional([F])) &
541                                   q ((xΣq)  (q  p))
542
543AOT_theorem "extof-e": ExtensionOf(x, p)  TruthValueOf(x, p)
544proof (safe intro!: "≡I" "→I" "tv-p"[THEN "dfI"] "exten-p"[THEN "dfI"]
545            dest!: "tv-p"[THEN "dfE"] "exten-p"[THEN "dfE"])
546  AOT_assume 1: [A!]x & F (x[F]  Propositional([F])) & q (x Σ q  (q  p))
547  AOT_hence θ: [A!]x & F (x[F]  q(F = y q])) & q (x Σ q  (q  p))
548    by (AOT_subst q(F = y q]) Propositional([F]) for: F :: <κ>)
549       (auto simp add: "df-rules-formulas[3]" "df-rules-formulas[4]"
550                       "≡I" "prop-prop1")
551  AOT_show [A!]x & F (x[F]  q ((q  p) & F = y q]))
552  proof(safe intro!: "&I" GEN 1[THEN "&E"(1), THEN "&E"(1)] "≡I" "→I")
553    fix F
554    AOT_assume 0: x[F]
555    AOT_hence q (F = y q])
556      using θ[THEN "&E"(1), THEN "&E"(2)] "∀E"(2) "→E" by blast
557    then AOT_obtain q where q_prop: F = y q] using "∃E"[rotated] by blast
558    AOT_hence xy q] using 0 "rule=E" by blast
559    AOT_hence xΣq by (metis "dfI" "&I" "ex:1:a" "prop-enc" "rule-ui:3")
560    AOT_hence q  p using θ[THEN "&E"(2)] "∀E"(2) "≡E"(1) by blast
561    AOT_hence (q  p) & F = y q] using q_prop "&I" by blast
562    AOT_thus q ((q  p) & F = y q]) by (rule "∃I")
563  next
564    fix F
565    AOT_assume q ((q  p) & F = y q])
566    then AOT_obtain q where q_prop: (q  p) & F = y q]
567      using "∃E"[rotated] by blast
568    AOT_hence xΣq using θ[THEN "&E"(2)] "∀E"(2) "&E" "≡E"(2) by blast
569    AOT_hence xy q] by (metis "dfE" "&E"(2) "prop-enc")
570    AOT_thus x[F] using q_prop[THEN "&E"(2), symmetric] "rule=E" by blast
571  qed
572next
573  AOT_assume 0: [A!]x & F (x[F]  q ((q  p) & F = y q]))
574  AOT_show [A!]x & F (x[F]  Propositional([F])) & q (x Σ q  (q  p))
575  proof(safe intro!: "&I" 0[THEN "&E"(1)] GEN "→I")
576    fix F
577    AOT_assume x[F]
578    AOT_hence q ((q  p) & F = y q])
579      using 0[THEN "&E"(2)] "∀E"(2) "≡E"(1) by blast
580    then AOT_obtain q where (q  p) & F = y q]
581      using "∃E"[rotated] by blast
582    AOT_hence F = y q] using "&E"(2) by blast
583    AOT_hence q F = y q] by (rule "∃I")
584    AOT_thus Propositional([F]) by (metis "dfI" "prop-prop1")
585  next
586    AOT_show xΣr  (r  p) for r
587    proof(rule "≡I"; rule "→I")
588      AOT_assume xΣr
589      AOT_hence xy r] by (metis "dfE" "&E"(2) "prop-enc")
590      AOT_hence q ((q  p) & y r] = y q]) 
591        using 0[THEN "&E"(2), THEN "∀E"(1), OF "prop-prop2:2", THEN "≡E"(1)] by blast
592      then AOT_obtain q where (q  p) & y r] = y q]
593        using "∃E"[rotated] by blast
594      AOT_thus r  p
595        by (metis "rule=E" "&E"(1,2) id_sym "≡E"(2) "Commutativity of ≡"
596                  "p-identity-thm2:3")
597    next
598      AOT_assume r  p
599      AOT_hence (r  p) & y r] = y r]
600        by (metis "rule=I:1" "≡S"(1) "≡E"(2) "Commutativity of &" "prop-prop2:2")
601      AOT_hence q ((q  p) & y r] = y q]) by (rule "∃I")
602      AOT_hence xy r]
603        using 0[THEN "&E"(2), THEN "∀E"(1), OF "prop-prop2:2", THEN "≡E"(2)] by blast
604      AOT_thus xΣr by (metis "dfI" "&I" "ex:1:a" "prop-enc" "rule-ui:3")
605    qed
606  qed
607qed
608
609AOT_theorem "ext-p-tv:1": ∃!x ExtensionOf(x, p)
610  by (AOT_subst ExtensionOf(x, p) TruthValueOf(x, p) for: x)
611     (auto simp: "extof-e" "p-has-!tv:2")
612
613AOT_theorem "ext-p-tv:2": ιx(ExtensionOf(x, p))
614  using "A-Exists:2" "RA[2]" "ext-p-tv:1" "≡E"(2) by blast
615
616AOT_theorem "ext-p-tv:3": ιx(ExtensionOf(x, p)) = p
617proof -
618  AOT_have 0: 𝒜x(ExtensionOf(x, p)  TruthValueOf(x,p))
619    by (rule "RA[2]"; rule GEN; rule "extof-e")
620  AOT_have 1: p = ιx TruthValueOf(x,p)
621    using "rule-id-df:1" "the-tv-p" "uni-tv" by blast
622  show ?thesis
623    apply (rule "equiv-desc-eq:1"[THEN "→E", OF 0, THEN "∀E"(1)[where τ=«p»],
624                                  THEN "≡E"(2), symmetric])
625    using "1" "t=t-proper:1" "vdash-properties:10" apply blast
626    by (fact 1)
627qed
628(*<*)end(*>*)
629