Finally: Gödel’s Proof of Incompleteness!

Finally, we’re at the end of our walkthrough of Gödel great incompleteness proof. As a refresher, the basic proof sketch is:

  1. Take a simple logic. We’ve been using a variant of the Principia Mathematica’s logic, because that’s what Gödel used.
  2. Show that any statement in the logic can be encoded as a number using an arithmetic process based on the syntax of the logic. The process of encoding statements numerically is called Gödel numbering.
  3. Show that you can express meta-mathematical properties of logical statements in terms of arithemetic properties of their Gödel numbers. In particular, we need to build up the logical infrastructure that we need to talk about whether or not a statement is provable.
  4. Using meta-mathematical properties, show how you can create an unprovable statement encoded as a Gödel number.

What came before:

  1. Gödel numbering: The logic of the Principia, and how to encode it as numbers. This was step 1 in the sketch.
  2. Arithmetic Properties: what it means to say that a property can be expressed arithemetically. This set the groundwork for step 2 in the proof sketch.
  3. Encoding meta-math arithmetically: how to take meta-mathematical properties of logical statements, and define them as arithmetic properties of the Gödel numberings of the statements. This was step 2 proper.

So now we can move on to step three, where we actually see why mathematical logic is necessarily incomplete.

When we left off with Gödel, we’d gone through a very laborious process showing how we could express meta-mathematical properties of logical statements as primitive recursive functions and relations. We built up to being able to express one non-primitive recursive property, which describes the property that a given statement is provable:

pred provable(x) =
  some y {
    proofFor(y, x)

The reason for going through all of that was that we really needed to show how we could capture all of the necessary properties of logical statements in terms of arithmetic properties of their Gödel numbers.

Now we can get to the target of Gödel’s effort. What Gödel was trying to do was show how to defeat the careful stratification of the Principia’s logic. In the principia, Russell and Whitehead had tried to avoid problems with self-reference by creating a very strict stratification, where each variable or predicate had a numeric level, and could only reason about objects from lower levels. So if natural numbers were the primitive objects in the domain being reasoned about, then level-1 objects would be things like specific natural numbers, and level-1 predicates could reason about specific natural numbers, but not about sets of natural numbers or predicates over the natural numbers. Level-2 objects would be sets of natural numbers, and level-2 predicates could reason about natural numbers and sets of natural numbers, but not about predicates over sets of natural numbers, or sets of sets of natural numbers. Level-3 objects would be sets of sets of natural numbers… and so on.

The point of this stratification was to make self-reference impossible. You couldn’t make a statement of the form “This predicate is true”: the predicate would be a level-N predicate, and only a level N+1 predicate could reason about a level-N predicate.

What Gödel did in the laborious process we went through in the last post is embed a model of logical statements in the natural numbers. That’s the real trick: the logic is designed to work with a set of objects that are a model of the natural numbers. By embedding a model of logical statements in the natural numbers, he made it possible for a level-1 predicate (a predicate about a specific natural number) to reason about any logical statement or object. A level-1 predicate can now reason about a level-7 object! A level-1 predicate can reason about the set defined by a level-1 predicate: a level-1 predicate can reason about itself!.

Now, we can finally start getting to the point of all of this: incompleteness! We’re going to use our newfound ability to nest logical statements into numbers to construct an unprovable true statement.

In the last post, one of the meta-mathematical properties that we defined for the Gödel-numbered logic was immConseq, which defines when some statement x is an immediate consequence of a set of statements S. As a reminder, that means that x can be inferred from statements in S in one inferrence step.

We can use that property to define what it means to be a consequence of a set of statements: it’s the closure of immediate consequence. We can define it in pseudo-code as:

def conseq(κ) = {
  K = κ + axioms
  added_to_k = false
  do {
    added_to_k = false
    for all c in immConseq(K) {
      if c not in K {
        add c to K
        added_to_k = true
  } while added_to_k
  return K

In other words, Conseq(κ) is the complete set of everything that can possibly be inferred from the statements in κ and the axioms of the system. We can say that there’s a proof for a statement x in κ if and only if x ∈ Conseq(κ).

We can the idea of Conseq use that to define a strong version of what it means for a logical system with a set of facts to be consistent. A system is ω-consistent if and only if there is not a statement a such that: a ∈ Conseq(κ) ∧ not(forall(v, a)) ∈ Conseq(κ).

In other words, the system is ω-consistent as long as it’s never true that both a universal statement and it. But for our purposes, we can treat it as being pretty much the same thing. (Yes, that’s a bit hand-wavy, but I’m not trying to write an entire book about Gödel here!)

(Gödel’s version of the definition of ω-consistency is harder to read than this, because he’s very explicit about the fact that Conseq is a property of the numbers. I’m willing to fuzz that, because we’ve shown that the statements and the numbers are interchangable.)

Using the definition of ω-consistency, we can finally get to the actual statement of the incompleteness theorem!

Gödel’s First Incompleteness Theorem: For every ω-consistent primitive recursive set κ of formulae, there is a primitive-recursive predicate r(x) such that neither forall(v, r) nor not(forall(v, r)) is provable.

To prove that, we’ll construct the predicate r.

First, we need to define a version of our earlier isProofFigure that’s specific to the set of statements κ:

pred isProofFigureWithKappa(x, kappa) = {
  all n in 1 to length(x) {
    isAxiom(item(n, x)) or
    item(n, x) in kappa or
    some p in 0 to n {
      some q in 0 to n {
        immedConseq(item(n, x), item(p, x), item(q, x))
  } and length(x) > 0

This is the same as the earlier definition – just specialized so that it ensures that every statement in the proof figure is either an axiom, or a member of κ.

We can do the same thing to specialize the predicate proofFor and provable:

pred proofForStatementWithKappa(x, y, kappa) = {
  isProofFigureWithKappa(x, kappa) and
  item(length(x), x) = y

pred provableWithKappa(x, kappa) = {
  some y {
    proofForStatementWithKappa(y, x, kappa)

If κ is the set of basic truths that we can work with, then provable in κ is equivalent to provable.

Now, we can define a predicate UnprovableInKappa:

pred NotAProofWithKappa(x, y, kappa) = {
  not (proofForKappa(x, subst(y, 19, number(y))))

Based on everything that we’ve done so far, NotAProofWithKappa is primitive recursive.

This is tricky, but it’s really important. We’re getting very close to the goal, and it’s subtle, so let’s take the time to understand this.

  • Remember that in a Gödel numbering, each prime number is a variable. So 19 here is just the name of a free variable in y.
  • Using the Principia’s logic, the fact that variable 19 is free means that the statement is parametric in variable 19. For the moment, it’s an incomplete statement, because it’s got an unbound parameter.
  • What we’re doing in NotAProofWithKappa is substituting the numeric coding of y for the value of y‘s parameter. When that’s done, y is no longer incomplete: it’s unbound variable has been replaced by a binding.
  • With that substitution, NotAProofWithKappa(x, y, kappa) is true when x does not prove that y(y) is true.

What NotAProofWithKappa does is give us a way to check whether a specific sequence of statements x is not a proof of y.

We want to expand NotAProofWithKappa to something universal. Instead of just saying that a specific sequence of statements x isn’t a proof for y, we want to be able to say that no possible sequence of statements is a proof for y. That’s easy to do in logic: you just wrap the statement in a “∀ x ( )”. In Gödel numbering, we defined a function that does exactly that. So the universal form of provability is: ∀ a (NotAProofWithKappa(a, y, kappa)).

In terms of the Gödel numbering, if we assume that the Gödel number for the variable a is 17, and the variable y is numbered as 19, we’re talking about the statement p = forall(17, ProvableInKappa(17, 19, kappa).

p is the statement that for some logical statement (the value of variable 19, or y in our definition), there is no possible value for variable 17 (a) where a proves y in κ.

All we need to do now is show that we can make p become self-referential. No problem: we can just put number(p) in as the value of y in UnprovableInKappa. If we let q be the numeric value of the statement UnprovableInKappa(a, y), then:

r = subst(q, 19, p)

i = subst(p, 19, r)

i says that there is no possible value x that proves p(p). In other words, p(p) is unprovable: there exists no possible proof that there is no possible proof of p!

This is what we’ve been trying to get at all this time: self-reference! We’ve got a predicate y which is able to express a property of itself. Worse, it’s able to express a negative property of itself!

Now we’re faced with two possible choices. Either i is provable – in which case, κ is inconsistent! Or else i is unprovable – in which case κ is incomplete, because we’ve identified a true statement that can’t be proven!

That’s it: we’ve shown that in the principia’s logic, using nothing but arithmetic, we can create a true statement that cannot be proven. If, somehow, it were to be proven, the entire logic would be inconsistent. So the principia’s logic is incomplete: there are true statements that cannot be proven true.

We can go a bit further: the process that we used to produce this result about the Principia’s logic is actually applicable to other logics. There’s no magic here: if your logic is powerful enough to do Peano arithmetic, you can use the same trick that we demonstrated here, and show that the logic must be either incomplete or inconsistent. (Gödel proved this formally, but we’ll just handwave it.)

Looking at this with modern eyes, it doesn’t seem quite as profound as it did back in Gödel’s day.

When we look at it through the lens of today, what we see is that in the Principia’s logic, proof is a mechanical process: a computation. If every true statement was provable, then you could take any statement S, and write a program to search for a proof of either S or ¬ S, and eventually, that program would find one or the other, and stop.

In short, you’d be able to solve the halting problem. The proof of the halting problem is really an amazingly profound thing: on a very deep level, it’s the same thing as incompleteness, only it’s easier to understand.

But at the time that Gödel was working, Turing hadn’t written his paper about the halting problem. Incompletess was published in 1931; Turing’s halting paper was published in 1936. This was a totally unprecedented idea when it was published. Gödel produced one of the most profound and surprising results in the entire history of mathematics, showing that the efforts of the best mathematicians in the world to produce the perfection of mathematics were completely futile.

5 thoughts on “Finally: Gödel’s Proof of Incompleteness!

  1. lily

    woah, I’ve looked at a couple proofs of Godel’s theorem from a math point of view. Your computer science approach looks absolutely bizarre to me=p

  2. Chris P. Cogan

    About Russell’s theory of types and stratification. I understand that Russell himself didn’t like his own type theory, and that he was pleased when G. Spencer-Brown showed him that it was unneeded. My own view is simply that we should avoid making the truth of a proposition dependent only on what we hypothetically assume it to be. The logical paradoxes all arise from direct or indirect reasoning from a proposition whose truth can’t be determined except by trying out assumed possible values and seeing if this leads to a contradiction or not. For example, to determine if the set of all sets that are not members of themselves is a member of itself, we hypothetically assume either that it is or that it isn’t, and see where that leads us. This is where the infinite flip-flop loop begins, and it occurs for two reasons (only one of which is mentioned above):

    1. The proposition implies its own negation and that negated version implies ITS own negation,
    2. There is no INDEPENDENT basis for deciding whether the set is a member of itself or not.

    It is worth noting that essentially the same problem arises even in the case of propositions that don’t lead to paradoxes but which, when a truth value is hypothetically assumed, lead to the “conclusion” that that truth value is the actual (not merely hypothetical) truth value. For example, if we suppose that the set of all sets that ARE members of themselves is a member of itself, no paradoxical flip occurs, but the problem is that when we assume that it is not a member of itself, there is again no paradoxical flip. That is, it doesn’t care what truth value you assign. This is because it really has no truth value of its own.

    Note that, in both cases, we get circularity. In this second kind of self-dependent proposition, we get a kind of truth-value vacuousnes, and in the paradoxical case, we need one more step to complete the circle.

    To put my view in different words, what we need to ban are not self-referential propositions generally, but only those that have no independent (independent from themselves, that is) basis for determining a fixed truth value.

    (I’ve used the idea of propositions here because that seems to be the easiest way to understand the issue, and because all of the other types of logical paradox can be translated into a propositional form–as in the proposition that the set of all sets that are not members of themselves is (or is not) a member of itself).

  3. spencer

    I’m still trying to parse the following:

    “In other words, the system is ω-consistent as long as it’s never true that both a universal statement and it.”

    Should this be longer? Something like “The system is ω-consistent as long as a universal statement and a statement contradicting that universal statement are never both true.”?

  4. Marius

    Earlier today I posted a reply to a post on this blog which I only after hitting the Post Comment-button realized was from 2007!

    The subject was what Gödel himself saw as the true implications of his incompleteness theorem, which differs a bit from how it is often popularly interpreted (much like the Theory of Relativity, which is in some ways a theory of absolutes, such as the absolute causal separation of events outside of the light-cone).

    My main source for this is Rebecca Goldstein’s book “Incompleteness”, a highly interesting source on Gödel’s world view and philosophy of mathematics.

    I’ll reproduce the comment here as it’s relevant to this more recent series of posts:

    “My question is this: If I believe in a single coherent reality that exists independent of my ability to perceive it (that is, I’m not making it up and it would continue in my absence), does Godel’s theorem pose a problem for my belief or just my ability to describe it?”

    At most the latter! In fact, Gödel was a hardcore mathematical Platonist and he was always disappointed that his incompleteness theorem was misunderstood as implying that no absolute mathematical truths exist. What *he* believed to have shown, was that in any “sufficiently complex” axiomatic system (those that can produce ordinary whole number arithmetic), it is possible to create a statement that *we*, from our point of view “outside” the system, *know* to be true, but which is unprovable within the system.

    He essentially does this by using arithmetic to encode a statement that says, “This statement is unprovable in this system”, which, *if* the system is consistent, necessarily has to be true, or else we would have derived a contradiction in the system.

    From the point of view of the system, this is a statement about arithmetic, saying something about prime factors of some humongous number, which the system is not able to prove or disprove. From our point of view, as humans outside the system, the statement has a double meaning which we have encoded in it, which enables us to say for sure that it must be true, if the system is consistent.

    Hence, any sufficiently complex (i.e. useful) axiomatic system is either inconsistent or incomplete. Hence, in any useful and consistent (an inconsistent system isn’t very useful!) mathematical system, there are *true* statements that cannot be proven. Hence, mathematical truth and provability are not the same – truth is independent from formal provability.

    For this reason, Gödel also believed statements such as the Continuum Hypothesis have an absolute truth value despite their independence from our usual axioms of set theory (he believed the Continuum Hypothesis to be false and at some point I think he conjectured that the cardinality of the continuum is aleph_2).

    It is interesting, in light of this, to ponder how difficult it is to prove seemingly simple statements in number theory that everybody believe to be true, such as the Goldbach conjecture.


Leave a Reply