# Theory AOT_BasicLogicalObjects

```1(*<*)
2theory AOT_BasicLogicalObjects
3  imports AOT_PLM
4begin
5(*>*)
6
7section‹Basic 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) ≡⇩d⇩f 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)
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)
25
26
27AOT_theorem "uni-tv": ‹❙ιx TruthValueOf(x,p)↓›
28  using "A-Exists:2" "RA" "≡E"(2) "p-has-!tv:2" by blast
29
30AOT_define TheTruthValueOf :: ‹φ ⇒ κ⇩s› (‹∘_›  100)
31  "the-tv-p": ‹∘p =⇩d⇩f ❙ιx TruthValueOf(x,p)›
32
33AOT_define PropEnc :: ‹τ ⇒ φ ⇒ φ› (infixl ‹❙Σ› 40)
34  "prop-enc": ‹x❙Σp ≡⇩d⇩f x↓ & x[λy 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 "=⇩d⇩fI"(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" 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 "≡⇩d⇩fI"] "&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) ≡⇩d⇩f ∃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 "≡⇩d⇩fE"], THEN "&E"(2)].
145
146AOT_act_theorem "T-lem:3": ‹∘p❙Σr ≡ (r ≡ p)›
147proof -
148  AOT_have θ: ‹∘p[λy 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 ‹∘p[λy r]› by (metis "≡⇩d⇩fE" "&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 ‹∘p[λy r]› using θ "≡E"(2) by blast
167    AOT_thus ‹∘p❙Σr›
168      by (metis "≡⇩d⇩fI" "&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 "≡⇩d⇩fE" "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 "≡⇩d⇩fI"] "tv-p"[THEN "≡⇩d⇩fI"]
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 "≡⇩d⇩fI"] "tv-p"[THEN "≡⇩d⇩fI"]
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": ‹⊤ =⇩d⇩f ❙ιx (A!x & ∀F (x[F] ≡ ∃p(p & F = [λy p])))›
218AOT_define TheFalse :: κ⇩s (‹⊥›)
219  "the-true:2": ‹⊥ =⇩d⇩f ❙ι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"[unvarify x⇩1 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"[unvarify x⇩1 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" "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": ‹∃x∃y(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 ‹a[λy 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 ‹¬b[λy p]›
339        proof (rule "raa-cor:2")
340          AOT_assume ‹b[λy 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 "≡⇩d⇩fE" "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 "≡⇩d⇩fE" "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 "≡⇩d⇩fE"])
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) "≡⇩d⇩fE" "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 "≡⇩d⇩fE"])
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) "≡⇩d⇩fE" "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 "≡⇩d⇩fE" "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 "≡⇩d⇩fE" "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›
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 "≡⇩d⇩fE" "&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›
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 "≡⇩d⇩fE" "&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) ≡⇩d⇩f 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 "≡⇩d⇩fI"] "exten-p"[THEN "≡⇩d⇩fI"]
545            dest!: "tv-p"[THEN "≡⇩d⇩fE"] "exten-p"[THEN "≡⇩d⇩fE"])
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" "df-rules-formulas"
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 ‹x[λy q]› using 0 "rule=E" by blast
559    AOT_hence ‹x❙Σq› by (metis "≡⇩d⇩fI" "&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 ‹x[λy q]› by (metis "≡⇩d⇩fE" "&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 "≡⇩d⇩fI" "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 ‹x[λy r]› by (metis "≡⇩d⇩fE" "&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 ‹x[λy 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 "≡⇩d⇩fI" "&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" "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"; 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```