From db7b3ec56c04e7d734ade297732703e41305cc1b Mon Sep 17 00:00:00 2001 From: SnO2WMaN Date: Sat, 2 Aug 2025 19:21:55 +0900 Subject: [PATCH 1/3] Church's Theorem wip --- Foundation.lean | 1 + .../FirstOrder/Incompleteness/Church.lean | 100 ++++++++++++++++++ 2 files changed, 101 insertions(+) create mode 100644 Foundation/FirstOrder/Incompleteness/Church.lean diff --git a/Foundation.lean b/Foundation.lean index ede69744..55668e41 100644 --- a/Foundation.lean +++ b/Foundation.lean @@ -75,6 +75,7 @@ import Foundation.FirstOrder.Incompleteness.Second import Foundation.FirstOrder.Incompleteness.Examples import Foundation.FirstOrder.Incompleteness.Tarski +import Foundation.FirstOrder.Incompleteness.Church import Foundation.FirstOrder.Hauptsatz diff --git a/Foundation/FirstOrder/Incompleteness/Church.lean b/Foundation/FirstOrder/Incompleteness/Church.lean new file mode 100644 index 00000000..162b26c9 --- /dev/null +++ b/Foundation/FirstOrder/Incompleteness/Church.lean @@ -0,0 +1,100 @@ +import Foundation.FirstOrder.Incompleteness.First + +/-! + # Church's Undecidability of First-Order Logic Theorem +-/ + + +namespace LO.ISigma1 + +open Entailment FirstOrder FirstOrder.Arithmetic + +variable {T : Theory β„’β‚’α΅£} [πˆπšΊβ‚ βͺ― T] [Entailment.Consistent T] + +lemma not_exists_provable_switch : Β¬βˆƒ Ο„ : Semisentence β„’β‚’α΅£ 1, βˆ€ Οƒ, (T ⊒!. Οƒ β†’ T ⊒!. Ο„/[βŒœΟƒβŒ]) ∧ (T ⊬. Οƒ β†’ T ⊒!. βˆΌΟ„/[βŒœΟƒβŒ]) := by + rintro βŸ¨Ο„, hΟ„βŸ©; + have ⟨h₁, hβ‚‚βŸ© := hΟ„ $ fixpoint β€œx. Β¬!Ο„ x”; + by_cases h : T ⊒!. fixpoint (βˆΌΟ„/[#0]); + . apply Entailment.Consistent.not_bot (𝓒 := T.toAxiom); + . infer_instance; + . have H₁ : T ⊒!. Ο„/[⌜fixpoint (βˆΌΟ„/[#0])⌝] := h₁ h; + have Hβ‚‚ : T ⊒!. fixpoint (βˆΌΟ„/[#0]) β­€ βˆΌΟ„/[⌜fixpoint (βˆΌΟ„/[#0])⌝] := by simpa using diagonal β€œx. Β¬!Ο„ x”; + cl_prover [h, H₁, Hβ‚‚]; + . apply h; + have H₁ : T ⊒!. βˆΌΟ„/[⌜fixpoint (βˆΌΟ„/[#0])⌝] := hβ‚‚ h; + have Hβ‚‚ : T ⊒!. fixpoint (βˆΌΟ„/[#0]) β­€ βˆΌΟ„/[⌜fixpoint (βˆΌΟ„/[#0])⌝] := by simpa using diagonal β€œx. Β¬!Ο„ x”; + cl_prover [H₁, Hβ‚‚]; + +end LO.ISigma1 + + +namespace LO.FirstOrder + +open LO.Entailment +open ISigma1 FirstOrder FirstOrder.Arithmetic + +section + +variable {L : Language} {T : Theory L} {Οƒ : Sentence L} + +@[simp] lemma Theory.eq_empty_toAxiom_empty : (βˆ… : Theory L).toAxiom = βˆ… := by simp [Theory.toAxiom]; + +noncomputable def Theory.finite_conjunection (T_finite : T.Finite) : Sentence L := + letI A := T.toAxiom; + haveI A_finite : A.Finite := by apply Set.Finite.image; simpa; + A_finite.toFinset.conj + +lemma iff_axiomProvable_empty_context_provable {A : Axiom L} : A ⊒! Οƒ ↔ A *⊒[(βˆ… : Axiom L)]! Οƒ := by + constructor; + . intro h; + sorry; + . intro h; + sorry; + +lemma iff_provableβ‚€_empty_context_provable : T ⊒!. Οƒ ↔ (T.toAxiom) *⊒[(βˆ… : Theory L).toAxiom]! Οƒ := by + apply Iff.trans iff_axiomProvable_empty_context_provable; + simp; + +variable [DecidableEq (Sentence L)] + +lemma firstorder_provable_of_finite_provable (T_finite : T.Finite) : T ⊒!. Οƒ ↔ βˆ… ⊒!. (Theory.finite_conjunection T_finite) ➝ Οƒ := by + apply Iff.trans ?_ FConj_DT.symm; + apply Iff.trans iff_provableβ‚€_empty_context_provable; + simp; + +end + +namespace Arithmetic + +variable {T : ArithmeticTheory} [πˆπšΊβ‚ βͺ― T] [Entailment.Consistent T] [T.SoundOnHierarchy 𝚺 1] +variable {Οƒ : Sentence _} + +lemma not_RePred_theorems : Β¬REPred (fun n : β„• ↦ βˆƒ Οƒ : Sentence β„’β‚’α΅£, n = βŒœΟƒβŒ ∧ T ⊒!. Οƒ) := by + have := ISigma1.not_exists_provable_switch (T := T); + contrapose! this; + use codeOfREPred (Ξ» n : β„• ↦ βˆƒ Οƒ : Sentence β„’β‚’α΅£, n = βŒœΟƒβŒ ∧ T ⊒!. Οƒ); + intro Οƒ; + constructor; + . intro hΟƒ; + simpa using re_complete (T := T) this (x := βŒœΟƒβŒ) |>.mp $ by use Οƒ; + . sorry; + +lemma firstorder_undecidability_of_finite_theory + (T_finite : T.Finite) + : Β¬REPred (fun n : β„• ↦ βˆƒ Οƒ : Sentence β„’β‚’α΅£, n = βŒœΟƒβŒ ∧ βˆ… ⊒!. Οƒ) := by + by_contra h; + apply not_RePred_theorems (T := T); + replace h : REPred (fun n : β„• ↦ βˆƒ Οƒ : Sentence β„’β‚’α΅£, n = βŒœΟƒβŒ ∧ βˆ… ⊒!. (Theory.finite_conjunection T_finite) ➝ Οƒ) := by + sorry; + have := funext + (f := fun n : β„• ↦ βˆƒ Οƒ : Sentence β„’β‚’α΅£, n = βŒœΟƒβŒ ∧ βˆ… ⊒!. (Theory.finite_conjunection T_finite) ➝ Οƒ) + (g := fun n ↦ βˆƒ Οƒ, n = βŒœΟƒβŒ ∧ T ⊒!. Οƒ) + $ by simp [firstorder_provable_of_finite_provable T_finite]; + rwa [this] at h; + +lemma firstorder_undecidability : Β¬REPred (fun n : β„• ↦ βˆƒ Οƒ : Sentence β„’β‚’α΅£, n = βŒœΟƒβŒ ∧ βˆ… ⊒!. Οƒ) := by + apply @firstorder_undecidability_of_finite_theory (T := 𝐏𝐀⁻) (by sorry) inferInstance (by sorry) (by simp); + +end Arithmetic + +end LO.FirstOrder From 48da9bb2dfddfd934a6a2035246891d98b2f8258 Mon Sep 17 00:00:00 2001 From: SnO2WMaN Date: Mon, 4 Aug 2025 10:18:25 +0900 Subject: [PATCH 2/3] wip --- .../FirstOrder/Incompleteness/Church.lean | 34 ++++++++----------- 1 file changed, 15 insertions(+), 19 deletions(-) diff --git a/Foundation/FirstOrder/Incompleteness/Church.lean b/Foundation/FirstOrder/Incompleteness/Church.lean index 162b26c9..2a6caae7 100644 --- a/Foundation/FirstOrder/Incompleteness/Church.lean +++ b/Foundation/FirstOrder/Incompleteness/Church.lean @@ -1,4 +1,5 @@ import Foundation.FirstOrder.Incompleteness.First +import Mathlib.Computability.Reduce /-! # Church's Undecidability of First-Order Logic Theorem @@ -11,7 +12,7 @@ open Entailment FirstOrder FirstOrder.Arithmetic variable {T : Theory β„’β‚’α΅£} [πˆπšΊβ‚ βͺ― T] [Entailment.Consistent T] -lemma not_exists_provable_switch : Β¬βˆƒ Ο„ : Semisentence β„’β‚’α΅£ 1, βˆ€ Οƒ, (T ⊒!. Οƒ β†’ T ⊒!. Ο„/[βŒœΟƒβŒ]) ∧ (T ⊬. Οƒ β†’ T ⊒!. βˆΌΟ„/[βŒœΟƒβŒ]) := by +lemma not_exists_theorem_representable_predicate : Β¬βˆƒ Ο„ : Semisentence β„’β‚’α΅£ 1, βˆ€ Οƒ, (T ⊒!. Οƒ β†’ T ⊒!. Ο„/[βŒœΟƒβŒ]) ∧ (T ⊬. Οƒ β†’ T ⊒!. βˆΌΟ„/[βŒœΟƒβŒ]) := by rintro βŸ¨Ο„, hΟ„βŸ©; have ⟨h₁, hβ‚‚βŸ© := hΟ„ $ fixpoint β€œx. Β¬!Ο„ x”; by_cases h : T ⊒!. fixpoint (βˆΌΟ„/[#0]); @@ -69,31 +70,26 @@ namespace Arithmetic variable {T : ArithmeticTheory} [πˆπšΊβ‚ βͺ― T] [Entailment.Consistent T] [T.SoundOnHierarchy 𝚺 1] variable {Οƒ : Sentence _} -lemma not_RePred_theorems : Β¬REPred (fun n : β„• ↦ βˆƒ Οƒ : Sentence β„’β‚’α΅£, n = βŒœΟƒβŒ ∧ T ⊒!. Οƒ) := by - have := ISigma1.not_exists_provable_switch (T := T); +open Classical in +/-- Godel number of theorems of `T` is not computable. -/ +theorem not_computable_theorems : Β¬ComputablePred (fun n : β„• ↦ βˆƒ Οƒ : Sentence β„’β‚’α΅£, n = βŒœΟƒβŒ ∧ T ⊒!. Οƒ) := by + have := ISigma1.not_exists_theorem_representable_predicate (T := T); contrapose! this; + -- TODO: applying `ComputablePred fun n ↦ βˆƒ Οƒ, n = βŒœΟƒβŒ ∧ T ⊒!. Οƒ` to Representation theorem. + have ⟨h₁, hβ‚‚βŸ© := ComputablePred.computable_iff_re_compl_re.mp this; use codeOfREPred (Ξ» n : β„• ↦ βˆƒ Οƒ : Sentence β„’β‚’α΅£, n = βŒœΟƒβŒ ∧ T ⊒!. Οƒ); intro Οƒ; constructor; . intro hΟƒ; - simpa using re_complete (T := T) this (x := βŒœΟƒβŒ) |>.mp $ by use Οƒ; + simpa using re_complete h₁ (x := βŒœΟƒβŒ) |>.mp βŸ¨Οƒ, by tauto⟩; . sorry; -lemma firstorder_undecidability_of_finite_theory - (T_finite : T.Finite) - : Β¬REPred (fun n : β„• ↦ βˆƒ Οƒ : Sentence β„’β‚’α΅£, n = βŒœΟƒβŒ ∧ βˆ… ⊒!. Οƒ) := by - by_contra h; - apply not_RePred_theorems (T := T); - replace h : REPred (fun n : β„• ↦ βˆƒ Οƒ : Sentence β„’β‚’α΅£, n = βŒœΟƒβŒ ∧ βˆ… ⊒!. (Theory.finite_conjunection T_finite) ➝ Οƒ) := by - sorry; - have := funext - (f := fun n : β„• ↦ βˆƒ Οƒ : Sentence β„’β‚’α΅£, n = βŒœΟƒβŒ ∧ βˆ… ⊒!. (Theory.finite_conjunection T_finite) ➝ Οƒ) - (g := fun n ↦ βˆƒ Οƒ, n = βŒœΟƒβŒ ∧ T ⊒!. Οƒ) - $ by simp [firstorder_provable_of_finite_provable T_finite]; - rwa [this] at h; - -lemma firstorder_undecidability : Β¬REPred (fun n : β„• ↦ βˆƒ Οƒ : Sentence β„’β‚’α΅£, n = βŒœΟƒβŒ ∧ βˆ… ⊒!. Οƒ) := by - apply @firstorder_undecidability_of_finite_theory (T := 𝐏𝐀⁻) (by sorry) inferInstance (by sorry) (by simp); +open Classical in +/-- Godel number of theorems of first-order logic on `β„’β‚’α΅£` is not computable. -/ +theorem firstorder_undecidability : Β¬ComputablePred (fun n : β„• ↦ βˆƒ Οƒ : Sentence β„’β‚’α΅£, n = βŒœΟƒβŒ ∧ βˆ… ⊒!. Οƒ) := by + by_contra h; + apply @not_computable_theorems (T := 𝐏𝐀⁻) (by sorry) inferInstance inferInstance; + sorry; end Arithmetic From baed7e775c6ae407cb3dba9b4dfe1d28022d1155 Mon Sep 17 00:00:00 2001 From: SnO2WMaN Date: Mon, 4 Aug 2025 13:20:50 +0900 Subject: [PATCH 3/3] wip (2) --- .../FirstOrder/Incompleteness/Church.lean | 32 +++++++++++++------ 1 file changed, 22 insertions(+), 10 deletions(-) diff --git a/Foundation/FirstOrder/Incompleteness/Church.lean b/Foundation/FirstOrder/Incompleteness/Church.lean index 2a6caae7..735c14cc 100644 --- a/Foundation/FirstOrder/Incompleteness/Church.lean +++ b/Foundation/FirstOrder/Incompleteness/Church.lean @@ -6,6 +6,21 @@ import Mathlib.Computability.Reduce -/ +section + +variable {Ξ± Ξ²} [Primcodable Ξ±] [Primcodable Ξ²] + +lemma ComputablePred.range_subset {f : Ξ± β†’ Ξ²} (hf : Computable f) {A} (hA : ComputablePred A) : ComputablePred { x | A (f x) } := by + apply computable_iff.mpr; + obtain ⟨inA, hinA₁, rfl⟩ := computable_iff.mp hA; + use Ξ» x => inA (f x); + constructor; + . apply Computable.comp <;> assumption; + . rfl; + +end + + namespace LO.ISigma1 open Entailment FirstOrder FirstOrder.Arithmetic @@ -73,16 +88,13 @@ variable {Οƒ : Sentence _} open Classical in /-- Godel number of theorems of `T` is not computable. -/ theorem not_computable_theorems : Β¬ComputablePred (fun n : β„• ↦ βˆƒ Οƒ : Sentence β„’β‚’α΅£, n = βŒœΟƒβŒ ∧ T ⊒!. Οƒ) := by - have := ISigma1.not_exists_theorem_representable_predicate (T := T); - contrapose! this; - -- TODO: applying `ComputablePred fun n ↦ βˆƒ Οƒ, n = βŒœΟƒβŒ ∧ T ⊒!. Οƒ` to Representation theorem. - have ⟨h₁, hβ‚‚βŸ© := ComputablePred.computable_iff_re_compl_re.mp this; - use codeOfREPred (Ξ» n : β„• ↦ βˆƒ Οƒ : Sentence β„’β‚’α΅£, n = βŒœΟƒβŒ ∧ T ⊒!. Οƒ); - intro Οƒ; - constructor; - . intro hΟƒ; - simpa using re_complete h₁ (x := βŒœΟƒβŒ) |>.mp βŸ¨Οƒ, by tauto⟩; - . sorry; + by_contra hC; + let D : β„• β†’ Prop := fun n : β„• ↦ βˆƒ Οƒ : Semisentence β„’β‚’α΅£ 1, n = βŒœΟƒβŒ ∧ T ⊬. Οƒ/[βŒœΟƒβŒ]; + have : ComputablePred D := by + let f : β„• β†’ β„• := Ξ» n => if h : βˆƒ Οƒ : Semisentence β„’β‚’α΅£ 1, n = βŒœΟƒβŒ then ⌜(h.choose/[⌜h.choose⌝] : Sentence β„’β‚’α΅£)⌝ else 0; + have : ComputablePred (Ξ» x => Β¬βˆƒ Οƒ, f x = βŒœΟƒβŒ ∧ T ⊒!. Οƒ) := ComputablePred.range_subset (f := f) (by sorry) (ComputablePred.not hC); + sorry; + simpa [D] using re_complete (T := T) (ComputablePred.to_re this) (x := ⌜(codeOfREPred D)⌝); open Classical in /-- Godel number of theorems of first-order logic on `β„’β‚’α΅£` is not computable. -/