Symptom

The proof assistant is failing you. You are trying to verify a piece of concurrent code in Coq or Lean, and the tool will not accept your termination argument. A colleague says, without much conviction, “well, Gödel — you can’t prove everything anyway.”

That sentence is almost always wrong in context, and it is the most commonly misapplied result in mathematics. It has been used to argue that human minds exceed computers, that formal verification is pointless, that AI is impossible, that no software can ever be proved correct, and that mathematics is arbitrary. None of these follow.

But the theorem does have real engineering content, and it is much more specific and much sharper than the folklore. The second theorem in particular is a hard constraint on the verification stack — it says something concrete about what your proof assistant can and cannot say about itself, and it is the reason Coq’s kernel cannot prove its own soundness. That is worth understanding precisely, because the precise version is useful and the vague version is only ever used to excuse giving up.

Statement

First incompleteness theorem. Any consistent formal system $F$ that is effectively axiomatizable and strong enough to express elementary arithmetic contains a sentence $G_F$ that is true but neither provable nor refutable in $F$.

Second incompleteness theorem. For such an $F$, the sentence $\mathrm{Con}(F)$ expressing $F$’s own consistency is not provable in $F$, unless $F$ is inconsistent.

The three hypotheses are all load-bearing, and every misreading drops one:

  • Effectively axiomatizable. The axioms must be recognizable by an algorithm. Drop this and “the set of all true arithmetic statements” is a complete theory — useless, because you cannot check whether something is an axiom.
  • Strong enough for arithmetic. Specifically, capable of representing primitive recursive functions. Weaker systems escape entirely.
  • Consistent. An inconsistent system proves everything, including its own consistency, which is precisely why the second theorem’s converse is worthless as reassurance.

The second theorem is the one with teeth. The first says there is a weird sentence you cannot settle; you can shrug and add it as an axiom. The second says the one thing you most want to prove about your system — that it does not prove false things — is exactly the thing it cannot prove.

Argument

Step one: arithmetization. Assign a number to every symbol, then to every formula (as a sequence of symbols), then to every proof (as a sequence of formulas), using prime factorization or any injective encoding. This is Gödel numbering, and it is the same idea as T013’s machine encoding: syntax is data, and data is numbers. It is 1931, so this is the first appearance of the idea that would become the stored-program computer.

Step two: provability becomes arithmetic. Because the axioms are algorithmically recognizable and proof-checking is mechanical, the relation “$p$ encodes a proof of the formula encoded by $f$” is a primitive recursive relation on numbers, hence expressible inside the system as a formula $\mathrm{Prf}(p, f)$. The system can now talk about its own proofs, in the only language it has: arithmetic. This step is the hard technical labour of the paper and it is what everyone skips.

Step three: the diagonal lemma. For any formula $\psi(x)$ with one free variable, there is a sentence $\sigma$ with $F \vdash \sigma \leftrightarrow \psi(\ulcorner\sigma\urcorner)$. The construction is the same self-application as Kleene’s recursion theorem (T014): build a formula that, applied to its own number, produces itself. Apply this to $\psi(x) = \neg\exists p, \mathrm{Prf}(p, x)$ and you get $G$, a sentence equivalent to “there is no proof of me.”

Step four. If $F \vdash G$, then there is a proof of $G$, so $\neg G$ is provable too, and $F$ is inconsistent. If $F \vdash \neg G$, then $F$ proves there is a proof of $G$; with consistency (Rosser’s refinement removes the need for the stronger $\omega$-consistency Gödel originally assumed) this also collapses. So neither is provable. And since $G$ is unprovable, what $G$ asserts is the case — $G$ is true in the standard model, and unprovable in $F$.

Step five: the second theorem, which is the good one. The argument of step four is itself elementary and arithmetizable. Formalize “if $F$ is consistent then $G$ is unprovable” inside $F$: you get $F \vdash \mathrm{Con}(F) \to G$. If $F$ could prove $\mathrm{Con}(F)$, it could prove $G$, which step four forbids. Hence $F \nvdash \mathrm{Con}(F)$. The elegance is that the second theorem needs no new construction, only the observation that the first proof can be carried out inside the system.

