G1

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)

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 ⊬ ↑𝗖𝗼𝗻