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), 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‹
  \label{TAO_Paradox_description_backdoor}
›
    
  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

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!,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

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,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
      
  lemma original_paradox:
    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