# Theory AOT_BasicLogicalObjects

(*<*)
theory AOT_BasicLogicalObjects
imports AOT_PLM
begin
(*>*)

section‹Basic Logical Objects›
(* Note: so far only the parts required for possible world theory are implemented *)

AOT_define TruthValueOf :: τ  φ  φ (TruthValueOf'(_,_'))
"tv-p": TruthValueOf(x,p) df 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)

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)

AOT_theorem "uni-tv": ιx TruthValueOf(x,p)
using  "RA[2]" "≡E"(2)  by blast

AOT_define TheTruthValueOf :: φ  κs (_› [100] 100)
"the-tv-p": p =df ιx TruthValueOf(x,p)

AOT_define PropEnc :: τ  φ  φ (infixl Σ 40)
"prop-enc": xΣp df x & xy 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 [THEN "→E", OF "&I", OF "uni-tv"] by simp
thus ?thesis
using "=dfI"(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:  "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!: [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 "dfI"] "&I" )
AOT_thus pΣp
by (rule "rule=E"[rotated, OF "tv-id:1"[symmetric]])
qed

(* TODO more theorems *)

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)  "≡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 ] by blast
moreover AOT_have q ((q  p) & y p] = y q])
by (rule "∃I"(2)[where β=p])
(simp add: "rule=I:1" "&I"  )
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)  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)  "≡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"(1) )
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 ] by blast
moreover AOT_have q ((q  p) & y p] = y q])
by (rule "∃I"(2)[where β=p])
(simp add: "rule=I:1" "&I"  )
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)  by fast
qed

AOT_define TruthValue :: τ  φ (TruthValue'(_'))
"T-value": TruthValue(x) df p (TruthValueOf(x,p))

(* TODO more theorems *)

AOT_act_theorem "T-lem:1": TruthValueOf(p, p)
proof -
AOT_have θ: p = ιx TruthValueOf(x, p)
using  "the-tv-p" "uni-tv" by blast
moreover AOT_have p
using  calculation  by blast
ultimately show ?thesis by (metis "rule=E" id_sym  "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 "dfE"], THEN "&E"(2)].

AOT_act_theorem "T-lem:3": pΣr  (r  p)
proof -
AOT_have θ: py r]  q ((q  p) & y r] = y q])
using "T-lem:2"[THEN "∀E"(1), OF ].
show ?thesis
proof(rule "≡I"; rule "→I")
AOT_assume pΣr
AOT_hence py r] by (metis "dfE" "&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)  by blast
ultimately AOT_show r  p
by (metis "rule=E" "&E"(1) "≡E"(6) )
next
AOT_assume r  p
moreover AOT_have y r] = y r]
by (simp add: "rule=I:1" )
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 py r] using θ "≡E"(2) by blast
AOT_thus pΣr
by (metis "dfI" "&I" "prop-enc" )
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:  GEN)
moreover AOT_have p
using "dfE" "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)  "the-tv-p" "uni-tv" by blast
AOT_thus TruthValueOf(x, p)  x = p using "∀E"(2) by blast
qed

(* TODO more theorems *)

AOT_theorem "TV-lem2:1":
(A!x & F (x[F]  q (q & F = y q])))  TruthValue(x)
proof(safe intro!: "→I" "T-value"[THEN "dfI"] "tv-p"[THEN "dfI"]
"∃I"(1)[rotated, OF ])
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: )
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 "dfI"] "tv-p"[THEN "dfI"]
"∃I"(1)[rotated, OF ])
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"  )
by (auto simp add: )
qed

AOT_define TheTrue :: κs ()
"the-true:1":  =df ιx (A!x & F (x[F]  p(p & F = y p])))
AOT_define TheFalse :: κs ()
"the-true:2":  =df ιx (A!x & F (x[F]  p(¬p & F = y p])))

AOT_theorem "the-true:3":
proof(safe intro!: [unvarify x y, THEN "→E", rotated 2, OF "∨I"(1)]
"∃I"(1)[where τ=«x q(q  q)]»] "&I" )
AOT_have false_def:  = ιx (A!x & F (x[F]  p(¬p & F = y p])))
by (simp add:   )
moreover AOT_show false_den:
by (meson "→E"
)
ultimately AOT_have false_prop: 𝒜(A! & F ([F]  p(¬p & F = y p])))
using [unvarify x, THEN "≡E"(1), THEN "&E"(1)] by blast
AOT_hence 𝒜F ([F]  p(¬p & F = y p]))
using  "&E"(2) "≡E"(1) by blast
AOT_hence F 𝒜([F]  p(¬p & F = y p]))
using "≡E"(1) [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 ] by blast

