From 5cdd3b6098b5ad3bb240e6f0e40007beb96172e4 Mon Sep 17 00:00:00 2001 From: palalansouki Date: Sun, 15 Sep 2024 01:55:52 +0900 Subject: [PATCH] G1 --- src/first_order/goedel1.md | 121 ++++++++++--------------------------- src/first_order/goedel2.md | 3 +- 2 files changed, 33 insertions(+), 91 deletions(-) diff --git a/src/first_order/goedel1.md b/src/first_order/goedel1.md index 5a22107..3990640 100644 --- a/src/first_order/goedel1.md +++ b/src/first_order/goedel1.md @@ -13,102 +13,43 @@ def LO.System.Complete : Prop := ∀ f, 𝓢 ⊢! f ∨ 𝓢 ⊢! ~f ## Theorem -$\Sigma_1$-sound and computable first-order theory, which is stronger than $\mathsf{PA}^-$, is incomplete. +Let $T$ be a $\Delta_1$-definable arithmetic theory, stronger than $\mathsf{R}_0$ and $\Sigma_1$-sound. -```lean -theorem LO.FirstOrder.Arith.first_incompleteness - (T : LO.FirstOrder.Theory ℒₒᵣ) - [DecidablePred T] - [𝐄𝐐 ≼ T] - [𝐏𝐀⁻ ≼ T] - [LO.FirstOrder.Arith.SigmaOneSound T] - [LO.FirstOrder.Theory.Computable T] : - ¬LO.System.Complete T -``` - -This theorem is proved two distinct approach. - -- [G1 in `FirstIncompleteness.lean`](https://formalizedformallogic.github.io/Foundation/docs/Logic/FirstOrder/Incompleteness/FirstIncompleteness.html#LO.FirstOrder.Arith.first_incompleteness) -- [G1 in `SelfReference.lean`](https://formalizedformallogic.github.io/Foundation/docs/Logic/FirstOrder/Incompleteness/SelfReference.html#LO.FirstOrder.Arith.FirstIncompletenessBySelfReference.not_complete) - -`FirstIncompleteness.lean` is computability theoretic proof, while `SelfReference.lean` uses a well-known self-referential argument. - -### G1 in `FirstIncompleteness.lean` - -Define a set of formulae with one variable. -$$ D \coloneqq \{\varphi \mid T \vdash \lnot \varphi({\ulcorner \varphi \urcorner}) \} $$ - $D$ is r.e. since $T$ is computable. (one could use Craig's trick to weaken this condition to r.e., but I will not do that here.) - -By the representation theorem, there exists a $\Sigma_1$ formula $\rho(x)$ that represents $D$. i.e., - -$$ T \vdash \rho({\ulcorner \varphi \urcorner}) \iff T \vdash \lnot \varphi({\ulcorner \varphi \urcorner})$$ - -Let $\gamma := \rho({\ulcorner \rho \urcorner})$. The next follows immediately. - -$$ T \vdash \gamma \iff T \vdash \lnot \gamma $$ - -Thus, as $T$ is consistent, $\gamma$ is undecidable from $T$. +### Representeation Theorem -### G1 in `SelfReference.lean` +#### Theorem: Let $S$ be a r.e. set. Then, there exists a formula $\varphi_S(x)$ such that $n \in S \iff T \vdash \varphi_S(\overline{n})$ for all $n \in \mathbb{N}$. -Since the substitution of a formula is computable, there exists an $\Sigma_1$ formula $\mathrm{ssbs}(x, y, z)$ that represents this: - -$$ -T \vdash (\forall x)[\mathrm{ssbs}(x, {\ulcorner \varphi \urcorner}, {\ulcorner \psi \urcorner}) - \leftrightarrow x = {\ulcorner \varphi({\ulcorner \psi \urcorner}) \urcorner}] -$$ - -Define a sentence $\mathrm{fixpoint}_\theta$ for formula (with one variable) $\theta$ as follows. +```lean +lemma re_complete + [𝐑₀ ≼ T] [Sigma1Sound T] + {p : ℕ → Prop} (hp : RePred p) {x : ℕ} : + p x ↔ T ⊢! ↑((codeOfRePred p)/[‘↑x’] : Sentence ℒₒᵣ) +``` +- [re_complete](https://formalizedformallogic.github.io/Incompleteness/docs/Logic/FirstOrder/Arith/Representation.html#LO.FirstOrder.Arith.re_complete) -$$ - \begin{align*} - \mathrm{fixpoint}_\theta - &\coloneqq \mathrm{diag}_\theta(\ulcorner \mathrm{diag}_\theta \urcorner) \\ - \mathrm{diag}_\theta(x) - &\coloneqq (\forall y)[\mathrm{ssbs}(y, x, x) \to \theta (y)] - \end{align*} -$$ +### Main Theorem -#### Fixpoint Lemma: $T \vdash \mathrm{fixpoint}_\theta \leftrightarrow \theta({\ulcorner \mathrm{fixpoint}_\theta \urcorner})$ +#### Theorem: $\Sigma_1$-sound and $\Delta_1$-definable first-order theory, which is stronger than $\mathsf{R_0}$, is incomplete. - _Proof._ - $$ - \begin{align*} - \mathrm{fixpoint}_\theta - &\equiv - (\forall x)[ - \mathrm{ssbs}( - x, - {\ulcorner \mathrm{diag}_\theta \urcorner}, - {\ulcorner \mathrm{diag}_\theta \urcorner}) \to - \theta (x) - ] \\ - &\leftrightarrow - \theta(\ulcorner \mathrm{diag}_\theta(\ulcorner \mathrm{diag}_\theta \urcorner) \urcorner) \\ - &\equiv - \theta(\ulcorner \mathrm{fixpoint}_\theta \urcorner) - \end{align*} - $$ - ∎ - -Let $G := \mathrm{fixpoint}_{\lnot\mathrm{prov_T}(x)}$ (Gödel sentence; the sentence that states "This sentence is not provable"), -where $\mathrm{prov}_T(x)$ is a formula represents provability. - -Since $G$ is undecidable, this results in the incompleteness of $T$. -- Assume that $T \vdash G$. $T \vdash \lnot \mathrm{prov}_T(\ulcorner G \urcorner)$ follows from the fixpoint lemma, - while $T \vdash \mathrm{prov}_T(\ulcorner G \urcorner)$ follows from the hypothesis. a contradiction. -- Assume that $T \vdash \lnot G$. $T \vdash \mathrm{prov}_T(\ulcorner G \urcorner)$ follows from the fixpoint lemma, - and $T \vdash G$ follows. a contradiction. + Define a set of formulae with one variable. + $$ D \coloneqq \{\varphi \mid T \vdash \lnot \varphi({\ulcorner \varphi \urcorner}) \} $$ + $D$ is r.e. since $T$ is $\Delta_1$-definable. (one could use Craig's trick to weaken this condition to $\Sigma_1$, but I will not do that here.) + + By the representation theorem, there exists a $\Sigma_1$ formula $\rho(x)$ that represents $D$. i.e., + + $$ T \vdash \rho({\ulcorner \varphi \urcorner}) \iff T \vdash \lnot \varphi({\ulcorner \varphi \urcorner})$$ + + Let $\gamma := \rho({\ulcorner \rho \urcorner})$. The next follows immediately. + + $$ T \vdash \gamma \iff T \vdash \lnot \gamma $$ + + Thus, as $T$ is consistent, $\gamma$ is undecidable from $T$. ∎ -## About Second Theorem - -To prove the second incompleteness theorem, as outlined in Gödel's original paper, one can derive it by proving the first incompleteness theorem again within arithmetic. -Although this fact has not yet been formalized in this project. -These efforts are being undertaken in a separated repository [iehality/Arithmetization](https://github.com/iehality/Arithmetization). - -Notably, the formalization of the second incompleteness theorem has already been accomplished by L. C. Paulson in Isabelle. -However, owing to the technical simplicity for coding and others. this formalization is on _hereditarily finite sets_ and not on arithmetic. - -- [L. C. Paulson, "A machine-assisted proof of Gödel's incompleteness theorems for the theory of hereditarily finite sets"](https://www.repository.cam.ac.uk/items/bda52431-26e0-4e86-8d63-409bcedd4617) -- [Isabelle AFP](https://www.isa-afp.org/entries/Incompleteness.html) +```lean +theorem goedel_first_incompleteness + (T : Theory ℒₒᵣ) [𝐑₀ ≼ T] [Sigma1Sound T] [T.Delta1Definable] : + ¬System.Complete T +``` +- [goedel_first_incompleteness](https://formalizedformallogic.github.io/Incompleteness/docs/Incompleteness/Arith/First.html#LO.FirstOrder.Arith.goedel_first_incompleteness) \ No newline at end of file diff --git a/src/first_order/goedel2.md b/src/first_order/goedel2.md index ab9e217..393448b 100644 --- a/src/first_order/goedel2.md +++ b/src/first_order/goedel2.md @@ -224,6 +224,7 @@ $$ \theta(\ulcorner \mathrm{fixpoint}_\theta \urcorner) \end{align*} $$ + ∎ ```lean theorem LO.FirstOrder.Arith.diagonal (θ : Semisentence ℒₒᵣ 1) : @@ -258,7 +259,7 @@ lemma consistent_iff_goedel [𝐈𝚺₁ ≼ T] [T.Delta1Definable] : T ⊢! ↑ ``` - [consistent_iff_goedel](https://formalizedformallogic.github.io/Incompleteness/docs/Incompleteness/Arith/Second.html#LO.FirstOrder.Arith.consistent_iff_goedel) -#### Gödel's Second Incompleteness Theorem: $T$ cannot prove its own consistency, i.e., $T \nvdash \mathrm{Con}_T$ if $T$ is consistent. Moreover, $\mathrm{Con}_T$ is undecidable from $T$ if $\mathbb{N} \models T$. +#### Theorem: $T$ cannot prove its own consistency, i.e., $T \nvdash \mathrm{Con}_T$ if $T$ is consistent. Moreover, $\mathrm{Con}_T$ is undecidable from $T$ if $\mathbb{N} \models T$. ```lean theorem goedel_second_incompleteness [𝐈𝚺₁ ≼ T] [T.Delta1Definable] [System.Consistent T] : T ⊬ ↑𝗖𝗼𝗻