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