theory TAO_99_Paradox
imports TAO_9_PLM TAO_98_ArtificialTheorems
begin

(*<*)
begin
(*>*)

text‹
Under the additional assumption that expressions of the form
@{term "(λx . ⦇G,❙ιy . φ y x⦈)"} for arbitrary ‹φ› are
\emph{proper maps}, for which ‹β›-conversion holds,
the theory becomes inconsistent.
›

subsection‹Auxiliary Lemmas›

lemma exe_impl_exists:
"[⦇(❙λx . ❙∀ p . p ❙→ p), ❙ιy . φ y x⦈ ❙≡ (❙∃!y . ❙𝒜φ y x) in v]"
proof (rule "❙≡I"; rule CP)
fix φ :: "ν⇒ν⇒𝗈" and x :: ν and v :: i
assume "[⦇(❙λx . ❙∀ p . p ❙→ p),❙ιy . φ y x⦈ in v]"
hence "[❙∃y. ❙𝒜φ y x ❙& (❙∀z. ❙𝒜φ z x ❙→ z ❙= y)
❙& ⦇(❙λx . ❙∀ p . p ❙→ p), y⇧P⦈ in v]"
using nec_russell_axiom[equiv_lr] SimpleExOrEnc.intros by auto
then obtain y where
"[❙𝒜φ y x ❙& (❙∀z. ❙𝒜φ z x ❙→ z ❙= y)
❙& ⦇(❙λx . ❙∀ p . p ❙→ p), y⇧P⦈ in v]"
by (rule Instantiate)
hence "[❙𝒜φ y x ❙& (❙∀z. ❙𝒜φ z x ❙→ z ❙= y) in v]"
using "❙&E" by blast
hence "[❙∃y . ❙𝒜φ y x ❙& (❙∀z. ❙𝒜φ z x ❙→ z ❙= y) in v]"
by (rule existential)
thus "[❙∃!y. ❙𝒜φ y x in v]"
unfolding exists_unique_def by simp
next
fix φ :: "ν⇒ν⇒𝗈" and x :: ν and v :: i
assume "[❙∃!y. ❙𝒜φ y x in v]"
hence "[❙∃y. ❙𝒜φ y x ❙& (❙∀z. ❙𝒜φ z x ❙→ z ❙= y) in v]"
unfolding exists_unique_def by simp
then obtain y where
"[❙𝒜φ y x ❙& (❙∀z. ❙𝒜φ z x ❙→ z ❙= y) in v]"
by (rule Instantiate)
moreover have "[⦇(❙λx . ❙∀ p . p ❙→ p),y⇧P⦈ in v]"
apply (rule beta_C_meta_1[equiv_rl])
apply show_proper
by PLM_solver
ultimately have "[❙𝒜φ y x ❙& (❙∀z. ❙𝒜φ z x ❙→ z ❙= y)
❙& ⦇(❙λx . ❙∀ p . p ❙→ p),y⇧P⦈ in v]"
using "❙&I" by blast
hence "[❙∃ y . ❙𝒜φ y x ❙& (❙∀z. ❙𝒜φ z x ❙→ z ❙= y)
❙& ⦇(❙λx . ❙∀ p . p ❙→ p),y⇧P⦈ in v]"
by (rule existential)
thus "[⦇(❙λx . ❙∀ p . p ❙→ p), ❙ιy. φ y x⦈ in v]"
using nec_russell_axiom[equiv_rl]
SimpleExOrEnc.intros by auto
qed

