Theory TAO_99_Paradox

theory TAO_99_Paradox
imports TAO_9_PLM TAO_98_ArtificialTheorems
begin

section‹Paradox›

(*<*)
locale Paradox = PLM
begin
(*>*)

text‹
\label{TAO_Paradox_paradox}
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), yP 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), yP 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),yP 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),yP in v]"
        using "&I" by blast
      hence "[ y . 𝒜φ y x & (z. 𝒜φ z x  z = y)
              & (λx .  p . p  p),yP 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 & ψ (xP)))  𝒜ψ (xP) in v]"
  proof (rule "I"; rule CP)
    fix x v
    let  = "λ y x. y = x & ψ (xP)"
    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 & ψ (xP)) in v]"
      using "&E" by blast
    thus "[𝒜(ψ (xP)) in v]"
      using Act_Basic_2[equiv_lr] "&E" by blast
  next
    fix x v
    let  = "λ y x. y = x & ψ (xP)"
    assume 1: "[𝒜ψ (xP) 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 & ψ (xP)) 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‹
  \label{TAO_Paradox_description_backdoor}
›
    
  definition backdoor where
    "backdoor  λ ψ . λx . (λx .  p . p  p), ιy . y = x & ψ (xP)"
    
  lemma fake_beta:
    assumes " G φ. IsProperInX (λx . G,ιy . φ y x)"
    shows "[backdoor (λ x . ψ x), xP  𝒜ψ (xP) in v]"
  proof (rule "I"; rule CP)
    assume "[backdoor ψ,xP in v]"
    hence "[λx. p. p  p,ιy. y = x & ψ (xP) in v]"
      using beta_C_meta_1[equiv_lr, OF assms]
      unfolding backdoor_def identity_ν_def by fast
    hence "[!y. 𝒜 (y = x & ψ (xP)) in v]"
      using exe_impl_exists[equiv_lr] by fast
    thus "[𝒜ψ (xP) in v]"
      using exists_unique_actual_equiv[equiv_lr] by blast
  next
    assume "[𝒜ψ (xP) in v]"
    hence "[!y. 𝒜 (y = x & ψ (xP)) in v]"
      using exists_unique_actual_equiv[equiv_rl] by blast
    hence "[λx. p. p  p,ιy. y = x & ψ (xP) in v]"
      using exe_impl_exists[equiv_rl] by fast
    thus "[backdoor ψ,xP 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), xP  ψ (xP) in dw]"
    using fake_beta[OF assms]
      logic_actual[necessitation_averse_axiom_instance]
      intro_elim_6_e by blast

subsection‹Resulting Paradox›

text‹
  \label{TAO_Paradox_russell-paradox}
›
  
  lemma paradox:
    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!,xP & (F. xP,F  (F = K)) in dw]"
      using A_objects[axiom_instance] by fast
    then obtain x where x_prop:
      "[A!,xP & (F. xP,F  (F = K)) in dw]"
      by (rule Instantiate)
    {
      assume "[K,xP in dw]"
      hence "[ F . xP,F & ¬F,xP in dw]"
        unfolding K_def using fake_beta_act[OF assms, equiv_lr]
        by blast
      then obtain F where F_def:
        "[xP,F & ¬F,xP 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,xP in dw]"
        using l_identity[axiom_instance,deduction,deduction]
             F_def[conj2] by fast
    }
    hence 1: "[¬K,xP in dw]"
      using reductio_aa_1 by blast
    hence "[¬( F . xP,F & ¬F,xP) 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 . xP,F  F,xP in dw]"
      apply - unfolding exists_def by PLM_solver
    moreover have "[xP,K in dw]"
      using x_prop[conj2, THEN "E"[where β=K], equiv_rl]
            id_eq_1 by blast
    ultimately have "[K,xP 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

subsection‹Original Version of the Paradox›