AOT_have true_def:  = ιx (A!x & F (x[F]  p(p & F = y p])))
by (simp add:   )
moreover AOT_show true_den:
by (meson     "→E")
ultimately AOT_have true_prop: 𝒜(A! & F ([F]  p(p & F = y p])))
using [unvarify x, THEN "≡E"(1), THEN "&E"(1)]  by blast
AOT_hence 𝒜F ([F]  p(p & F = y p]))
using  "&E"(2) "≡E"(1) by blast
AOT_hence F 𝒜([F]  p(p & F = y p]))
using "≡E"(1) [axiom_inst] by blast
AOT_hence 𝒜(x q(q  q)]  p(p & x q(q  q)] = y p]))
using "∀E"(1)[rotated, OF ] by blast
moreover AOT_have 𝒜p(p & x q(q  q)] = y p])
by (safe intro!: [THEN "→E"] RN "∃I"(1)[where τ="«q(q  q)»"] "&I"
GEN "→I"  "rule=I:1" )
ultimately AOT_have 𝒜(x q(q  q)])
using  "≡E"(1,2) by blast
AOT_thus x q(q  q)]
using [unvarify x1 F, THEN "≡E"(1)] true_den  by blast

AOT_show ¬x q(q  q)]
proof(rule )
AOT_assume x q(q  q)]
AOT_hence 𝒜x q(q  q)]
using [unvarify x1 F, THEN "≡E"(2)]
false_den  by blast
AOT_hence 𝒜p(¬p & x q(q  q)] = y p])
using false_enc_cond  "≡E"(1) by blast
AOT_hence p 𝒜(¬p & x q(q  q)] = y p])
using  "≡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  "&E"(2) "≡E"(1))
AOT_hence x q(q  q)] = y p]
using "id-act:1"[unvarify α β, THEN "≡E"(2)]  by blast
AOT_hence (q(q  q)) = p
using [unvarify p, THEN "≡E"(2)]
by blast
moreover AOT_have 𝒜¬p using p_prop
using  "&E"(1) "≡E"(1) by blast
ultimately AOT_have 𝒜¬q(q  q)
by (metis  "≡E"(1,2)  "rule=E")
moreover AOT_have ¬𝒜¬q(q  q)
by (meson  "RA[2]"  "≡E"(1) )
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:   )
AOT_hence true_den:
using   by blast
AOT_show TruthValue()
using "y-in:2"[unvarify z, OF true_den, THEN "→E", OF true_def]
[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:   )
AOT_hence false_den:
using   by blast
AOT_show TruthValue()
using "y-in:2"[unvarify z, OF false_den, THEN "→E", OF false_def]
[unvarify x, OF false_den, THEN "→E"] by blast
qed

