Gödel's Incompleteness Theorem

Stream: maths

[Palalansoukî]

Last year, I completed a formal proof of Gödel's first incompleteness theorem, and this time, I have finished formalizing the proof of second incompleteness theorem. I proved that a theory $T$, which is stronger than $\mathsf{I}\Sigma_1$​, $\Delta_1$-definable, and has $\mathbb{N}$ as a model, cannot prove or disprove a statement asserting its own consistency:

theorem goedel_second_incompleteness [𝐈𝚺₁ ≼ T] [T.Delta1Definable] [System.Consistent T] :
    T ⊬ ↑𝗖𝗼𝗻

theorem consistent_undecidable [𝐈𝚺₁ ≼ T] [T.Delta1Definable] [ℕ ⊧ₘ* T] :
    System.Undecidable T ↑𝗖𝗼𝗻

• goedel_second_incompleteness
• consistent_undecidable

The formal proof of G2 has already been done using Isabelle, but my result is stronger. The result in Isabelle is based on the theory of hereditary finite sets ($\mathsf{HF}$), which is equivalent to Peano arithmetic, but I proved it for a weaker theory, $\mathsf{I}\Sigma_1$. This is likely the first formalization.

I also showed a stronger result on the first incompleteness theorem than before, proving the incompleteness of Cobham's $\mathsf{R}_0$. $\mathsf{R}_0$ is a theory of arithmetic weaker than Robinson's $\mathsf{Q}$, known as the weakest theory where essential incompleteness holds. This is also likely the first formalization of this.

theorem goedel_first_incompleteness [𝐑₀ ≼ T] [T.Delta1Definable] [Sigma1Sound T] :
    ¬System.Complete T

• goedel_first_incompleteness

In addition, there are several important theorems as byproducts, which I hope to include in mathlib in the future.

• The exponential function's graph can be expressed by a $\Sigma_0$-formula of arithmetic.
• $\mathbf{RE} = \mathbf{\Sigma_1}​$.

There are a few things to note. First, the definition of the arithmetical hierarchy differs slightly from the standard one. Typically, $\Sigma_n$/$\Pi_n$-formula is defined as a formula with quantifiers alternating $n$ times starting with $\exists$/$\forall$, but in my formalization, $\Sigma_n$/$\Pi_n$​ is defined as those closed by $\land$/$\lor$/bounded quantifiers. However, since it is known that $\mathsf{I}\Sigma_n \vdash \mathsf{I}\Sigma_0(\Sigma_n)$, there is no issue in terms of the provability strength of $\mathsf{I}\Sigma_n$.

Also, I adopted Tait-calculus as a proof system. Tait-calculus has fewer inference rules, making the formalization easier to handle, but the formulas themselves must satisfy the De Morgan rules. Because of this, it is not directly compatible with ModelTheory in mathlib.

[Adam Topaz]

Congratulations! This is really great!

[Aaron Anderson]

Just checking what you mean by saying "the formulas themselves must satisfy the De Morgan rules" - do you mean that you're requiring that not/neg isn't part of the inductive definition?

[Palalansoukî]

That's right. Formulas are defined as

$A | B | R(\vec{v}) | \overline{R}(\vec{v}) | \top | \bot | A \land B | A \lor B | \forall A | \exists A$

and negation is defined inductively.

$\lnot R(\vec{v}) \coloneqq \overline{R}(\vec{v})$
$\lnot\overline{R}(\vec{v}) \coloneqq R(\vec{v})$
$\lnot\top \coloneqq \bot$
$\lnot\bot \coloneqq \top$
$\lnot(A \land B) \coloneqq \lnot A \lor \lnot B$
$\lnot(A \lor B) \coloneqq \lnot A \land \lnot B$
$\lnot\forall A \coloneqq \exists \lnot A$
$\lnot\exists A \coloneqq \forall \lnot A$

Also in ModelTheory the equality symbol is always included in the atomic formula, but not in my formalization. However, it would be possible to define appropriate translations between each other.

[David Michael Roberts]

Cool! Could you say what the language and axioms for R_0 are in the usual mathematical vernacular? I guess this is the formal definition: https://github.com/FormalizedFormalLogic/Foundation/blob/41ecee31d573798ea47f005189841c76041090b5/Logic/FirstOrder/Arith/Theory.lean#L21-L26

I think I'm most mystified by leastNumber...

[Palalansoukî]

In my formalization, Language of $\mathsf{R}_0$ is $\mathcal{L}_\mathrm{OR} \coloneqq \{0, 1, +, \cdot, =, <\}$, and $\mathsf{R}_0$ consists of axioms of equality and following infinite axioms.
$\Omega_1: \overline{n} + \overline{m} = \overline{n + m}$ for all $n, m \in \mathbb{N}$
$\Omega_2: \overline{n} \cdot \overline{m} = \overline{n m}$ for all $n, m \in \mathbb{N}$
$\Omega_3: \overline{n} \neq \overline{m}$ for all $n, m \in \mathbb{N}$, such that $n \ne m$
$\Omega_4: (\forall x)[x < \overline{n} \leftrightarrow x = \overline{0} \lor x = \overline{1} \lor \cdots \lor x = \overline{n - 1}]$ for all $n \in \mathbb{N}$
$\overline{n}$ is a numeral of $n$, defined as
$\overline{n} \coloneqq \begin{cases} \underbrace{1 + \cdots + 1}_{n} & \text{if } n \ne 0 \\ 0 & \text{if } n = 0\end{cases}$

leastNumber is the least number principle $\mathsf{L}\varphi$, but it is just defined and not used.

[Nir Paz]

This is really cool!
Could you explain why the exponential function's graph is sigma 0? I can't figure it out

[Palalansoukî]

Technically, the proof is quite complex. The core of the proof is to use the definition of exponential ($2^x$) by prefix induction used by Buss.

$2^0 := 1 \\ 2^{2n} := 2^n \cdot 2^n \\ 2^{2n + 1} := 2 \cdot 2^n \cdot 2^n$

The proof can be found in Logical Foundations of Proof Complexity by Cook & Nguyen or Metamathematics of First-Order Arithmetic by Hajek & Pudlak.

[Palalansoukî]

I opened a PR to update the Freek's list. #16968