The relationship to the halting problem. T010 is the same theorem in computational dress, and each gives a proof of the other. If provability were decidable you could decide halting by asking for a proof that a machine halts; conversely, the set of provable sentences is recursively enumerable while the set of true arithmetic sentences is not, so they cannot coincide. Gödel came first by five years, which is why this post is placed as the prehistory of Part II rather than a corollary of it. Turing’s contribution was to make the diagonalization mechanical, and that is what made it engineering.

Forbids

A single formal system settling all mathematical questions. Hilbert’s programme, as originally stated, is dead. There is no algorithmic axiom set from which every arithmetic truth follows.

A system proving its own consistency. If your proof checker verifies a proof of its own soundness, you have found a bug or an inconsistency, not a reassurance. This is a real design constraint: Coq’s soundness is proved in a metatheory strictly stronger than Coq (typically ZFC plus inaccessible cardinals), and that regress does not terminate.

A complete, sound, effective decision procedure for arithmetic. No tool will ever decide arbitrary statements about integers. Every SMT solver’s integer arithmetic is either incomplete or restricted to a decidable fragment, and this is why.

Escaping by adding $G$ as an axiom. The new system $F + G$ is still effectively axiomatizable and still arithmetic, so it has its own $G’$. The process never terminates, and transfinite iteration (Turing’s ordinal logics) just relocates the problem into naming ordinals.

Does not forbid

It does not say your program cannot be verified, and this is the misreading that costs money. seL4 is a fully verified microkernel with a machine-checked proof of functional correctness. CompCert is a verified C compiler. The CakeML compiler is verified down to machine code. Incompleteness concerns sentences constructed by diagonalization; it says nothing about whether your concrete specification is provable, and empirically the answer is usually yes. The obstacle in practice is always effort, never Gödel.

It does not say humans out-perform machines. The Lucas–Penrose argument claims we “see” $G$ is true while machines cannot. But we see it only given consistency of $F$ — and any formal system can also prove $\mathrm{Con}(F) \to G$. The human is doing exactly the inference the machine can do, and the claim that humans know their own consistency is unsupported and probably false.

It does not apply to systems too weak for arithmetic, and lots of useful systems are. Presburger arithmetic (addition, no multiplication) is complete and decidable, and is what array-bounds and loop-dependence analyses actually use. The theory of real closed fields is decidable (Tarski), which is why geometric solvers work. Propositional logic is decidable. Weakness is a feature, and this is the same trade as T012’s total languages and T038’s parser levels.

It does not make consistency unknowable. Gentzen proved the consistency of Peano arithmetic in 1936 using transfinite induction up to $\varepsilon_0$. That is a real proof; it just uses a principle PA does not have. The theorem forbids self-certification, not certification.

It does not make undecidable statements exotic. Independent statements have turned out to be mathematically natural: the Paris–Harrington theorem, Goodstein’s theorem, and Kruskal’s tree theorem are all independent of PA and all things someone would want to prove. So “unprovable statements are contrived self-referential curiosities” is a comforting claim that stopped being true in 1977.

Boundary

  • Löb’s theorem. If $F \vdash (\mathrm{Prov}(\ulcorner A \urcorner) \to A)$ then $F \vdash A$. Believing your own proofs only about $A$ already commits you to $A$. The second theorem is the case $A = \bot$, and Löb is the sharper statement.
  • Tarski’s undefinability of truth. Truth is not arithmetically definable at all, a stronger and cleaner result than incompleteness, and it explains why the liar sentence does not simply live inside the system.
  • Completeness vs. incompleteness. Gödel also proved the completeness theorem for first-order logic: every logically valid sentence is provable. There is no conflict. Completeness is about logical consequence from arbitrary axioms; incompleteness is about a specific structure, the standard integers, which no first-order axiom set pins down.
  • The verification stack in practice. Since no system certifies itself, real systems shrink what must be trusted: a small kernel (LCF-style), independently checkable proof objects, and multiple independent checkers. The response to the regress is to make the base of it small enough to audit by eye.
  • Reverse mathematics. Rather than asking what is unprovable, ask which axioms a theorem needs. Most of classical analysis lives in weak subsystems, which is a much more informative map of the terrain than “some things are unprovable.”