Theory AOT_BasicLogicalObjects
theory AOT_BasicLogicalObjects
imports AOT_PLM
begin
section‹Basic Logical Objects›
AOT_define TruthValueOf :: ‹τ ⇒ φ ⇒ φ› (‹TruthValueOf'(_,_')›)
"tv-p": ‹TruthValueOf(x,p) ≡⇩d⇩f A!x & ∀F (x[F] ≡ ∃q((q ≡ p) & F = [λy q]))›
AOT_theorem "p-has-!tv:1": ‹∃x TruthValueOf(x,p)›
using "tv-p"[THEN "≡Df"]
by (AOT_subst ‹TruthValueOf(x,p)›
‹A!x & ∀F (x[F] ≡ ∃q((q ≡ p) & F = [λy q]))› for: x)
(simp add: "A-objects"[axiom_inst])
AOT_theorem "p-has-!tv:2": ‹∃!x TruthValueOf(x,p)›
using "tv-p"[THEN "≡Df"]
by (AOT_subst ‹TruthValueOf(x,p)›
‹A!x & ∀F (x[F] ≡ ∃q((q ≡ p) & F = [λy q]))› for: x)
(simp add: "A-objects!")
AOT_theorem "uni-tv": ‹❙ιx TruthValueOf(x,p)↓›
using "A-Exists:2" "RA[2]" "≡E"(2) "p-has-!tv:2" by blast
AOT_define TheTruthValueOf :: ‹φ ⇒ κ⇩s› (‹∘_› [100] 100)
"the-tv-p": ‹∘p =⇩d⇩f ❙ιx TruthValueOf(x,p)›
AOT_define PropEnc :: ‹τ ⇒ φ ⇒ φ› (infixl ‹❙Σ› 40)
"prop-enc": ‹x❙Σp ≡⇩d⇩f x↓ & x[λy p]›
AOT_theorem "tv-id:1": ‹∘p = ❙ιx (A!x & ∀F (x[F] ≡ ∃q((q ≡ p) & F = [λy q])))›
proof -
AOT_have ‹□∀x(TruthValueOf(x,p) ≡ A!x & ∀F (x[F] ≡ ∃q((q ≡ p) & F = [λy q])))›
by (rule RN; rule GEN; rule "tv-p"[THEN "≡Df"])
AOT_hence ‹❙ιx TruthValueOf(x,p) = ❙ιx (A!x & ∀F (x[F] ≡ ∃q((q ≡ p) & F = [λy q])))›
using "equiv-desc-eq:3"[THEN "→E", OF "&I", OF "uni-tv"] by simp
thus ?thesis
using "=⇩d⇩fI"(1)[OF "the-tv-p", OF "uni-tv"] by fast
qed
AOT_theorem "tv-id:2": ‹∘p❙Σp›
proof -
AOT_modally_strict {
AOT_have ‹(p ≡ p) & [λy p] = [λy p]›
by (auto simp: "prop-prop2:2" "rule=I:1" intro!: "≡I" "→I" "&I")
AOT_hence ‹∃q ((q ≡ p) & [λy p] = [λy q])›
using "∃I" by fast
}
AOT_hence ‹❙𝒜∃q ((q ≡ p) & [λy p] = [λy q])›
using "RA[2]" by blast
AOT_hence ‹❙ιx(A!x & ∀F (x[F] ≡ ∃q ((q ≡ p) & F = [λy q])))[λy p]›
by (safe intro!: "desc-nec-encode:1"[unvarify F, THEN "≡E"(2)] "cqt:2")
AOT_hence ‹❙ιx(A!x & ∀F (x[F] ≡ ∃q ((q ≡ p) & F = [λy q])))❙Σp›
by (safe intro!: "prop-enc"[THEN "≡⇩d⇩fI"] "&I" "A-descriptions")
AOT_thus ‹∘p❙Σp›
by (rule "rule=E"[rotated, OF "tv-id:1"[symmetric]])
qed
AOT_theorem "TV-lem1:1":
‹p ≡ ∀F(∃q (q & F = [λy q]) ≡ ∃q((q ≡ p) & F = [λy q]))›
proof(safe intro!: "≡I" "→I" GEN)
fix F
AOT_assume ‹∃q (q & F = [λy q])›
then AOT_obtain q where ‹q & F = [λy q]› using "∃E"[rotated] by blast
moreover AOT_assume p
ultimately AOT_have ‹(q ≡ p) & F = [λy q]›
by (metis "&I" "&E"(1) "&E"(2) "deduction-theorem" "≡I")
AOT_thus ‹∃q ((q ≡ p) & F = [λy q])› by (rule "∃I")
next
fix F
AOT_assume ‹∃q ((q ≡ p) & F = [λy q])›
then AOT_obtain q where ‹(q ≡ p) & F = [λy q]› using "∃E"[rotated] by blast
moreover AOT_assume p
ultimately AOT_have ‹q & F = [λy q]›
by (metis "&I" "&E"(1) "&E"(2) "≡E"(2))
AOT_thus ‹∃q (q & F = [λy q])› by (rule "∃I")
next
AOT_assume ‹∀F (∃q (q & F = [λy q]) ≡ ∃q ((q ≡ p) & F = [λy q]))›
AOT_hence ‹∃q (q & [λy p] = [λy q]) ≡ ∃q ((q ≡ p) & [λy p] = [λy q])›
using "∀E"(1)[rotated, OF "prop-prop2:2"] by blast
moreover AOT_have ‹∃q ((q ≡ p) & [λy p] = [λy q])›
by (rule "∃I"(2)[where β=p])
(simp add: "rule=I:1" "&I" "oth-class-taut:3:a" "prop-prop2:2")
ultimately AOT_have ‹∃q (q & [λy p] = [λy q])› using "≡E"(2) by blast
then AOT_obtain q where ‹q & [λy p] = [λy q]› using "∃E"[rotated] by blast
AOT_thus ‹p›
using "rule=E" "&E"(1) "&E"(2) id_sym "≡E"(2) "p-identity-thm2:3" by fast
qed
AOT_theorem "TV-lem1:2":
‹¬p ≡ ∀F(∃q (¬q & F = [λy q]) ≡ ∃q((q ≡ p) & F = [λy q]))›
proof(safe intro!: "≡I" "→I" GEN)
fix F
AOT_assume ‹∃q (¬q & F = [λy q])›
then AOT_obtain q where ‹¬q & F = [λy q]› using "∃E"[rotated] by blast
moreover AOT_assume ‹¬p›
ultimately AOT_have ‹(q ≡ p) & F = [λy q]›
by (metis "&I" "&E"(1) "&E"(2) "deduction-theorem" "≡I" "raa-cor:3")
AOT_thus ‹∃q ((q ≡ p) & F = [λy q])› by (rule "∃I")
next
fix F
AOT_assume ‹∃q ((q ≡ p) & F = [λy q])›
then AOT_obtain q where ‹(q ≡ p) & F = [λy q]› using "∃E"[rotated] by blast
moreover AOT_assume ‹¬p›
ultimately AOT_have ‹¬q & F = [λy q]›
by (metis "&I" "&E"(1) "&E"(2) "≡E"(1) "raa-cor:3")
AOT_thus ‹∃q (¬q & F = [λy q])› by (rule "∃I")
next
AOT_assume ‹∀F (∃q (¬q & F = [λy q]) ≡ ∃q ((q ≡ p) & F = [λy q]))›
AOT_hence ‹∃q (¬q & [λy p] = [λy q]) ≡ ∃q ((q ≡ p) & [λy p] = [λy q])›
using "∀E"(1)[rotated, OF "prop-prop2:2"] by blast
moreover AOT_have ‹∃q ((q ≡ p) & [λy p] = [λy q])›
by (rule "∃I"(2)[where β=p])
(simp add: "rule=I:1" "&I" "oth-class-taut:3:a" "prop-prop2:2")
ultimately AOT_have ‹∃q (¬q & [λy p] = [λy q])› using "≡E"(2) by blast
then AOT_obtain q where ‹¬q & [λy p] = [λy q]› using "∃E"[rotated] by blast
AOT_thus ‹¬p›
using "rule=E" "&E"(1) "&E"(2) id_sym "≡E"(2) "p-identity-thm2:3" by fast
qed
AOT_define TruthValue :: ‹τ ⇒ φ› (‹TruthValue'(_')›)
"T-value": ‹TruthValue(x) ≡⇩d⇩f ∃p (TruthValueOf(x,p))›
AOT_act_theorem "T-lem:1": ‹TruthValueOf(∘p, p)›
proof -
AOT_have θ: ‹∘p = ❙ιx TruthValueOf(x, p)›
using "rule-id-df:1" "the-tv-p" "uni-tv" by blast
moreover AOT_have ‹∘p↓›
using "t=t-proper:1" calculation "vdash-properties:10" by blast
ultimately show ?thesis by (metis "rule=E" id_sym "vdash-properties:10" "y-in:3")
qed
AOT_act_theorem "T-lem:2": ‹∀F (∘p[F] ≡ ∃q((q ≡ p) & F = [λy q]))›
using "T-lem:1"[THEN "tv-p"[THEN "≡⇩d⇩fE"], THEN "&E"(2)].
AOT_act_theorem "T-lem:3": ‹∘p❙Σr ≡ (r ≡ p)›
proof -
AOT_have θ: ‹∘p[λy r] ≡ ∃q ((q ≡ p) & [λy r] = [λy q])›
using "T-lem:2"[THEN "∀E"(1), OF "prop-prop2:2"].
show ?thesis
proof(rule "≡I"; rule "→I")
AOT_assume ‹∘p❙Σr›
AOT_hence ‹∘p[λy r]› by (metis "≡⇩d⇩fE" "&E"(2) "prop-enc")
AOT_hence ‹∃q ((q ≡ p) & [λy r] = [λy q])› using θ "≡E"(1) by blast
then AOT_obtain q where ‹(q ≡ p) & [λy r] = [λy q]› using "∃E"[rotated] by blast
moreover AOT_have ‹r = q› using calculation
using "&E"(2) "≡E"(2) "p-identity-thm2:3" by blast
ultimately AOT_show ‹r ≡ p›
by (metis "rule=E" "&E"(1) "≡E"(6) "oth-class-taut:3:a")
next
AOT_assume ‹r ≡ p›
moreover AOT_have ‹[λy r] = [λy r]›
by (simp add: "rule=I:1" "prop-prop2:2")
ultimately AOT_have ‹(r ≡ p) & [λy r] = [λy r]› using "&I" by blast
AOT_hence ‹∃q ((q ≡ p) & [λy r] = [λy q])› by (rule "∃I"(2)[where β=r])
AOT_hence ‹∘p[λy r]› using θ "≡E"(2) by blast
AOT_thus ‹∘p❙Σr›
by (metis "≡⇩d⇩fI" "&I" "prop-enc" "russell-axiom[enc,1].ψ_denotes_asm")
qed
qed
AOT_act_theorem "T-lem:4": ‹TruthValueOf(x, p) ≡ x = ∘p›
proof -
AOT_have ‹∀x (x = ❙ιx TruthValueOf(x, p) ≡ ∀z (TruthValueOf(z, p) ≡ z = x))›
by (simp add: "fund-cont-desc" GEN)
moreover AOT_have ‹∘p↓›
using "≡⇩d⇩fE" "tv-id:2" "&E"(1) "prop-enc" by blast
ultimately AOT_have
‹(∘p = ❙ιx TruthValueOf(x, p)) ≡ ∀z (TruthValueOf(z, p) ≡ z = ∘p)›
using "∀E"(1) by blast
AOT_hence ‹∀z (TruthValueOf(z, p) ≡ z = ∘p)›
using "≡E"(1) "rule-id-df:1" "the-tv-p" "uni-tv" by blast
AOT_thus ‹TruthValueOf(x, p) ≡ x = ∘p› using "∀E"(2) by blast
qed
AOT_theorem "TV-lem2:1":
‹(A!x & ∀F (x[F] ≡ ∃q (q & F = [λy q]))) → TruthValue(x)›
proof(safe intro!: "→I" "T-value"[THEN "≡⇩d⇩fI"] "tv-p"[THEN "≡⇩d⇩fI"]
"∃I"(1)[rotated, OF "log-prop-prop:2"])
AOT_assume ‹[A!]x & ∀F (x[F] ≡ ∃q (q & F = [λy q]))›
AOT_thus ‹[A!]x & ∀F (x[F] ≡ ∃q ((q ≡ (∀p (p → p))) & F = [λy q]))›
apply (AOT_subst ‹∃q ((q ≡ (∀p (p → p))) & F = [λy q])›
‹∃q (q & F = [λy q])› for: F :: ‹<κ>›)
apply (AOT_subst ‹q ≡ ∀p (p →p)› ‹q› for: q)
apply (metis (no_types, lifting) "→I" "≡I" "≡E"(2) GEN)
by (auto simp: "cqt-further:7")
qed
AOT_theorem "TV-lem2:2":
‹(A!x & ∀F (x[F] ≡ ∃q (¬q & F = [λy q]))) → TruthValue(x)›
proof(safe intro!: "→I" "T-value"[THEN "≡⇩d⇩fI"] "tv-p"[THEN "≡⇩d⇩fI"]
"∃I"(1)[rotated, OF "log-prop-prop:2"])
AOT_assume ‹[A!]x & ∀F (x[F] ≡ ∃q (¬q & F = [λy q]))›
AOT_thus ‹[A!]x & ∀F (x[F] ≡ ∃q ((q ≡ (∃p (p & ¬p))) & F = [λy q]))›
apply (AOT_subst ‹∃q ((q ≡ (∃p (p & ¬p))) & F = [λy q])›
‹∃q (¬q & F = [λy q])› for: F :: ‹<κ>›)
apply (AOT_subst ‹q ≡ ∃p (p & ¬p)› ‹¬q› for: q)
apply (metis (no_types, lifting)
"→I" "∃E" "≡E"(1) "≡I" "raa-cor:1" "raa-cor:3")
by (auto simp add: "cqt-further:7")
qed
AOT_define TheTrue :: κ⇩s (‹⊤›)
"the-true:1": ‹⊤ =⇩d⇩f ❙ιx (A!x & ∀F (x[F] ≡ ∃p(p & F = [λy p])))›
AOT_define TheFalse :: κ⇩s (‹⊥›)
"the-true:2": ‹⊥ =⇩d⇩f ❙ιx (A!x & ∀F (x[F] ≡ ∃p(¬p & F = [λy p])))›
AOT_theorem "the-true:3": ‹⊤ ≠ ⊥›
proof(safe intro!: "ab-obey:2"[unvarify x y, THEN "→E", rotated 2, OF "∨I"(1)]
"∃I"(1)[where τ=‹«[λx ∀q(q → q)]»›] "&I" "prop-prop2:2")
AOT_have false_def: ‹⊥ = ❙ιx (A!x & ∀F (x[F] ≡ ∃p(¬p & F = [λy p])))›
by (simp add: "A-descriptions" "rule-id-df:1[zero]" "the-true:2")
moreover AOT_show false_den: ‹⊥↓›
by (meson "→E" "t=t-proper:1" "A-descriptions"
"rule-id-df:1[zero]" "the-true:2")
ultimately AOT_have false_prop: ‹❙𝒜(A!⊥ & ∀F (⊥[F] ≡ ∃p(¬p & F = [λy p])))›
using "nec-hintikka-scheme"[unvarify x, THEN "≡E"(1), THEN "&E"(1)] by blast
AOT_hence ‹❙𝒜∀F (⊥[F] ≡ ∃p(¬p & F = [λy p]))›
using "Act-Basic:2" "&E"(2) "≡E"(1) by blast
AOT_hence ‹∀F ❙𝒜(⊥[F] ≡ ∃p(¬p & F = [λy p]))›
using "≡E"(1) "logic-actual-nec:3"[axiom_inst] by blast
AOT_hence false_enc_cond:
‹❙𝒜(⊥[λx ∀q(q → q)] ≡ ∃p(¬p & [λx ∀q(q → q)] = [λy p]))›
using "∀E"(1)[rotated, OF "prop-prop2:2"] by blast
AOT_have true_def: ‹⊤ = ❙ιx (A!x & ∀F (x[F] ≡ ∃p(p & F = [λy p])))›
by (simp add: "A-descriptions" "rule-id-df:1[zero]" "the-true:1")
moreover AOT_show true_den: ‹⊤↓›
by (meson "t=t-proper:1" "A-descriptions" "rule-id-df:1[zero]" "the-true:1" "→E")
ultimately AOT_have true_prop: ‹❙𝒜(A!⊤ & ∀F (⊤[F] ≡ ∃p(p & F = [λy p])))›
using "nec-hintikka-scheme"[unvarify x, THEN "≡E"(1), THEN "&E"(1)] by blast
AOT_hence ‹❙𝒜∀F (⊤[F] ≡ ∃p(p & F = [λy p]))›
using "Act-Basic:2" "&E"(2) "≡E"(1) by blast
AOT_hence ‹∀F ❙𝒜(⊤[F] ≡ ∃p(p & F = [λy p]))›
using "≡E"(1) "logic-actual-nec:3"[axiom_inst] by blast
AOT_hence ‹❙𝒜(⊤[λx ∀q(q → q)] ≡ ∃p(p & [λx ∀q(q → q)] = [λy p]))›
using "∀E"(1)[rotated, OF "prop-prop2:2"] by blast
moreover AOT_have ‹❙𝒜∃p(p & [λx ∀q(q → q)] = [λy p])›
by (safe intro!: "nec-imp-act"[THEN "→E"] RN "∃I"(1)[where τ="«∀q(q → q)»"] "&I"
GEN "→I" "log-prop-prop:2" "rule=I:1" "prop-prop2:2")
ultimately AOT_have ‹❙𝒜(⊤[λx ∀q(q → q)])›
using "Act-Basic:5" "≡E"(1,2) by blast
AOT_thus ‹⊤[λx ∀q(q → q)]›
using "en-eq:10[1]"[unvarify x⇩1 F, THEN "≡E"(1)] true_den "prop-prop2:2" by blast
AOT_show ‹¬⊥[λx ∀q(q → q)]›
proof(rule "raa-cor:2")
AOT_assume ‹⊥[λx ∀q(q → q)]›
AOT_hence ‹❙𝒜⊥[λx ∀q(q → q)]›
using "en-eq:10[1]"[unvarify x⇩1 F, THEN "≡E"(2)]
false_den "prop-prop2:2" by blast
AOT_hence ‹❙𝒜∃p(¬p & [λx ∀q(q → q)] = [λy p])›
using false_enc_cond "Act-Basic:5" "≡E"(1) by blast
AOT_hence ‹∃p ❙𝒜(¬p & [λx ∀q(q → q)] = [λy p])›
using "Act-Basic:10" "≡E"(1) by blast
then AOT_obtain p where p_prop: ‹❙𝒜(¬p & [λx ∀q(q → q)] = [λy p])›
using "∃E"[rotated] by blast
AOT_hence ‹❙𝒜[λx ∀q(q → q)] = [λy p]›
by (metis "Act-Basic:2" "&E"(2) "≡E"(1))
AOT_hence ‹[λx ∀q(q → q)] = [λy p]›
using "id-act:1"[unvarify α β, THEN "≡E"(2)] "prop-prop2:2" by blast
AOT_hence ‹(∀q(q → q)) = p›
using "p-identity-thm2:3"[unvarify p, THEN "≡E"(2)]
"log-prop-prop:2" by blast
moreover AOT_have ‹❙𝒜¬p› using p_prop
using "Act-Basic:2" "&E"(1) "≡E"(1) by blast
ultimately AOT_have ‹❙𝒜¬∀q(q → q)›
by (metis "Act-Sub:1" "≡E"(1,2) "raa-cor:3" "rule=E")
moreover AOT_have ‹¬❙𝒜¬∀q(q → q)›
by (meson "Act-Sub:1" "RA[2]" "if-p-then-p" "≡E"(1) "universal-cor")
ultimately AOT_show ‹❙𝒜¬∀q(q → q) & ¬❙𝒜¬∀q(q → q)›
using "&I" by blast
qed
qed
AOT_act_theorem "T-T-value:1": ‹TruthValue(⊤)›
proof -
AOT_have true_def: ‹⊤ = ❙ιx (A!x & ∀F (x[F] ≡ ∃p(p & F = [λy p])))›
by (simp add: "A-descriptions" "rule-id-df:1[zero]" "the-true:1")
AOT_hence true_den: ‹⊤↓›
using "t=t-proper:1" "vdash-properties:6" by blast
AOT_show ‹TruthValue(⊤)›
using "y-in:2"[unvarify z, OF true_den, THEN "→E", OF true_def]
"TV-lem2:1"[unvarify x, OF true_den, THEN "→E"] by blast
qed
AOT_act_theorem "T-T-value:2": ‹TruthValue(⊥)›
proof -
AOT_have false_def: ‹⊥ = ❙ιx (A!x & ∀F (x[F] ≡ ∃p(¬p & F = [λy p])))›
by (simp add: "A-descriptions" "rule-id-df:1[zero]" "the-true:2")
AOT_hence false_den: ‹⊥↓›
using "t=t-proper:1" "vdash-properties:6" by blast
AOT_show ‹TruthValue(⊥)›
using "y-in:2"[unvarify z, OF false_den, THEN "→E", OF false_def]
"TV-lem2:2"[unvarify x, OF false_den, THEN "→E"] by blast
qed
AOT_theorem "two-T": ‹∃x∃y(TruthValue(x) & TruthValue(y) & x ≠ y &
∀z (TruthValue(z) → z = x ∨ z = y))›
proof -
AOT_obtain a where a_prop: ‹A!a & ∀F (a[F] ≡ ∃p (p & F = [λy p]))›
using "A-objects"[axiom_inst] "∃E"[rotated] by fast
AOT_obtain b where b_prop: ‹A!b & ∀F (b[F] ≡ ∃p (¬p & F = [λy p]))›
using "A-objects"[axiom_inst] "∃E"[rotated] by fast
AOT_obtain p where p: p
by (metis "log-prop-prop:2" "raa-cor:3" "rule-ui:1" "universal-cor")
show ?thesis
proof(rule "∃I"(2)[where β=a]; rule "∃I"(2)[where β=b];
safe intro!: "&I" GEN "→I")
AOT_show ‹TruthValue(a)›
using "TV-lem2:1" a_prop "vdash-properties:10" by blast
next
AOT_show ‹TruthValue(b)›
using "TV-lem2:2" b_prop "vdash-properties:10" by blast
next
AOT_show ‹a ≠ b›
proof(rule "ab-obey:2"[THEN "→E", OF "∨I"(1)])
AOT_show ‹∃F (a[F] & ¬b[F])›
proof(rule "∃I"(1)[where τ="«[λy p]»"]; rule "&I" "prop-prop2:2")
AOT_show ‹a[λy p]›
by(safe intro!: "∃I"(2)[where β=p] "&I" p "rule=I:1"[OF "prop-prop2:2"]
a_prop[THEN "&E"(2), THEN "∀E"(1), THEN "≡E"(2), OF "prop-prop2:2"])
next
AOT_show ‹¬b[λy p]›
proof (rule "raa-cor:2")
AOT_assume ‹b[λy p]›
AOT_hence ‹∃q (¬q & [λy p] = [λy q])›
using "∀E"(1)[rotated, OF "prop-prop2:2", THEN "≡E"(1)]
b_prop[THEN "&E"(2)] by fast
then AOT_obtain q where ‹¬q & [λy p] = [λy q]›
using "∃E"[rotated] by blast
AOT_hence ‹¬p›
by (metis "rule=E" "&E"(1) "&E"(2) "deduction-theorem" "≡I"
"≡E"(2) "p-identity-thm2:3" "raa-cor:3")
AOT_thus ‹p & ¬p› using p "&I" by blast
qed
qed
qed
next
fix z
AOT_assume ‹TruthValue(z)›
AOT_hence ‹∃p (TruthValueOf(z, p))›
by (metis "≡⇩d⇩fE" "T-value")
then AOT_obtain p where ‹TruthValueOf(z, p)› using "∃E"[rotated] by blast
AOT_hence z_prop: ‹A!z & ∀F (z[F] ≡ ∃q ((q ≡ p) & F = [λy q]))›
using "≡⇩d⇩fE" "tv-p" by blast
{
AOT_assume p: ‹p›
AOT_have ‹z = a›
proof(rule "ab-obey:1"[THEN "→E", THEN "→E", OF "&I",
OF z_prop[THEN "&E"(1)], OF a_prop[THEN "&E"(1)]];
rule GEN)
fix G
AOT_have ‹z[G] ≡ ∃q ((q ≡ p) & G = [λy q])›
using z_prop[THEN "&E"(2)] "∀E"(2) by blast
also AOT_have ‹∃q ((q ≡ p) & G = [λy q]) ≡ ∃q (q & G = [λy q])›
using "TV-lem1:1"[THEN "≡E"(1), OF p, THEN "∀E"(2)[where β=G], symmetric].
also AOT_have ‹… ≡ a[G]›
using a_prop[THEN "&E"(2), THEN "∀E"(2)[where β=G], symmetric].
finally AOT_show ‹z[G] ≡ a[G]›.
qed
AOT_hence ‹z = a ∨ z = b› by (rule "∨I")
}
moreover {
AOT_assume notp: ‹¬p›
AOT_have ‹z = b›
proof(rule "ab-obey:1"[THEN "→E", THEN "→E", OF "&I",
OF z_prop[THEN "&E"(1)], OF b_prop[THEN "&E"(1)]];
rule GEN)
fix G
AOT_have ‹z[G] ≡ ∃q ((q ≡ p) & G = [λy q])›
using z_prop[THEN "&E"(2)] "∀E"(2) by blast
also AOT_have ‹∃q ((q ≡ p) & G = [λy q]) ≡ ∃q (¬q & G = [λy q])›
using "TV-lem1:2"[THEN "≡E"(1), OF notp, THEN "∀E"(2), symmetric].
also AOT_have ‹… ≡ b[G]›
using b_prop[THEN "&E"(2), THEN "∀E"(2), symmetric].
finally AOT_show ‹z[G] ≡ b[G]›.
qed
AOT_hence ‹z = a ∨ z = b› by (rule "∨I")
}
ultimately AOT_show ‹z = a ∨ z = b›
by (metis "reductio-aa:1")
qed
qed
AOT_act_theorem "valueof-facts:1": ‹TruthValueOf(x, p) → (p ≡ x = ⊤)›
proof(safe intro!: "→I" dest!: "tv-p"[THEN "≡⇩d⇩fE"])
AOT_assume θ: ‹[A!]x & ∀F (x[F] ≡ ∃q ((q ≡ p) & F = [λy q]))›
AOT_have a: ‹A!⊤›
using "∃E" "T-T-value:1" "T-value" "&E"(1) "≡⇩d⇩fE" "tv-p" by blast
AOT_have true_def: ‹⊤ = ❙ιx (A!x & ∀F (x[F] ≡ ∃p(p & F = [λy p])))›
by (simp add: "A-descriptions" "rule-id-df:1[zero]" "the-true:1")
AOT_hence true_den: ‹⊤↓›
using "t=t-proper:1" "vdash-properties:6" by blast
AOT_have b: ‹∀F (⊤[F] ≡ ∃q (q & F = [λy q]))›
using "y-in:2"[unvarify z, OF true_den, THEN "→E", OF true_def] "&E" by blast
AOT_show ‹p ≡ x = ⊤›
proof(safe intro!: "≡I" "→I")
AOT_assume p
AOT_hence ‹∀F (∃q (q & F = [λy q]) ≡ ∃q ((q ≡ p) & F = [λy q]))›
using "TV-lem1:1"[THEN "≡E"(1)] by blast
AOT_hence ‹∀F(⊤[F] ≡ ∃q ((q ≡ p) & F = [λy q]))›
using b "cqt-basic:10"[THEN "→E", OF "&I", OF b] by fast
AOT_hence c: ‹∀F(∃q((q ≡ p) & F = [λy q]) ≡ ⊤[F])›
using "cqt-basic:11"[THEN "≡E"(1)] by fast
AOT_hence ‹∀F (x[F] ≡ ⊤[F])›
using "cqt-basic:10"[THEN "→E", OF "&I", OF θ[THEN "&E"(2)]] by fast
AOT_thus ‹x = ⊤›
by (rule "ab-obey:1"[unvarify y, OF true_den, THEN "→E", THEN "→E",
OF "&I", OF θ[THEN "&E"(1)], OF a])
next
AOT_assume ‹x = ⊤›
AOT_hence d: ‹∀F (⊤[F] ≡ ∃q ((q ≡ p) & F = [λy q]))›
using "rule=E" θ[THEN "&E"(2)] by fast
AOT_have ‹∀F (∃q (q & F = [λy q]) ≡ ∃q ((q ≡ p) & F = [λy q]))›
using "cqt-basic:10"[THEN "→E", OF "&I",
OF b[THEN "cqt-basic:11"[THEN "≡E"(1)]], OF d].
AOT_thus p using "TV-lem1:1"[THEN "≡E"(2)] by blast
qed
qed
AOT_act_theorem "valueof-facts:2": ‹TruthValueOf(x, p) → (¬p ≡ x = ⊥)›
proof(safe intro!: "→I" dest!: "tv-p"[THEN "≡⇩d⇩fE"])
AOT_assume θ: ‹[A!]x & ∀F (x[F] ≡ ∃q ((q ≡ p) & F = [λy q]))›
AOT_have a: ‹A!⊥›
using "∃E" "T-T-value:2" "T-value" "&E"(1) "≡⇩d⇩fE" "tv-p" by blast
AOT_have false_def: ‹⊥ = ❙ιx (A!x & ∀F (x[F] ≡ ∃p(¬p & F = [λy p])))›
by (simp add: "A-descriptions" "rule-id-df:1[zero]" "the-true:2")
AOT_hence false_den: ‹⊥↓›
using "t=t-proper:1" "vdash-properties:6" by blast
AOT_have b: ‹∀F (⊥[F] ≡ ∃q (¬q & F = [λy q]))›
using "y-in:2"[unvarify z, OF false_den, THEN "→E", OF false_def] "&E" by blast
AOT_show ‹¬p ≡ x = ⊥›
proof(safe intro!: "≡I" "→I")
AOT_assume ‹¬p›
AOT_hence ‹∀F (∃q (¬q & F = [λy q]) ≡ ∃q ((q ≡ p) & F = [λy q]))›
using "TV-lem1:2"[THEN "≡E"(1)] by blast
AOT_hence ‹∀F(⊥[F] ≡ ∃q ((q ≡ p) & F = [λy q]))›
using b "cqt-basic:10"[THEN "→E", OF "&I", OF b] by fast
AOT_hence c: ‹∀F(∃q((q ≡ p) & F = [λy q]) ≡ ⊥[F])›
using "cqt-basic:11"[THEN "≡E"(1)] by fast
AOT_hence ‹∀F (x[F] ≡ ⊥[F])›
using "cqt-basic:10"[THEN "→E", OF "&I", OF θ[THEN "&E"(2)]] by fast
AOT_thus ‹x = ⊥›
by (rule "ab-obey:1"[unvarify y, OF false_den, THEN "→E", THEN "→E",
OF "&I", OF θ[THEN "&E"(1)], OF a])
next
AOT_assume ‹x = ⊥›
AOT_hence d: ‹∀F (⊥[F] ≡ ∃q ((q ≡ p) & F = [λy q]))›
using "rule=E" θ[THEN "&E"(2)] by fast
AOT_have ‹∀F (∃q (¬q & F = [λy q]) ≡ ∃q ((q ≡ p) & F = [λy q]))›
using "cqt-basic:10"[THEN "→E", OF "&I",
OF b[THEN "cqt-basic:11"[THEN "≡E"(1)]], OF d].
AOT_thus ‹¬p› using "TV-lem1:2"[THEN "≡E"(2)] by blast
qed
qed
AOT_act_theorem "q-True:1": ‹p ≡ (∘p = ⊤)›
apply (rule "valueof-facts:1"[unvarify x, THEN "→E", rotated, OF "T-lem:1"])
using "≡⇩d⇩fE" "tv-id:2" "&E"(1) "prop-enc" by blast
AOT_act_theorem "q-True:2": ‹¬p ≡ (∘p = ⊥)›
apply (rule "valueof-facts:2"[unvarify x, THEN "→E", rotated, OF "T-lem:1"])
using "≡⇩d⇩fE" "tv-id:2" "&E"(1) "prop-enc" by blast
AOT_act_theorem "q-True:3": ‹p ≡ ⊤❙Σp›
proof(safe intro!: "≡I" "→I")
AOT_assume p
AOT_hence ‹∘p = ⊤› by (metis "≡E"(1) "q-True:1")
moreover AOT_have ‹∘p❙Σp›
by (simp add: "tv-id:2")
ultimately AOT_show ‹⊤❙Σp›
using "rule=E" "T-lem:4" by fast
next
AOT_have true_def: ‹⊤ = ❙ιx (A!x & ∀F (x[F] ≡ ∃p(p & F = [λy p])))›
by (simp add: "A-descriptions" "rule-id-df:1[zero]" "the-true:1")
AOT_hence true_den: ‹⊤↓›
using "t=t-proper:1" "vdash-properties:6" by blast
AOT_have b: ‹∀F (⊤[F] ≡ ∃q (q & F = [λy q]))›
using "y-in:2"[unvarify z, OF true_den, THEN "→E", OF true_def] "&E" by blast
AOT_assume ‹⊤❙Σp›
AOT_hence ‹⊤[λy p]› by (metis "≡⇩d⇩fE" "&E"(2) "prop-enc")
AOT_hence ‹∃q (q & [λy p] = [λy q])›
using b[THEN "∀E"(1), OF "prop-prop2:2", THEN "≡E"(1)] by blast
then AOT_obtain q where ‹q & [λy p] = [λy q]› using "∃E"[rotated] by blast
AOT_thus ‹p›
using "rule=E" "&E"(1) "&E"(2) id_sym "≡E"(2) "p-identity-thm2:3" by fast
qed
AOT_act_theorem "q-True:5": ‹¬p ≡ ⊥❙Σp›
proof(safe intro!: "≡I" "→I")
AOT_assume ‹¬p›
AOT_hence ‹∘p = ⊥› by (metis "≡E"(1) "q-True:2")
moreover AOT_have ‹∘p❙Σp›
by (simp add: "tv-id:2")
ultimately AOT_show ‹⊥❙Σp›
using "rule=E" "T-lem:4" by fast
next
AOT_have false_def: ‹⊥ = ❙ιx (A!x & ∀F (x[F] ≡ ∃p(¬p & F = [λy p])))›
by (simp add: "A-descriptions" "rule-id-df:1[zero]" "the-true:2")
AOT_hence false_den: ‹⊥↓›
using "t=t-proper:1" "vdash-properties:6" by blast
AOT_have b: ‹∀F (⊥[F] ≡ ∃q (¬q & F = [λy q]))›
using "y-in:2"[unvarify z, OF false_den, THEN "→E", OF false_def] "&E" by blast
AOT_assume ‹⊥❙Σp›
AOT_hence ‹⊥[λy p]› by (metis "≡⇩d⇩fE" "&E"(2) "prop-enc")
AOT_hence ‹∃q (¬q & [λy p] = [λy q])›
using b[THEN "∀E"(1), OF "prop-prop2:2", THEN "≡E"(1)] by blast
then AOT_obtain q where ‹¬q & [λy p] = [λy q]› using "∃E"[rotated] by blast
AOT_thus ‹¬p›
using "rule=E" "&E"(1) "&E"(2) id_sym "≡E"(2) "p-identity-thm2:3" by fast
qed
AOT_act_theorem "q-True:4": ‹p ≡ ¬(⊥❙Σp)›
using "q-True:5"
by (metis "deduction-theorem" "≡I" "≡E"(2) "≡E"(4) "raa-cor:3")
AOT_act_theorem "q-True:6": ‹¬p ≡ ¬(⊤❙Σp)›
using "≡E"(1) "oth-class-taut:4:b" "q-True:3" by blast
AOT_define ExtensionOf :: ‹τ ⇒ φ ⇒ φ› (‹ExtensionOf'(_,_')›)
"exten-p": ‹ExtensionOf(x,p) ≡⇩d⇩f A!x &
∀F (x[F] → Propositional([F])) &
∀q ((x❙Σq) ≡ (q ≡ p))›
AOT_theorem "extof-e": ‹ExtensionOf(x, p) ≡ TruthValueOf(x, p)›
proof (safe intro!: "≡I" "→I" "tv-p"[THEN "≡⇩d⇩fI"] "exten-p"[THEN "≡⇩d⇩fI"]
dest!: "tv-p"[THEN "≡⇩d⇩fE"] "exten-p"[THEN "≡⇩d⇩fE"])
AOT_assume 1: ‹[A!]x & ∀F (x[F] → Propositional([F])) & ∀q (x ❙Σ q ≡ (q ≡ p))›
AOT_hence θ: ‹[A!]x & ∀F (x[F] → ∃q(F = [λy q])) & ∀q (x ❙Σ q ≡ (q ≡ p))›
by (AOT_subst ‹∃q(F = [λy q])› ‹Propositional([F])› for: F :: ‹<κ>›)
(auto simp add: "df-rules-formulas[3]" "df-rules-formulas[4]"
"≡I" "prop-prop1")
AOT_show ‹[A!]x & ∀F (x[F] ≡ ∃q ((q ≡ p) & F = [λy q]))›
proof(safe intro!: "&I" GEN 1[THEN "&E"(1), THEN "&E"(1)] "≡I" "→I")
fix F
AOT_assume 0: ‹x[F]›
AOT_hence ‹∃q (F = [λy q])›
using θ[THEN "&E"(1), THEN "&E"(2)] "∀E"(2) "→E" by blast
then AOT_obtain q where q_prop: ‹F = [λy q]› using "∃E"[rotated] by blast
AOT_hence ‹x[λy q]› using 0 "rule=E" by blast
AOT_hence ‹x❙Σq› by (metis "≡⇩d⇩fI" "&I" "ex:1:a" "prop-enc" "rule-ui:3")
AOT_hence ‹q ≡ p› using θ[THEN "&E"(2)] "∀E"(2) "≡E"(1) by blast
AOT_hence ‹(q ≡ p) & F = [λy q]› using q_prop "&I" by blast
AOT_thus ‹∃q ((q ≡ p) & F = [λy q])› by (rule "∃I")
next
fix F
AOT_assume ‹∃q ((q ≡ p) & F = [λy q])›
then AOT_obtain q where q_prop: ‹(q ≡ p) & F = [λy q]›
using "∃E"[rotated] by blast
AOT_hence ‹x❙Σq› using θ[THEN "&E"(2)] "∀E"(2) "&E" "≡E"(2) by blast
AOT_hence ‹x[λy q]› by (metis "≡⇩d⇩fE" "&E"(2) "prop-enc")
AOT_thus ‹x[F]› using q_prop[THEN "&E"(2), symmetric] "rule=E" by blast
qed
next
AOT_assume 0: ‹[A!]x & ∀F (x[F] ≡ ∃q ((q ≡ p) & F = [λy q]))›
AOT_show ‹[A!]x & ∀F (x[F] → Propositional([F])) & ∀q (x ❙Σ q ≡ (q ≡ p))›
proof(safe intro!: "&I" 0[THEN "&E"(1)] GEN "→I")
fix F
AOT_assume ‹x[F]›
AOT_hence ‹∃q ((q ≡ p) & F = [λy q])›
using 0[THEN "&E"(2)] "∀E"(2) "≡E"(1) by blast
then AOT_obtain q where ‹(q ≡ p) & F = [λy q]›
using "∃E"[rotated] by blast
AOT_hence ‹F = [λy q]› using "&E"(2) by blast
AOT_hence ‹∃q F = [λy q]› by (rule "∃I")
AOT_thus ‹Propositional([F])› by (metis "≡⇩d⇩fI" "prop-prop1")
next
AOT_show ‹x❙Σr ≡ (r ≡ p)› for r
proof(rule "≡I"; rule "→I")
AOT_assume ‹x❙Σr›
AOT_hence ‹x[λy r]› by (metis "≡⇩d⇩fE" "&E"(2) "prop-enc")
AOT_hence ‹∃q ((q ≡ p) & [λy r] = [λy q])›
using 0[THEN "&E"(2), THEN "∀E"(1), OF "prop-prop2:2", THEN "≡E"(1)] by blast
then AOT_obtain q where ‹(q ≡ p) & [λy r] = [λy q]›
using "∃E"[rotated] by blast
AOT_thus ‹r ≡ p›
by (metis "rule=E" "&E"(1,2) id_sym "≡E"(2) "Commutativity of ≡"
"p-identity-thm2:3")
next
AOT_assume ‹r ≡ p›
AOT_hence ‹(r ≡ p) & [λy r] = [λy r]›
by (metis "rule=I:1" "≡S"(1) "≡E"(2) "Commutativity of &" "prop-prop2:2")
AOT_hence ‹∃q ((q ≡ p) & [λy r] = [λy q])› by (rule "∃I")
AOT_hence ‹x[λy r]›
using 0[THEN "&E"(2), THEN "∀E"(1), OF "prop-prop2:2", THEN "≡E"(2)] by blast
AOT_thus ‹x❙Σr› by (metis "≡⇩d⇩fI" "&I" "ex:1:a" "prop-enc" "rule-ui:3")
qed
qed
qed
AOT_theorem "ext-p-tv:1": ‹∃!x ExtensionOf(x, p)›
by (AOT_subst ‹ExtensionOf(x, p)› ‹TruthValueOf(x, p)› for: x)
(auto simp: "extof-e" "p-has-!tv:2")
AOT_theorem "ext-p-tv:2": ‹❙ιx(ExtensionOf(x, p))↓›
using "A-Exists:2" "RA[2]" "ext-p-tv:1" "≡E"(2) by blast
AOT_theorem "ext-p-tv:3": ‹❙ιx(ExtensionOf(x, p)) = ∘p›
proof -
AOT_have 0: ‹❙𝒜∀x(ExtensionOf(x, p) ≡ TruthValueOf(x,p))›
by (rule "RA[2]"; rule GEN; rule "extof-e")
AOT_have 1: ‹∘p = ❙ιx TruthValueOf(x,p)›
using "rule-id-df:1" "the-tv-p" "uni-tv" by blast
show ?thesis
apply (rule "equiv-desc-eq:1"[THEN "→E", OF 0, THEN "∀E"(1)[where τ=‹«∘p»›],
THEN "≡E"(2), symmetric])
using "1" "t=t-proper:1" "vdash-properties:10" apply blast
by (fact 1)
qed
end