Theory TAO_99_Paradox

theory TAO_99_Paradox
imports TAO_9_PLM TAO_98_ArtificialTheorems
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