Quelle  TAO_99_Paradox.thy

theory TAO_99_Paradox
imports TAO_9_PLM TAO_98_ArtificialTheorems
begin

section‹Paradox›

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

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

subsection‹Auxiliary Lemmas›

  lemma exe_impl_exists:
    "[((\<lambda>x . \<forall> p . p \<rightarrow> p), \<iota>y . φ y x) \<equiv> (\<exists>!y . \<A>φ y x) in v]"
    proof (rule "\<equiv>I"; rule CP)
      fix φ :: "ν==>ν==>o" and x :: ν and v :: i
      assume "[((\<lambda>x . \<forall> p . p \<rightarrow> p),\<iota>y . φ y x) in v]"
      hence "[\<exists>y. \<A>φ y x & (\<forall>z. \<A>φ z x \<rightarrow> z = y)
              & ((\<lambda>x . \<forall> p . p \<rightarrow> p), y^P) in v]"
        using nec_russell_axiom[equiv_lr] SimpleExOrEnc.intros by auto
      then obtain y where
        "[\<A>φ y x & (\<forall>z. \<A>φ z x \<rightarrow> z = y)
          & ((\<lambda>x . \<forall> p . p \<rightarrow> p), y^P) in v]"
        by (rule Instantiate)
      hence "[\<A>φ y x & (\<forall>z. \<A>φ z x \<rightarrow> z = y) in v]"
        using "&E" by blast
      hence "[\<exists>y . \<A>φ y x & (\<forall>z. \<A>φ z x \<rightarrow> z = y) in v]"
        by (rule existential)
      thus "[\<exists>!y. \<A>φ y x in v]"
        unfolding exists_unique_def by simp
    next
      fix φ :: "ν==>ν==>o" and x :: ν and v :: i
      assume "[\<exists>!y. \<A>φ y x in v]"
      hence "[\<exists>y. \<A>φ y x & (\<forall>z. \<A>φ z x \<rightarrow> z = y) in v]"
        unfolding exists_unique_def by simp
      then obtain y where
        "[\<A>φ y x & (\<forall>z. \<A>φ z x \<rightarrow> z = y) in v]"
        by (rule Instantiate)
      moreover have "[((\<lambda>x . \<forall> p . p \<rightarrow> p),y^P) in v]"
        apply (rule beta_C_meta_1[equiv_rl])
          apply show_proper
        by PLM_solver
      ultimately have "[\<A>φ y x & (\<forall>z. \<A>φ z x \<rightarrow> z = y)
                        & ((\<lambda>x . \<forall> p . p \<rightarrow> p),y^P) in v]"
        using "&I" by blast
      hence "[\<exists> y . \<A>φ y x & (\<forall>z. \<A>φ z x \<rightarrow> z = y)
              & ((\<lambda>x . \<forall> p . p \<rightarrow> p),y^P) in v]"
        by (rule existential)
      thus "[((\<lambda>x . \<forall> p . p \<rightarrow> p), \<iota>y. φ y x) in v]"
        using nec_russell_axiom[equiv_rl]
          SimpleExOrEnc.intros by auto
    qed

  lemma exists_unique_actual_equiv:
    "[(\<exists>!y . \<A>(y = x & ψ (x^P))) \<equiv> \<A>ψ (x^P) in v]"
  proof (rule "\<equiv>I"; rule CP)
    fix x v
    let ?φ = "λ y x. y = x & ψ (x^P)"
    assume "[\<exists>!y. \<A>?φ y x in v]"
    hence "[\<exists>α. \<A>?φ α x & (\<forall>β. \<A>?φ β x \<rightarrow> β = α) in v]"
      unfolding exists_unique_def by simp
    then obtain α where
      "[\<A>?φ α x & (\<forall>β. \<A>?φ β x \<rightarrow> β = α) in v]"
      by (rule Instantiate)
    hence "[\<A>(α = x & ψ (x^P)) in v]"
      using "&E" by blast
    thus "[\<A>(ψ (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: "[\<A>ψ (x^P) in v]"
    have "[x = x in v]"
      using id_eq_1[where 'a=ν] by simp
    hence "[\<A>(x = x) in v]"
      using id_act_3[equiv_lr] by fast
    hence "[\<A>(x = x & ψ (x^P)) in v]"
      using 1 Act_Basic_2[equiv_rl] "&I" by blast
    hence "[\<A>?φ x x in v]"
      by simp
    moreover have "[\<forall>β. \<A>?φ β x \<rightarrow> β = x in v]"
    proof (rule "\<forall>I"; rule CP)
      fix β
      assume "[\<A>?φ β x in v]"
      hence "[\<A>(β = 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 "[\<A>?φ x x & (\<forall>β. \<A>?φ β x \<rightarrow> β = x) in v]"
      using "&I" by fast
    hence "[\<exists>α. \<A>?φ α x & (\<forall>β. \<A>?φ β x \<rightarrow> β = α) in v]"
      by (rule existential)
    thus "[\<exists>!y. \<A>?φ 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 ≡ λ ψ . \<lambda>x . ((\<lambda>x . \<forall> p . p \<rightarrow> p), \<iota>y . y = x & ψ (x^P))"
    
  lemma fake_beta:
    assumes "∧ G φ. IsProperInX (λx . (G,\<iota>y . φ y x))"
    shows "[(backdoor (λ x . ψ x), x^P) \<equiv> \<A>ψ (x^P) in v]"
  proof (rule "\<equiv>I"; rule CP)
    assume "[(backdoor ψ,x^P) in v]"
    hence "[(\<lambda>x. \<forall>p. p \<rightarrow> p,\<iota>y. y = x & ψ (x^P)) in v]"
      using beta_C_meta_1[equiv_lr, OF assms]
      unfolding backdoor_def identity_ν_def by fast
    hence "[\<exists>!y. \<A> (y = x & ψ (x^P)) in v]"
      using exe_impl_exists[equiv_lr] by fast
    thus "[\<A>ψ (x^P) in v]"
      using exists_unique_actual_equiv[equiv_lr] by blast
  next
    assume "[\<A>ψ (x^P) in v]"
    hence "[\<exists>!y. \<A> (y = x & ψ (x^P)) in v]"
      using exists_unique_actual_equiv[equiv_rl] by blast
    hence "[(\<lambda>x. \<forall>p. p \<rightarrow> p,\<iota>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,\<iota>y . φ y x))"
    shows "[(backdoor (λ x . ψ x), x^P) \<equiv> ψ (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,\<iota>y . φ y x))"
    shows "False"
  proof -
    obtain K where K_def:
      "K = backdoor (λ x . \<exists> F . {x,F} & \<not>(F,x))" by auto
    have "[\<exists>x. (A!,x^P) & (\<forall>F. {x^P,F} \<equiv> (F = K)) in dw]"
      using A_objects[axiom_instance] by fast
    then obtain x where x_prop:
      "[(A!,x^P) & (\<forall>F. {x^P,F} \<equiv> (F = K)) in dw]"
      by (rule Instantiate)
    {
      assume "[(K,x^P) in dw]"
      hence "[\<exists> F . {x^P,F} & \<not>(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} & \<not>(F,x^P) in dw]" by (rule Instantiate)
      hence "[F = K in dw]"
        using x_prop[conj2, THEN "\<forall>E"[where β=F], equiv_lr]
          "&E" unfolding K_def by blast
      hence "[\<not>(K,x^P) in dw]"
        using l_identity[axiom_instance,deduction,deduction]
             F_def[conj2] by fast
    }
    hence 1: "[\<not>(K,x^P) in dw]"
      using reductio_aa_1 by blast
    hence "[\<not>(\<exists> F . {x^P,F} & \<not>(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 "[\<forall> F . {x^P,F} \<rightarrow> (F,x^P) in dw]"
      apply - unfolding exists_def by PLM_solver
    moreover have "[{x^P,K} in dw]"
      using x_prop[conj2, THEN "\<forall>E"[where β=K], equiv_rl]
            id_eq_1 by blast
    ultimately have "[(K,x^P) in dw]"
      using "\<forall>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,\<iota>y . φ y x))"
  shows Fx_equiv_xH: "[\<forall> H . \<exists> F . \<box>(\<forall>x. (F,x^P) \<equiv> {x^P,H}) in v]"
  proof (rule "\<forall>I")
    fix H
    let ?G = "(\<lambda>x . \<forall> p . p \<rightarrow> p)"
    obtain φ where φ_def: "φ = (λ y x . (y^P) = x & {x,H})" by auto
    have "[\<exists>F. \<box>(\<forall>x. (F,x^P) \<equiv> (?G,\<iota>y . φ y (x^P))) in v]"
      using relations_1[OF assms] by simp
    hence 1: "[\<exists>F. \<box>(\<forall>x. (F,x^P) \<equiv> (\<exists>!y . \<A>φ y (x^P))) in v]"
      apply - apply (PLM_subst_method
          "λ x . (?G,\<iota>y . φ y (x^P))" "λ x . (\<exists>!y. \<A>φ y (x^P))")
      using exe_impl_exists by auto
    then obtain F where F_def: "[\<box>(\<forall>x. (F,x^P) \<equiv> (\<exists>!y . \<A>φ y (x^P))) in v]"
      by (rule Instantiate)
    moreover have 2: "∧ v x . [(\<exists>!y . \<A>φ y (x^P)) \<equiv> {x^P,H} in v]"
    proof (rule "\<equiv>I"; rule CP)
      fix x v
      assume "[\<exists>!y. \<A>φ y (x^P) in v]"
      hence "[\<exists>α. \<A>φ α (x^P) & (\<forall>β. \<A>φ β (x^P) \<rightarrow> β = α) in v]"
        unfolding exists_unique_def by simp
      then obtain α where "[\<A>φ α (x^P) & (\<forall>β. \<A>φ β (x^P) \<rightarrow> β = α) in v]"
        by (rule Instantiate)
      hence "[\<A>(α^P = x^P & {x^P,H}) in v]"
        unfolding φ_def using "&E" by blast
      hence "[\<A>({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: "[\<A>({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 "[\<A>(x = x) in v]"
        using id_act_3[equiv_lr] by fast
      hence "[\<A>(x^P = x^P & {x^P,H}) in v]"
        unfolding identity_ν_def using 1 Act_Basic_2[equiv_rl] "&I" by blast
      hence "[\<A>φ x (x^P) in v]"
        unfolding φ_def by simp
      moreover have "[\<forall>β. \<A>φ β (x^P) \<rightarrow> β = x in v]"
      proof (rule "\<forall>I"; rule CP)
        fix β
        assume "[\<A>φ β (x^P) in v]"
        hence "[\<A>(β = 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 "[\<A>φ x (x^P) & (\<forall>β. \<A>φ β (x^P) \<rightarrow> β = x) in v]"
        using "&I" by fast
      hence "[\<exists>α. \<A>φ α (x^P) & (\<forall>β. \<A>φ β (x^P) \<rightarrow> β = α) in v]"
        by (rule existential)
      thus "[\<exists>!y. \<A>φ y (x^P) in v]"
        unfolding exists_unique_def by simp
    qed
    have "[\<box>(\<forall>x. (F,x^P) \<equiv> {x^P,H}) in v]"
      apply (PLM_subst_goal_method
          "λφ . \<box>(\<forall>x. (F,x^P) \<equiv> φ x)"
          "λ x . (\<exists>!y . \<A>φ y (x^P))")
      using 2 F_def by auto
    thus "[\<exists> F . \<box>(\<forall>x. (F,x^P) \<equiv> {x^P,H}) in v]"
      by (rule existential)
  qed

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

(*<*)
end
(*>*)

end