Theory AOT_BasicLogicalObjects
1
2theory AOT_BasicLogicalObjects
3 imports AOT_PLM
4begin
5
6
7section‹Basic Logical Objects›
8
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)
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 =⇩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[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 "≡⇩d⇩fI"] "&I" "A-descriptions")
60 AOT_thus ‹∘p❙Σp›
61 by (rule "rule=E"[rotated, OF "tv-id:1"[symmetric]])
62qed
63
64
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
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
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[1]"[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[1]"[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[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": ‹∃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›
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 "≡⇩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›
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 "≡⇩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[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 ‹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[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
628end
629