lemma exists_unique_actual_equiv:
"[(❙∃!y . ❙𝒜(y ❙= x ❙& ψ (x⇧P))) ❙≡ ❙𝒜ψ (x⇧P) in v]"
proof (rule "❙≡I"; rule CP)
fix x v
let ?φ = "λ y x. y ❙= x ❙& ψ (x⇧P)"
assume "[❙∃!y. ❙𝒜?φ y x in v]"
hence "[❙∃α. ❙𝒜?φ α x ❙& (❙∀β. ❙𝒜?φ β x ❙→ β ❙= α) in v]"
unfolding exists_unique_def by simp
then obtain α where
"[❙𝒜?φ α x ❙& (❙∀β. ❙𝒜?φ β x ❙→ β ❙= α) in v]"
by (rule Instantiate)
hence "[❙𝒜(α ❙= x ❙& ψ (x⇧P)) in v]"
using "❙&E" by blast
thus "[❙𝒜(ψ (x⇧P)) in v]"
using Act_Basic_2[equiv_lr] "❙&E" by blast
next
fix x v
let ?φ = "λ y x. y ❙= x ❙& ψ (x⇧P)"
assume 1: "[❙𝒜ψ (x⇧P) in v]"
have "[x ❙= x in v]"
using id_eq_1[where 'a=ν] by simp
hence "[❙𝒜(x ❙= x) in v]"
using id_act_3[equiv_lr] by fast
hence "[❙𝒜(x ❙= x ❙& ψ (x⇧P)) in v]"
using 1 Act_Basic_2[equiv_rl] "❙&I" by blast
hence "[❙𝒜?φ x x in v]"
by simp
moreover have "[❙∀β. ❙𝒜?φ β x ❙→ β ❙= x in v]"
proof (rule "❙∀I"; rule CP)
fix β
assume "[❙𝒜?φ β x in v]"
hence "[❙𝒜(β ❙= x) in v]"
using Act_Basic_2[equiv_lr] "❙&E" by fast
thus "[β ❙= x in v]" using id_act_3[equiv_rl] by fast
qed
ultimately have "[❙𝒜?φ x x ❙& (❙∀β. ❙𝒜?φ β x ❙→ β ❙= x) in v]"
using "❙&I" by fast
hence "[❙∃α. ❙𝒜?φ α x ❙& (❙∀β. ❙𝒜?φ β x ❙→ β ❙= α) in v]"
by (rule existential)
thus "[❙∃!y. ❙𝒜?φ y x in v]"
unfolding exists_unique_def by simp
qed

subsection‹Fake $\beta$-Conversion using Description Backdoor›
text‹
›

definition backdoor where
"backdoor ≡ λ ψ . ❙λx . ⦇(❙λx . ❙∀ p . p ❙→ p), ❙ιy . y ❙= x ❙& ψ (x⇧P)⦈"

lemma fake_beta:
assumes "⋀ G φ. IsProperInX (λx . ⦇G,❙ιy . φ y x⦈)"
shows "[⦇backdoor (λ x . ψ x), x⇧P⦈ ❙≡ ❙𝒜ψ (x⇧P) in v]"
proof (rule "❙≡I"; rule CP)
assume "[⦇backdoor ψ,x⇧P⦈ in v]"
hence "[⦇❙λx. ❙∀p. p ❙→ p,❙ιy. y ❙= x ❙& ψ (x⇧P)⦈ in v]"
using beta_C_meta_1[equiv_lr, OF assms]
unfolding backdoor_def identity_ν_def by fast
hence "[❙∃!y. ❙𝒜 (y ❙= x ❙& ψ (x⇧P)) in v]"
using exe_impl_exists[equiv_lr] by fast
thus "[❙𝒜ψ (x⇧P) in v]"
using exists_unique_actual_equiv[equiv_lr] by blast
next
assume "[❙𝒜ψ (x⇧P) in v]"
hence "[❙∃!y. ❙𝒜 (y ❙= x ❙& ψ (x⇧P)) in v]"
using exists_unique_actual_equiv[equiv_rl] by blast
hence "[⦇❙λx. ❙∀p. p ❙→ p,❙ιy. y ❙= x ❙& ψ (x⇧P)⦈ in v]"
using exe_impl_exists[equiv_rl] by fast
thus "[⦇backdoor ψ,x⇧P⦈ in v]"
using beta_C_meta_1[equiv_rl, OF assms]
unfolding backdoor_def unfolding identity_ν_def by fast
qed

lemma fake_beta_act:
assumes "⋀ G φ. IsProperInX (λx . ⦇G,❙ιy . φ y x⦈)"
shows "[⦇backdoor (λ x . ψ x), x⇧P⦈ ❙≡ ψ (x⇧P) in dw]"
using fake_beta[OF assms]
logic_actual[necessitation_averse_axiom_instance]
intro_elim_6_e by blast

text‹
›

assumes "⋀ G φ. IsProperInX (λx . ⦇G,❙ιy . φ y x⦈)"
shows "False"
proof -
obtain K where K_def:
"K = backdoor (λ x . ❙∃ F . ⦃x,F⦄ ❙& ❙¬⦇F,x⦈)" by auto
have "[❙∃x. ⦇A!,x⇧P⦈ ❙& (❙∀F. ⦃x⇧P,F⦄ ❙≡ (F ❙= K)) in dw]"
using A_objects[axiom_instance] by fast
then obtain x where x_prop:
"[⦇A!,x⇧P⦈ ❙& (❙∀F. ⦃x⇧P,F⦄ ❙≡ (F ❙= K)) in dw]"
by (rule Instantiate)
{
assume "[⦇K,x⇧P⦈ in dw]"
hence "[❙∃ F . ⦃x⇧P,F⦄ ❙& ❙¬⦇F,x⇧P⦈ in dw]"
unfolding K_def using fake_beta_act[OF assms, equiv_lr]
by blast
then obtain F where F_def:
"[⦃x⇧P,F⦄ ❙& ❙¬⦇F,x⇧P⦈ in dw]" by (rule Instantiate)
hence "[F ❙= K in dw]"
using x_prop[conj2, THEN "❙∀E"[where β=F], equiv_lr]
"❙&E" unfolding K_def by blast
hence "[❙¬⦇K,x⇧P⦈ in dw]"
using l_identity[axiom_instance,deduction,deduction]
F_def[conj2] by fast
}
hence 1: "[❙¬⦇K,x⇧P⦈ in dw]"
using reductio_aa_1 by blast
hence "[❙¬(❙∃ F . ⦃x⇧P,F⦄ ❙& ❙¬⦇F,x⇧P⦈) in dw]"
using fake_beta_act[OF assms,
THEN oth_class_taut_5_d[equiv_lr],
equiv_lr]
unfolding K_def by blast
hence "[❙∀ F . ⦃x⇧P,F⦄ ❙→ ⦇F,x⇧P⦈ in dw]"
apply - unfolding exists_def by PLM_solver
moreover have "[⦃x⇧P,K⦄ in dw]"
using x_prop[conj2, THEN "❙∀E"[where β=K], equiv_rl]
id_eq_1 by blast
ultimately have "[⦇K,x⇧P⦈ in dw]"
using "❙∀E" vdash_properties_10 by blast
hence "⋀φ. [φ in dw]"
using raa_cor_2 1 by blast
thus "False" using Semantics.T4 by auto
qed

text‹
Originally the paradox was discovered using the following
construction based on the comprehension theorem for relations
without the explicit construction of the description backdoor
and the resulting fake-‹β›-conversion.
›

lemma assumes "⋀ G φ. IsProperInX (λx . ⦇G,❙ιy . φ y x⦈)"
shows Fx_equiv_xH: "[❙∀ H . ❙∃ F . ❙□(❙∀x. ⦇F,x⇧P⦈ ❙≡ ⦃x⇧P,H⦄) in v]"
proof (rule "❙∀I")
fix H
let ?G = "(❙λx . ❙∀ p . p ❙→ p)"
obtain φ where φ_def: "φ = (λ y x . (y⇧P) ❙= x ❙& ⦃x,H⦄)" by auto
have "[❙∃F. ❙□(❙∀x. ⦇F,x⇧P⦈ ❙≡ ⦇?G,❙ιy . φ y (x⇧P)⦈) in v]"
using relations_1[OF assms] by simp
hence 1: "[❙∃F. ❙□(❙∀x. ⦇F,x⇧P⦈ ❙≡ (❙∃!y . ❙𝒜φ y (x⇧P))) in v]"
apply - apply (PLM_subst_method
"λ x . ⦇?G,❙ιy . φ y (x⇧P)⦈" "λ x . (❙∃!y. ❙𝒜φ y (x⇧P))")
using exe_impl_exists by auto
then obtain F where F_def: "[❙□(❙∀x. ⦇F,x⇧P⦈ ❙≡ (❙∃!y . ❙𝒜φ y (x⇧P))) in v]"
by (rule Instantiate)
moreover have 2: "⋀ v x . [(❙∃!y . ❙𝒜φ y (x⇧P)) ❙≡ ⦃x⇧P,H⦄ in v]"
proof (rule "❙≡I"; rule CP)
fix x v
assume "[❙∃!y. ❙𝒜φ y (x⇧P) in v]"
hence "[❙∃α. ❙𝒜φ α (x⇧P) ❙& (❙∀β. ❙𝒜φ β (x⇧P) ❙→ β ❙= α) in v]"
unfolding exists_unique_def by simp
then obtain α where "[❙𝒜φ α (x⇧P) ❙& (❙∀β. ❙𝒜φ β (x⇧P) ❙→ β ❙= α) in v]"
by (rule Instantiate)
hence "[❙𝒜(α⇧P ❙= x⇧P ❙& ⦃x⇧P,H⦄) in v]"
unfolding φ_def using "❙&E" by blast
hence "[❙𝒜(⦃x⇧P,H⦄) in v]"
using Act_Basic_2[equiv_lr] "❙&E" by blast
thus "[⦃x⇧P,H⦄ in v]"
using en_eq_10[equiv_lr] by simp
next
fix x v
assume "[⦃x⇧P,H⦄ in v]"
hence 1: "[❙𝒜(⦃x⇧P,H⦄) in v]"
using en_eq_10[equiv_rl] by blast
have "[x ❙= x in v]"
using id_eq_1[where 'a=ν] by simp
hence "[❙𝒜(x ❙= x) in v]"
using id_act_3[equiv_lr] by fast
hence "[❙𝒜(x⇧P ❙= x⇧P ❙& ⦃x⇧P,H⦄) in v]"
unfolding identity_ν_def using 1 Act_Basic_2[equiv_rl] "❙&I" by blast
hence "[❙𝒜φ x (x⇧P) in v]"
unfolding φ_def by simp
moreover have "[❙∀β. ❙𝒜φ β (x⇧P) ❙→ β ❙= x in v]"
proof (rule "❙∀I"; rule CP)
fix β
assume "[❙𝒜φ β (x⇧P) in v]"
hence "[❙𝒜(β ❙= x) in v]"
unfolding φ_def identity_ν_def
using Act_Basic_2[equiv_lr] "❙&E" by fast
thus "[β ❙= x in v]" using id_act_3[equiv_rl] by fast
qed
ultimately have "[❙𝒜φ x (x⇧P) ❙& (❙∀β. ❙𝒜φ β (x⇧P) ❙→ β ❙= x) in v]"
using "❙&I" by fast
hence "[❙∃α. ❙𝒜φ α (x⇧P) ❙& (❙∀β. ❙𝒜φ β (x⇧P) ❙→ β ❙= α) in v]"
by (rule existential)
thus "[❙∃!y. ❙𝒜φ y (x⇧P) in v]"
unfolding exists_unique_def by simp
qed
have "[❙□(❙∀x. ⦇F,x⇧P⦈ ❙≡ ⦃x⇧P,H⦄) in v]"
apply (PLM_subst_goal_method
"λφ . ❙□(❙∀x. ⦇F,x⇧P⦈ ❙≡ φ x)"
"λ x . (❙∃!y . ❙𝒜φ y (x⇧P))")
using 2 F_def by auto
thus "[❙∃ F . ❙□(❙∀x. ⦇F,x⇧P⦈ ❙≡ ⦃x⇧P,H⦄) in v]"
by (rule existential)
qed

lemma
assumes is_propositional: "(⋀G φ. IsProperInX (λx. ⦇G,❙ιy. φ y x⦈))"
and Abs_x: "[⦇A!,x⇧P⦈ in v]"
and Abs_y: "[⦇A!,y⇧P⦈ in v]"
and noteq: "[x ❙≠ y in v]"
shows diffprop: "[❙∃ F . ❙¬(⦇F,x⇧P⦈ ❙≡ ⦇F,y⇧P⦈) in v]"
proof -
have "[❙∃ F . ❙¬(⦃x⇧P, F⦄ ❙≡ ⦃y⇧P, F⦄) in v]"
using noteq unfolding exists_def
proof (rule reductio_aa_2)
assume 1: "[❙∀F. ❙¬❙¬(⦃x⇧P,F⦄ ❙≡ ⦃y⇧P,F⦄) in v]"
{
fix F
have "[(⦃x⇧P,F⦄ ❙≡ ⦃y⇧P,F⦄) in v]"
using 1[THEN "❙∀E"] useful_tautologies_1[deduction] by blast
}
hence "[❙∀F. ⦃x⇧P,F⦄ ❙≡ ⦃y⇧P,F⦄ in v]" by (rule "❙∀I")
thus "[x ❙= y in v]"
unfolding identity_ν_def
using ab_obey_1[deduction, deduction]
Abs_x Abs_y "❙&I" by blast
qed
then obtain H where H_def: "[❙¬(⦃x⇧P, H⦄ ❙≡ ⦃y⇧P, H⦄) in v]"
by (rule Instantiate)
hence 2: "[(⦃x⇧P, H⦄ ❙& ❙¬⦃y⇧P, H⦄) ❙∨ (❙¬⦃x⇧P, H⦄ ❙& ⦃y⇧P, H⦄) in v]"
apply - by PLM_solver
have "[❙∃F. ❙□(❙∀x. ⦇F,x⇧P⦈ ❙≡ ⦃x⇧P,H⦄) in v]"
using Fx_equiv_xH[OF is_propositional, THEN "❙∀E"] by simp
then obtain F where "[❙□(❙∀x. ⦇F,x⇧P⦈ ❙≡ ⦃x⇧P,H⦄) in v]"
by (rule Instantiate)
hence F_prop: "[❙∀x. ⦇F,x⇧P⦈ ❙≡ ⦃x⇧P,H⦄ in v]"
using qml_2[axiom_instance, deduction] by blast
hence a: "[⦇F,x⇧P⦈ ❙≡ ⦃x⇧P,H⦄ in v]"
using "❙∀E" by blast
have b: "[⦇F,y⇧P⦈ ❙≡ ⦃y⇧P,H⦄ in v]"
using F_prop "❙∀E" by blast
{
assume 1: "[⦃x⇧P, H⦄ ❙& ❙¬⦃y⇧P, H⦄ in v]"
hence "[⦇F,x⇧P⦈ in v]"
using a[equiv_rl] "❙&E" by blast
moreover have "[❙¬⦇F,y⇧P⦈ in v]"
using b[THEN oth_class_taut_5_d[equiv_lr], equiv_rl] 1[conj2] by auto
ultimately have "[⦇F,x⇧P⦈ ❙& (❙¬⦇F,y⇧P⦈) in v]"
by (rule "❙&I")
hence "[(⦇F,x⇧P⦈ ❙& ❙¬⦇F,y⇧P⦈) ❙∨ (❙¬⦇F,x⇧P⦈ ❙& ⦇F,y⇧P⦈) in v]"
using "❙∨I" by blast
hence "[❙¬(⦇F,x⇧P⦈ ❙≡ ⦇F,y⇧P⦈) in v]"
using oth_class_taut_5_j[equiv_rl] by blast
}
moreover {
assume 1: "[❙¬⦃x⇧P, H⦄ ❙& ⦃y⇧P, H⦄ in v]"
hence "[⦇F,y⇧P⦈ in v]"
using b[equiv_rl] "❙&E" by blast
moreover have "[❙¬⦇F,x⇧P⦈ in v]"
using a[THEN oth_class_taut_5_d[equiv_lr], equiv_rl] 1[conj1] by auto
ultimately have "[❙¬⦇F,x⇧P⦈ ❙& ⦇F,y⇧P⦈ in v]"
using "❙&I" by blast
hence "[(⦇F,x⇧P⦈ ❙& ❙¬⦇F,y⇧P⦈) ❙∨ (❙¬⦇F,x⇧P⦈ ❙& ⦇F,y⇧P⦈) in v]"
using "❙∨I" by blast
hence "[❙¬(⦇F,x⇧P⦈ ❙≡ ⦇F,y⇧P⦈) in v]"
using oth_class_taut_5_j[equiv_rl] by blast
}
ultimately have "[❙¬(⦇F,x⇧P⦈ ❙≡ ⦇F,y⇧P⦈) in v]"
using 2 intro_elim_4_b reductio_aa_1 by blast
thus "[❙∃ F . ❙¬(⦇F,x⇧P⦈ ❙≡ ⦇F,y⇧P⦈) in v]"
by (rule existential)
qed

assumes is_propositional: "(⋀G φ. IsProperInX (λx. ⦇G,❙ιy. φ y x⦈))"
shows "False"
proof -
fix v
have "[❙∃x y. ⦇A!,x⇧P⦈ ❙& ⦇A!,y⇧P⦈ ❙& x ❙≠ y ❙& (❙∀F. ⦇F,x⇧P⦈ ❙≡ ⦇F,y⇧P⦈) in v]"
using aclassical2 by auto
then obtain x where
"[❙∃ y. ⦇A!,x⇧P⦈ ❙& ⦇A!,y⇧P⦈ ❙& x ❙≠ y ❙& (❙∀F. ⦇F,x⇧P⦈ ❙≡ ⦇F,y⇧P⦈) in v]"
by (rule Instantiate)
then obtain y where xy_def:
"[⦇A!,x⇧P⦈ ❙& ⦇A!,y⇧P⦈ ❙& x ❙≠ y ❙& (❙∀F. ⦇F,x⇧P⦈ ❙≡ ⦇F,y⇧P⦈) in v]"
by (rule Instantiate)
have "[❙∃ F . ❙¬(⦇F,x⇧P⦈ ❙≡ ⦇F,y⇧P⦈) in v]"
using diffprop[OF assms, OF xy_def[conj1,conj1,conj1],
OF xy_def[conj1,conj1,conj2],
OF xy_def[conj1,conj2]]
by auto
then obtain F where "[❙¬(⦇F,x⇧P⦈ ❙≡ ⦇F,y⇧P⦈) in v]"
by (rule Instantiate)
moreover have "[⦇F,x⇧P⦈ ❙≡ ⦇F,y⇧P⦈ in v]"
using xy_def[conj2] by (rule "❙∀E")
ultimately have "⋀φ.[φ in v]"
using PLM.raa_cor_2 by blast
thus "False"
using Semantics.T4 by auto
qed

(*<*)
end
(*>*)

end