AOT_theorem "two-T": xy(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 [axiom_inst] "∃E"[rotated] by fast
AOT_obtain b where b_prop: A!b & F (b[F]  p (¬p & F = y p]))
using [axiom_inst] "∃E"[rotated] by fast
AOT_obtain p where p: p
by (metis    )
show ?thesis
proof(rule "∃I"(2)[where β=a]; rule "∃I"(2)[where β=b];
safe intro!: "&I" GEN "→I")
AOT_show TruthValue(a)
using  a_prop  by blast
next
AOT_show TruthValue(b)
using  b_prop  by blast
next
AOT_show a  b
proof(rule [THEN "→E", OF "∨I"(1)])
AOT_show F (a[F] & ¬b[F])
proof(rule "∃I"(1)[where τ="«y p]»"]; rule "&I" )
AOT_show ay p]
by(safe intro!: "∃I"(2)[where β=p] "&I" p "rule=I:1"[OF ]
a_prop[THEN "&E"(2), THEN "∀E"(1), THEN "≡E"(2), OF ])
next
AOT_show ¬by p]
proof (rule )
AOT_assume by p]
AOT_hence q (¬q & y p] = y q])
using "∀E"(1)[rotated, OF , 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)  "≡I"
"≡E"(2)  )
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 "dfE" "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 "dfE" "tv-p" by blast
{
AOT_assume p: p
AOT_have z = a
proof(rule [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 [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 [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 [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 )
qed
qed

AOT_act_theorem "valueof-facts:1": TruthValueOf(x, p)  (p  x = )
proof(safe intro!: "→I" dest!: "tv-p"[THEN "dfE"])
AOT_assume θ: [A!]x & F (x[F]  q ((q  p) & F = y q]))
AOT_have a: A!
using "∃E"  "T-value" "&E"(1) "dfE" "tv-p" by blast
AOT_have true_def:  = ιx (A!x & F (x[F]  p(p & F = y p])))
by (simp add:   )
AOT_hence true_den:
using   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 [THEN "≡E"(1)] by blast
AOT_hence F([F]  q ((q  p) & F = y q]))
using b [THEN "→E", OF "&I", OF b] by fast
AOT_hence c: F(q((q  p) & F = y q])  [F])
using [THEN "≡E"(1)] by fast
AOT_hence F (x[F]  [F])
using [THEN "→E", OF "&I", OF θ[THEN "&E"(2)]] by fast
AOT_thus x =
by (rule [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 [THEN "→E", OF "&I",
OF b[THEN [THEN "≡E"(1)]], OF d].
AOT_thus p using [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 "dfE"])
AOT_assume θ: [A!]x & F (x[F]  q ((q  p) & F = y q]))
AOT_have a: A!
using "∃E"  "T-value" "&E"(1) "dfE" "tv-p" by blast
AOT_have false_def:  = ιx (A!x & F (x[F]  p(¬p & F = y p])))
by (simp add:   )
AOT_hence false_den:
using   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 [THEN "≡E"(1)] by blast
AOT_hence F([F]  q ((q  p) & F = y q]))
using b [THEN "→E", OF "&I", OF b] by fast
AOT_hence c: F(q((q  p) & F = y q])  [F])
using [THEN "≡E"(1)] by fast
AOT_hence F (x[F]  [F])
using [THEN "→E", OF "&I", OF θ[THEN "&E"(2)]] by fast
AOT_thus x =
by (rule [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 [THEN "→E", OF "&I",
OF b[THEN [THEN "≡E"(1)]], OF d].
AOT_thus ¬p using [THEN "≡E"(2)] by blast
qed
qed

AOT_act_theorem "q-True:1": p  (p = )
apply (rule [unvarify x, THEN "→E", rotated, OF "T-lem:1"])
using "dfE" "tv-id:2" "&E"(1) "prop-enc" by blast

AOT_act_theorem "q-True:2": ¬p  (p = )
apply (rule [unvarify x, THEN "→E", rotated, OF "T-lem:1"])
using "dfE" "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:   )
AOT_hence true_den:
using   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 "dfE" "&E"(2) "prop-enc")
AOT_hence q (q & y p] = y q])
using b[THEN "∀E"(1), OF , 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)  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:   )
AOT_hence false_den:
using   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 "dfE" "&E"(2) "prop-enc")
AOT_hence q (¬q & y p] = y q])
using b[THEN "∀E"(1), OF , 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)  by fast
qed

AOT_act_theorem "q-True:4": p  ¬(Σp)
using "q-True:5"
by (metis  "≡I" "≡E"(2) "≡E"(4) )

AOT_act_theorem "q-True:6": ¬p  ¬(Σp)
using "≡E"(1)  "q-True:3" by blast

AOT_define ExtensionOf :: τ  φ  φ (ExtensionOf'(_,_'))
"exten-p": ExtensionOf(x,p) df 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 "dfI"] "exten-p"[THEN "dfI"]
dest!: "tv-p"[THEN "dfE"] "exten-p"[THEN "dfE"])
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 :: ‹<κ>›)
"≡I" )
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 xy q] using 0 "rule=E" by blast
AOT_hence xΣq by (metis "dfI" "&I" "ex:1:a" "prop-enc" )
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 xy q] by (metis "dfE" "&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 "dfI" )
next
AOT_show xΣr  (r  p) for r
proof(rule "≡I"; rule "→I")
AOT_assume xΣr
AOT_hence xy r] by (metis "dfE" "&E"(2) "prop-enc")
AOT_hence q ((q  p) & y r] = y q])
using 0[THEN "&E"(2), THEN "∀E"(1), OF , 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)
)
next
AOT_assume r  p
AOT_hence (r  p) & y r] = y r]
by (metis "rule=I:1" "≡S"(1) "≡E"(2)  )
AOT_hence q ((q  p) & y r] = y q]) by (rule "∃I")
AOT_hence xy r]
using 0[THEN "&E"(2), THEN "∀E"(1), OF , THEN "≡E"(2)] by blast
AOT_thus xΣr by (metis "dfI" "&I" "ex:1:a" "prop-enc" )
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" )

AOT_theorem "ext-p-tv:2": ιx(ExtensionOf(x, p))
using  "RA[2]"  "≡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  "the-tv-p" "uni-tv" by blast
show ?thesis
apply (rule [THEN "→E", OF 0, THEN "∀E"(1)[where τ=«p»],
THEN "≡E"(2), symmetric])
using "1"   apply blast
by (fact 1)
qed
(*<*)end(*>*)