Gödel's incompleteness theorem, explained (I)

The work of Austrian mathematician Kurt Gödel, developed in the first part of the twentieth century well before the advent of computers, is key to understanding the limitations upon modern artificial intelligence. But before we can understand why, it is important to comprehend what this, one of the most difficult theorems in mathematical logic, actually says and how it is proven.

Gödel’s first incompleteness theorem states that any mathematical system that is both powerful enough to express ordinary whole-number arithmetic and is built from a clear, mechanical list of rules will inevitably leave some true statements unprovable within that system. In short: if the system is consistent (it never proves a contradiction), then it is incomplete (there are true claims it cannot prove).

His second incompleteness theorem goes further: no such system can prove its own consistency, provided it really is consistent and strong enough to talk about whole numbers and proofs.

Before explaining why this is so, we need three ideas: what kind of systems we are talking about; how to let a system “talk about” its own statements and proofs; and how to build a sentence that, in effect, refers to itself.

Formal systems for arithmetic

A formal system is a precise system of stipulation, and any computer algorithm is a formal system:

• It has an alphabet of basic marks and carefully defined grammar for forming statements (sentences).

  
  

• It has a fixed list of axioms (starting points) and rules of inference that tell you how to derive new statements from old ones.

  
  

• It is effectively axiomatic: you could, in principle, program a machine to check whether a line is an axiom and whether a sequence of lines is a correct proof.

  
  

• It is strong enough to express everyday facts about whole numbers: addition, multiplication, comparisons, and simple reasoning about them.

“Consistent” means the system never proves both a statement and its denial. “Complete” (in Gödel’s sense here) means every true arithmetic statement expressible in the system is provable in it.

The key trick: letting arithmetic talk about syntax

At first glance, a system about numbers seems to have nothing to do with its own sentences and proofs. Gödel’s stroke of genius was to encode every bit of syntactic data—letters, words, sentences, and entire proofs—by ordinary whole numbers. This is called arithmetisation of syntax.

Think of it like giving every piece of text a unique barcode. Once you have a scheme that assigns a number to each symbol and a recipe for combining these numbers to encode whole sentences and proof lists, questions about strings of symbols can be turned into questions about numbers. For example:

• “Is this string a well-formed sentence?” becomes “Does this number have the arithmetical property that corresponds to being well-formed?”

  
  

• “Is this list of sentences a valid proof of that sentence?” becomes “Does this pair of numbers fit the arithmetical pattern that encodes a correct proof-relation?”

Because our system already knows how to reason about numbers, and because the encoding uses only basic arithmetic operations, the system can express these syntactic properties internally. In plain terms, the system can write down a statement that says, “There exists a number which is the barcode of a valid proof of the sentence with barcode such-and-such.”

From this we obtain a crucial ingredient: a provability predicate—a formula inside the system that, when fed the barcode of a sentence, asserts “there is a number that codes a proof of this sentence.” One can also express the absence of proof.

The mirror: building a self-referential sentence

The next ingredient is a general method for creating self-reference, called the diagonal or fixed-point construction. Here is the idea without symbols.

Suppose you can write templates for sentences with a blank—“The sentence with barcode ‘blank’ is not provable.” For any particular filling of the blank (that is, for any particular barcode), you have a concrete sentence. The diagonal method shows how to choose a filling that points the sentence back at itself. You end up with a specific sentence G that effectively says:

“This very sentence is not provable in the system.”

Nothing mystical happens: the claim is achieved by combining the barcode trick with a careful template so that the sentence’s own barcode is the one inserted into its blank.

Why G forces incompleteness

Consider what happens if the system is consistent.

• If the system proved G, then G would be false (because G asserts it is not provable). The system would have proved a falsehood, which contradicts consistency. So, assuming consistency, the system does not prove G.

  
  

• If the system proved “not G” (that G is false) then, unpacking what G says, the system would be proving that “G is provable.” But we just argued that in a consistent system G is not provable. Proving “not G” would thereby force a contradiction. So, again under the usual mild assumptions on the system, it also does not prove “not G.”

