Constructive proof of Gödel’s incompleteness theorem

constructive-mathematicsincompletenessmodel-theory

Gödel's first incompleteness theorem states that if a consistent theory $T$ extends Peano arithmetic, then there is an explicit formula $\Delta_T$ in the language of arithmetic, that is true in $\mathbb{N}$, but that $T$ does not prove.

An algorithm computes this formula $\Delta_T$, assuming that $T$ is recursive, so I understand how $\Delta_T$ is "explicit".

However, the proof I have that $\Delta_T$ is true in $\mathbb{N}$ is by contradiction. It starts by assuming that $\Delta_T$ is false in $\mathbb{N}$, then derives a contradiction and then concludes that $\Delta_T$ must be true in $\mathbb{N}$.

This argument would be constructively valid, if we had a constructively defined function

$$ eval_\mathbb{N} : \mathcal{L}_\text{arith} \to \{0,1\} $$

that computes whether a closed formula in the language of arithmetic is true or false in $\mathbb{N}$. Because then we would have a constructive case analysis in the finite range {0,1}.

However, the above evaluation function is usually defined recursively in a non-constructive manner. Specifically, the evaluation of a existential quantifier $\exists x, \phi(x)$ will be : if there is an $n\in\mathbb{N}$ such as the evaluation of $\phi(n)$ is 1, then $\exists x, \phi(x)$ evaluates to 1, otherwise it evaluates to 0. This is a call to the excluded middle principle, and more precisely to the limited principle of omniscience, since the question is whether a certain boolean sequence ever takes the value 1.

So is it even possible to define the notion of model of a theory constructively ? Or are those semantic methods and incompleteness theorems fundamentally classical, ie using excluded middle ?

This question came up during my study of the textbook "La théorie des ensembles", by Patrick Dehornoy (in French). Gödel's first incompleteness theorem is page 300, theorem 4.4.4, item (i) in the proof.

Best Answer

In what follows, work in your favorite foundational theory: one where it is sensible to talk about an object $\mathbb{N}$ satisfying the Peano axioms, about proofs, consistency, etc. and where you can prove the incompleteness theorems. For example Aczel's CZF, or even Martin-Löf Type Theory are suitable, constructive foundational systems.

Start with an effectively axiomatized, consistent first-order theory $T$ extending Peano Arithmetic. (What is a consistent theory? Precisely what your foundational theory proves is a consistent theory!)

Since $T$ is consistent, there is no proof of $\bot$ starting from the axioms of $T$ (this is the usual definition of consistency). But recall that, by construction, the arithmetical sentence $\mathrm{Con}(T)$ holds in $\mathbb{N}$ precisely if there does not exist an arithmetically coded proof of $\bot$ starting from the axioms of the theory $T$.

We now sketch a proof that the consistency of $T$ implies that $\mathrm{Con}(T)$ holds in $\mathbb{N}$. Assume for a contradiction that there exists an arithmetically coded proof of $\bot$ starting from the axioms of the theory $T$. Inductively* undo the arithmetic coding to produce a genuine proof of $\bot$ starting from the axioms of $T$. This contradicts the fact that $T$ is consistent, so our assumption must have been wrong, and therefore there is no arithmetically coded proof of $\bot$ starting from the axioms of the theory $T$. By definition this means that $\mathrm{Con}(T)$ holds in $\mathbb{N}$. Since we didn't invoke excluded middle or double-negation elimination anywhere, our proof is constructive.

We conclude that

  1. $T$ does not prove $\mathrm{Con}(T)$, but
  2. $\mathrm{Con}(T)$ holds in $\mathbb{N}$.

We are done. Notice that we didn't need to define anything like a computable $\mathrm{eval}_\mathbb{N}$ (which is, by the way, not possible). We did have to set up the notion of "sentence holding in a structure" to say what it means for $\mathrm{Con}(T)$ to hold in $\mathbb{N}$, but that works via the usual Tarskian paraphrasis, and does not require anything non-constructive. We also had to know that the Gödel/Rosser proofs of the incompleteness theorems (the versions not mentioning "truth") are constructive: Gödel points this out explicitly in his original papers.

edit: To answer your question in the comment below, I sketch a Tarskian definition of satisfaction in $\mathbb{N}$ using Agda notation. This one works for relational languages (which is sufficient for everything done above): the definition for languages with function symbols is a tad bit more complicated, but proceeds along similar lines. Below the type of variables, Var, is assumed to be something like $x_1,x_2,\dots$ of variables, so that you can compare them by index (but really any type with decidable equality would do). Satisfaction is defined with respect to a substitution $\sigma$ that maps free variables to their values: since sentences have no free variables, the choice of $\sigma$ does not really matter.

_[_≔_] : (Var → ℕ) → Var → ℕ → Var → ℕ
σ [ x ≔ n ] = σ' where
  σ' : Var → ℕ
  σ' y with compare y x
  σ' y | equal .x    = n
  σ' y | less _ _    = σ y
  σ' y | greater _ _ = σ y

_tarski_ : (Var → ℕ) → Formula → Set
σ tarski (atomic_equals x y) = σ x ≡ σ y
[...]
σ tarski (P ∧ Q) = (σ tarski P) × (σ tarski Q)
[...]
σ tarski (all x P) = ∀ (n : ℕ) → (σ [ x ≔ n ]) tarski P

* The exact details depend on how you defined the notion of proof. You use the fact that the length of a proof is a natural number (i.e. belongs to $\mathbb{N}$) to make the induction work, and if you defined it in a sufficiently clever way, you need not do any work at all.

Related Question