text‹
  \label{TAO_Paradox_original-paradox}
  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,xP  xP,H) in v]"
  proof (rule "I")
    fix H
    let ?G = "(λx .  p . p  p)"
    obtain φ where φ_def: "φ = (λ y x . (yP) = x & x,H)" by auto
    have "[F. (x. F,xP  ?G,ιy . φ y (xP)) in v]"
      using relations_1[OF assms] by simp
    hence 1: "[F. (x. F,xP  (!y . 𝒜φ y (xP))) in v]"
      apply - apply (PLM_subst_method
          "λ x . ?G,ιy . φ y (xP)" "λ x . (!y. 𝒜φ y (xP))")
      using exe_impl_exists by auto
    then obtain F where F_def: "[(x. F,xP  (!y . 𝒜φ y (xP))) in v]"
      by (rule Instantiate)
    moreover have 2: " v x . [(!y . 𝒜φ y (xP))  xP,H in v]"
    proof (rule "I"; rule CP)
      fix x v
      assume "[!y. 𝒜φ y (xP) in v]"
      hence "[α. 𝒜φ α (xP) & (β. 𝒜φ β (xP)  β = α) in v]"
        unfolding exists_unique_def by simp
      then obtain α where "[𝒜φ α (xP) & (β. 𝒜φ β (xP)  β = α) in v]"
        by (rule Instantiate)
      hence "[𝒜(αP = xP & xP,H) in v]"
        unfolding φ_def using "&E" by blast
      hence "[𝒜(xP,H) in v]"
        using Act_Basic_2[equiv_lr] "&E" by blast
      thus "[xP,H in v]"
        using en_eq_10[equiv_lr] by simp
    next
      fix x v
      assume "[xP,H in v]"
      hence 1: "[𝒜(xP,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 "[𝒜(xP = xP & xP,H) in v]"
        unfolding identity_ν_def using 1 Act_Basic_2[equiv_rl] "&I" by blast
      hence "[𝒜φ x (xP) in v]"
        unfolding φ_def by simp
      moreover have "[β. 𝒜φ β (xP)  β = x in v]"
      proof (rule "I"; rule CP)
        fix β
        assume "[𝒜φ β (xP) 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 (xP) & (β. 𝒜φ β (xP)  β = x) in v]"
        using "&I" by fast
      hence "[α. 𝒜φ α (xP) & (β. 𝒜φ β (xP)  β = α) in v]"
        by (rule existential)
      thus "[!y. 𝒜φ y (xP) in v]"
        unfolding exists_unique_def by simp
    qed
    have "[(x. F,xP  xP,H) in v]"
      apply (PLM_subst_goal_method
          "λφ . (x. F,xP  φ x)"
          "λ x . (!y . 𝒜φ y (xP))")
      using 2 F_def by auto
    thus "[ F . (x. F,xP  xP,H) in v]"
      by (rule existential)
  qed

            
  lemma
    assumes is_propositional: "(G φ. IsProperInX (λx. G,ιy. φ y x))"
        and Abs_x: "[A!,xP in v]"
        and Abs_y: "[A!,yP in v]"
        and noteq: "[x  y in v]"
  shows diffprop: "[ F . ¬(F,xP  F,yP) in v]"
  proof -
    have "[ F . ¬(xP, F  yP, F) in v]"
      using noteq unfolding exists_def
    proof (rule reductio_aa_2)
      assume 1: "[F. ¬¬(xP,F  yP,F) in v]"
      {
        fix F
        have "[(xP,F  yP,F) in v]"
          using 1[THEN "E"] useful_tautologies_1[deduction] by blast
      }
      hence "[F. xP,F  yP,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: "[¬(xP, H  yP, H) in v]"
      by (rule Instantiate)
    hence 2: "[(xP, H & ¬yP, H)  (¬xP, H & yP, H) in v]"
      apply - by PLM_solver
    have "[F. (x. F,xP  xP,H) in v]"
      using Fx_equiv_xH[OF is_propositional, THEN "E"] by simp
    then obtain F where "[(x. F,xP  xP,H) in v]"
      by (rule Instantiate)
    hence F_prop: "[x. F,xP  xP,H in v]"
      using qml_2[axiom_instance, deduction] by blast
    hence a: "[F,xP  xP,H in v]"
      using "E" by blast
    have b: "[F,yP  yP,H in v]"
      using F_prop "E" by blast
    {
      assume 1: "[xP, H & ¬yP, H in v]"
      hence "[F,xP in v]"
        using a[equiv_rl] "&E" by blast
      moreover have "[¬F,yP in v]"
        using b[THEN oth_class_taut_5_d[equiv_lr], equiv_rl] 1[conj2] by auto
      ultimately have "[F,xP & (¬F,yP) in v]"
        by (rule "&I")
      hence "[(F,xP & ¬F,yP)  (¬F,xP & F,yP) in v]"
        using "I" by blast
      hence "[¬(F,xP  F,yP) in v]"
        using oth_class_taut_5_j[equiv_rl] by blast
    }
    moreover {
      assume 1: "[¬xP, H & yP, H in v]"
      hence "[F,yP in v]"
        using b[equiv_rl] "&E" by blast
      moreover have "[¬F,xP in v]"
        using a[THEN oth_class_taut_5_d[equiv_lr], equiv_rl] 1[conj1] by auto
      ultimately have "[¬F,xP & F,yP in v]"
        using "&I" by blast
      hence "[(F,xP & ¬F,yP)  (¬F,xP & F,yP) in v]"
        using "I" by blast
      hence "[¬(F,xP  F,yP) in v]"
        using oth_class_taut_5_j[equiv_rl] by blast
    }
    ultimately have "[¬(F,xP  F,yP) in v]"
      using 2 intro_elim_4_b reductio_aa_1 by blast
    thus "[ F . ¬(F,xP  F,yP) in v]"
      by (rule existential)
  qed
      
  lemma original_paradox:
    assumes is_propositional: "(G φ. IsProperInX (λx. G,ιy. φ y x))"
    shows "False"
  proof -
    fix v
    have "[x y. A!,xP & A!,yP & x  y & (F. F,xP  F,yP) in v]"
      using aclassical2 by auto
    then obtain x where
      "[ y. A!,xP & A!,yP & x  y & (F. F,xP  F,yP) in v]"
      by (rule Instantiate)
    then obtain y where xy_def:
      "[A!,xP & A!,yP & x  y & (F. F,xP  F,yP) in v]"
      by (rule Instantiate)
    have "[ F . ¬(F,xP  F,yP) 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,xP  F,yP) in v]"
      by (rule Instantiate)
    moreover have "[F,xP  F,yP 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