Therefore G is not provable, and its denial is not provable either. Moreover out in the intended world of the whole numbers, G is actually true (because, indeed, there is no proof of it if the system is consistent). We have found a true but unprovable sentence: the system is incomplete.

This is Gödel’s first incompleteness theorem in essence.

A word on a technical refinement (Rosser’s trick)

Gödel’s original argument used a slightly stronger assumption called omega-consistency. Shortly afterwards, Rosser sharpened the construction so that mere consistency suffices. The high-level story above remains the same: one still encodes syntax into arithmetic and crafts a true sentence that defeats any consistent, effectively axiomatic arithmetic.

Why the system cannot prove its own consistency

The second incompleteness theorem uses the same machinery. Once the system can talk about its own proofs, it can also write a sentence that expresses “there is no proof of a contradiction.” Call that the consistency statement of the system.

If the system could prove its own consistency, one can show (still working entirely within arithmetic) that it would then also prove the Gödel sentence G from before. But we have already seen that, assuming the system is consistent, it cannot prove G. Therefore a consistent system cannot prove its own consistency statement.

Intuitively: a system cannot, from within, certify that its proof engine will never go off the rails—at least not if that engine is strong enough to capture ordinary arithmetic and follows mechanical rules. Now imagine that the engine is any modern computer, no matter how sophisticated. The engine cannot prove that it will never go off the rails.

What the theorems do—and do not—say

• They do not say mathematicians cannot know the system is consistent. They say the system itself cannot derive that fact. Mathematicians may argue for consistency using stronger principles, or by informal reasoning outside the system, but then those stronger principles face the same limitation about proving their own consistency. So there are statements that computers can never know are true but mathematicians or human beings can now are true.

  
  

• They do not undermine every area of mathematics. They apply to any single, effective axiom system that captures arithmetic. In practice, mathematics proceeds by adopting axioms sufficient for a domain and proving what one can; Gödel shows there can be no all-purpose, mechanically listable axiom system that settles every arithmetical truth. In the context of computation, computers can never know everything.

  
  

• They sit alongside Gödel’s separate completeness theorem for first-order logic (a system for expressing the logical relations between simple sentences), which says the rules of logic themselves are complete for pure logical consequence. There is no contradiction: the completeness theorem concerns logic alone; the incompleteness theorems concern arithmetic theories, of the kind that computers build, on top of that logic.

Why this mattered—and still does

Gödel changed the ambition of foundational programmes that sought a single, complete, mechanised basis for all of mathematics (and hence computational reasoning). Any such basis rich enough for arithmetic must leave truths beyond formal proof and cannot, from within, guarantee its own reliability. This does not paralyse mathematics; rather, it clarifies its nature: proof is formal, but mathematical truth over the whole numbers outruns any single formal net we can cast with a computable list of axioms.

A compact summary of the proof strategy

1. Design a way to encode every sentence and proof as a unique whole number.

2. Show that the system can express statements about those codes, including “x is a proof of y.”

3. Use the fixed-point method to build a specific sentence G that asserts of itself that there is no proof of it in the system.

4. Argue: if the system is consistent, it proves neither G nor its denial; moreover, G is true in the standard whole numbers. This yields incompleteness.

5. Express within the system the claim “there is no proof of a contradiction”. Show that, if the system could prove that claim, it would also prove G—contradicting step 4. Hence a consistent system cannot prove its own consistency.

That is Gödel’s theorem in prose: arithmetic can mirror talk about proofs well enough to create a sentence that eludes any consistent, mechanical axiom system; and no such system can vouch for its own consistency from within. This is a fundamental limitation on computational reasoning: no computational system can derive every proposition that a human can see as obviously true. Computational systems have a blind eye, and that eye is the human imagination in its capacity to see beyond the bounds of an internal system. Human imagination can undertake this exercise indefinitely: no matter how complex the system, the human imagination can always go one step further.