# Constructive proof of Gödel's incompleteness theorem

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.

• Could we define a natural notion of bi-valued truth of arithmetical sentences over constructive mathematics? I think the classical notion of a model does not go well with constructive mathematics. Mar 4, 2020 at 12:16
• @HanulJeon The evaluation of propositional formulas to {0,1} is constructive, because all cases in the evaluation are finite, you can exhaustively compute everything. This is no longer possible with a first-order formula and an infinite domain like $\mathbb{N}$. Mar 4, 2020 at 13:05
• I have seen a work about constructive model theory (e.g. this), so answer of your first question is "yes". However, their semantic definition seems not bi-valued, so it might not be satisfactory. Mar 4, 2020 at 13:15
• Your characterization of Incompleteness 1 is not right: it's missing a critical consistency assumption (and effectiveness, which you introduce later). As soon as you add that consistency assumption, you can use Incompleteness 2, take $\Delta_T$ to be $\mathrm{Con}(T)$, which then holds provably in $\mathbb{N}$ but is not provable in $T$. Mar 4, 2020 at 13:43
• @V.Semeria Thanks. If your question comes along while studying a textbook, it's usually a good idea to let the community know which book, even if it's hard to see in advance how it could help. E.g. In this particular case, I'm planning to post an answer later, and I'd prefer to use the same definitions of $\mathrm{Con}(T)$, etc. as the book does, since some possible choices are constructively inequivalent. Mar 4, 2020 at 15:32

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.

• MLTT suits me just fine : my favorite constructive foundation is Coq. Sorry but how do we set up the notion of "sentence holding in $\mathbb{N}$" ? In all books I read so far, the function $\text{eval}_\mathbb{N}$ is the only way to do it, and it is not constructively defined. What's Tarskian paraphrasis ? Mar 4, 2020 at 17:21
• By Tarskian paraphrasis, is "phi holds in N" defined as "coq proves phi_nat", where phi_nat is a sentence in the language of Coq, ie a Prop, where all quantifications are typed in nat, and where 0 and the arithmetical operations are interpreted as their obvious Coq corresponding terms? That would keep everything syntactic, instead of evaluating formulas to 0,1. Mar 4, 2020 at 23:23
• @V.Semeria: Not quite. You could formalize "Coq proves _" inside Coq, but that's not very useful for defining satisfaction. Instead, Coq (here Agda but the defn goes the same way in Coq) defines by induction on the structure of the formula F, a proposition that means "$\mathbb{N}$ satisfies F". It's the same as the model-theoretic definition of satisfaction: translating first-order syntax into the logic of the foundational theory. E.g. if S denotes the successor relation, the formula "all x exists y S(x,y)" is satisfied in $\mathbb{N}$ precisely if every natural has a successor. Mar 5, 2020 at 9:05