Incompleteness and Provability

Fixed point lemma in a theory extending Q

Let $\Th{T}$source be any theory extending $\Th{Q}$source, and let $!B(x)$source be any formula with only the variable $x$source free. Then there is a sentence $!A$source such that $\Th{T} \Proves!A \liff !B(\gn{!A})$source.

Explain

The fixed-point lemma says that for any formula $!B(x)$source, there is a sentence $!A$source such that $\Th{T} \Proves !A \liff !B(\gn{!A})$source, provided $\Th{T}$source extends $\Th{Q}$source. In the case of the liar sentence, we'd want $!A$source to be equivalent (provably in $\Th{T}$source) to “$\gn{!A}$source is false,” i.e., the statement that $\Gn{!A}$source is the Gödel number of a false sentence. To understand the idea of the proof, it will be useful to compare it with Quine's informal gloss of $!A$source as, “`yields a falsehood when preceded by its own quotation' yields a falsehood when preceded by its own quotation.” The operation of taking an expression, and then forming a sentence by preceding this expression by its own quotation may be called diagonalizing the expression, and the result its diagonalization. So, the diagonalization of `yields a falsehood when preceded by its own quotation' is “`yields a falsehood when preceded by its own quotation' yields a falsehood when preceded by its own quotation.” Now note that Quine's liar sentence is not the diagonalization of `yields a falsehood' but of `yields a falsehood when preceded by its own quotation.' So the property being diagonalized to yield the liar sentence itself involves diagonalization!

In the language of arithmetic, we form quotations of a formula with one free variable by computing its Gödel numbers and then substituting the standard numeral for that Gödel number into the free variable. The diagonalization of $!E(x)$source is $!E(\num{n})$source, where $n = \Gn{!E(x)}$source. (From now on, let's abbreviate $\num{\Gn{!E(x)}}$source as $\gn{!E(x)}$source.) So if $!B(x)$source is “is a falsehood,” then “yields a falsehood if preceded by its own quotation,” would be “yields a falsehood when applied to the Gödel number of its diagonalization.” If we had a symbol $\Obj{diag}$source for the function $\fn{diag}(n)$source which computes the Gödel number of the diagonalization of the formula with Gödel number $n$source, we could write $!E(x)$source as $!B(\Obj{diag}(x))$source. And Quine's version of the liar sentence would then be the diagonalization of it, i.e., $!E(\gn{!E(x)})$source or $!B(\Obj{diag}(\gn{!B(\Obj{diag}(x))}))$source. Of course, $!B(x)$source could now be any other property, and the same construction would work. For the incompleteness theorem, we'll take $!B(x)$source to be “$x$source is not derivable in $\Th{T}$source.” Then $!E(x)$source would be “yields a sentence not derivable in $\Th{T}$source when applied to the Gödel number of its diagonalization.”

To formalize this in $\Th{T}$source, we have to find a way to formalize $\fn{diag}$source. The function $\fn{diag}(n)$source is computable, in fact, it is primitive recursive: if $n$source is the Gödel number of a formula $!E(x)$source, $\fn{diag}(n)$source returns the Gödel number of $!E(\gn{!E(x)})$source. (Recall, $\gn{!E(x)}$source is the standard numeral of the Gödel number of $!E(x)$source, i.e., $\num{\Gn{!E(x)}}$source). If $\Obj{diag}$source were a function symbol in $\Th{T}$source representing the function $\fn{diag}$source, we could take $!A$source to be the formula $!B(\Obj{diag}(\gn{!B(\Obj{diag}(x))}))$source. Notice that

Assuming $\Th{T}$source can derive

it can derive $!B(\Obj{diag}(\gn{!B(\Obj{diag}(x))})) \liff !B(\gn{!A})$source. But the left hand side is, by definition, $!A$source.

Of course, $\Obj{diag}$source will in general not be a function symbol of $\Th{T}$source, and certainly is not one of $\Th{Q}$source. But, since $\fn{diag}$source is computable, it is representable in $\Th{Q}$source by some formula $!D_{\fn{diag}}(x,y)$source. So instead of writing $!B(\Obj{diag}(x))$source we can write $\lexists[y][(!D_{\fn{diag}}(x,y) \land !B(y))]$source. Otherwise, the proof sketched above goes through, and in fact, it goes through already in $\Th{Q}$source.

Fixed point lemma already provable in Q

Let $!B(x)$source be any formula with one free variable $x$source. Then there is a sentence $!A$source such that $\Th{Q} \Proves !A \liff !B(\gn{!A})$source.

Proof

Given $!B(x)$source, let $!E(x)$source be the formula $\lexists[y][(!D_{\fn{diag}}(x,y) \land !B(y))]$source and let $!A$source be its diagonalization, i.e., the formula $!E(\gn{!E(x)})$source.

Since $!D_{\fn{diag}}$source represents $\fn{diag}$source, and $\fn{diag}(\Gn{!E(x)}) = \Gn{!A}$source, $\Th{Q}$source can derive

Now we show that $\Th{Q} \Proves !A \liff !B(\gn{!A})$source. We argue informally, using just logic and facts derivable in $\Th{Q}$source.

First, suppose $!A$source, i.e., $!E(\gn{!E(x)})$source. Going back to the definition of $!E(x)$source, we see that $!E(\gn{!E(x)})$source just is

Consider such a $y$source. Since $!D_{\fn{diag}}(\gn{!E(x)},y)$source, by the second diagonal representation fact, uniqueness of the output, $y = \gn{!A}$source. So, from $!B(y)$source we have $!B(\gn{!A})$source.

Now suppose $!B(\gn{!A})$source. By the first diagonal representation fact, the represented value, we have

But that's just $!E(\gn{!E(x)})$source, i.e., $!A$source.

Digress

You should compare this to the proof of the fixed-point lemma in computability theory. The difference is that here we want to define a statement in terms of itself, whereas there we wanted to define a function in terms of itself; this difference aside, it is really the same idea.

Exercise ruling out a provable truth definition

A formula $!A(x)$source is a truth definition if $\Th{Q} \Proves !B \liff !A(\gn{!B})$source for all sentences $!B$source. Show that no formula is a truth definition by using the fixed-point lemma.

Consistency makes the Goedel sentence unprovable

If $\Th{T}$source is a consistent, axiomatizable theory extending $\Th{Q}$source, then $\Th{T} \Proves/ !G_\Th{T}$source.

Proof

Suppose $\Th{T}$source derives $!G_\Th{T}$source. Then there is a derivation, and so, for some number $m$source, the relation $\Prf[\Th{T}](m, \Gn{!G_\Th{T}})$source holds. But then $\Th{Q}$source derives the sentence $\OPrf[\Th{T}](\num m, \gn{!G_\Th{T}})$source. So $\Th{Q}$source derives $\lexists[x][\OPrf[\Th{T}](x,\gn{!G_\Th{T}})]$source, which is, by definition, $\OProv[\Th{T}](\gn{!G_\Th{T}})$source. By the defining equivalence of the Goedel sentence, $\Th{Q}$source derives $\lnot !G_\Th{T}$source, and since $\Th{T}$source extends $\Th{Q}$source, so does $\Th{T}$source. We have shown that if $\Th{T}$source derives $!G_\Th{T}$source, then it also derives $\lnot !G_\Th{T}$source, and hence it would be inconsistent.

Definition of omega consistency

A theory $\Th{T}$source is $\omega$source-consistent if the following holds: if $\lexists[x][!A(x)]$source is any sentence and $\Th{T}$source derives $\lnot !A(\num 0)$source, $\lnot !A(\num 1)$source, $\lnot !A(\num 2)$source, dots then $\Th{T}$source does not prove $\lexists[x][!A(x)]$source.

Omega consistency makes the Goedel sentence irrefutable

If $\Th{T}$source is an $\omega$source-consistent, axiomatizable theory extending $\Th{Q}$source, then $\Th{T} \Proves/ \lnot !G_\Th{T}$source.

Proof

We show that if $\Th{T}$source derives $\lnot !G_\Th{T}$source, then it is $\omega$source-inconsistent. Suppose $\Th{T}$source derives $\lnot !G_\Th{T}$source. If $\Th{T}$source is inconsistent, it is $\omega$source-inconsistent, and we are done. Otherwise, $\Th{T}$source is consistent, so it does not derive $!G_\Th{T}$source by the lemma that consistency makes the Goedel sentence unprovable. Since there is no derivation of $!G_\Th{T}$source in $\Th{T}$source, $\Th{Q}$source derives

and so does $\Th{T}$source. On the other hand, by the defining equivalence of the Goedel sentence, $\lnot !G_\Th{T}$source is equivalent to $\lexists[x][\OPrf[\Th{T}](x,\gn{!G_\Th{T}})]$source. So $\Th{T}$source is $\omega$source-inconsistent.

Exercise separating consistency from omega consistency

Every $\omega$source-consistent theory is consistent. Show that the converse does not hold, i.e., that there are consistent but $\omega$source-inconsistent theories. Do this by showing that $\Th{Q} \cup \{\lnot !G_\Th{Q}\}$source is consistent but $\omega$source-inconsistent.

Goedel first incompleteness theorem

Let $\Th{T}$source be any $\omega$source-consistent, axiomatizable theory extending $\Th{Q}$source. Then $\Th{T}$source is not complete.

Proof

If $\Th{T}$source is $\omega$source-consistent, it is consistent, so $\Th{T} \Proves/ !G_\Th{T}$source by the lemma that consistency makes the Goedel sentence unprovable. By the lemma that omega consistency makes the Goedel sentence irrefutable, $\Th{T} \Proves/ \lnot !G_\Th{T}$source. This means that $\Th{T}$source is incomplete, since it derives neither $!G_\Th{T}$source nor $\lnot !G_\Th{T}$source.

Rosser incompleteness theorem

Let $\Th{T}$source be any consistent, axiomatizable theory extending $\Th{Q}$source. Then $\Th{T}$source is not complete.

Proof

Recall that $\OProv[\Th{T}](y)$source is defined as $\lexists[x][\OPrf[\Th{T}](x, y)]$source, where $\OPrf[\Th{T}](x, y)$source represents the decidable relation which holds iff $x$source is the Gödel number of a derivation of the sentence with Gödel number $y$source. The relation that holds between $x$source and $y$source if $x$source is the Gödel number of a refutation of the sentence with Gödel number $y$source is also decidable. Let $\fn{not}(x)$source be the primitive recursive function which does the following: if $x$source is the code of a formula $!A$source, $\fn{not}(x)$source is a code of $\lnot !A$source. Then $\Refut[\Th{T}](x, y)$source holds iff $\Prf[\Th{T}](x, \fn{not}(y))$source. Let $\ORefut[\Th{T}](x, y)$source represent it. Then, if $\Th{T} \Proves \lnot !A$source and $\delta$source is a corresponding derivation, $\Th{Q} \Proves \ORefut[\Th{T}](\gn{\delta}, \gn{!A})$source. We define $\ORProv[\Th{T}](y)$source as

Roughly, $\ORProv[\Th{T}](y)$source says “there is a proof of $y$source in $\Th{T}$source, and there is no shorter refutation of $y$source.” Assuming $\Th{T}$source is consistent, $\ORProv[\Th{T}](y)$source is true of the same numbers as $\OProv[\Th{T}](y)$source; but from the point of view of provability in $\Th{T}$source (and we now know that there is a difference between truth and provability!) the two have different properties. If $\Th{T}$source is inconsistent, then the two do not hold of the same numbers! ($\ORProv[\Th{T}](y)$source is often read as “$y$source is Rosser provable.” Since, as just discussed, Rosser provability is not some special kind of provability---in inconsistent theories, there are sentences that are provable but not Rosser provable---this may be confusing. To avoid the confusion, you could instead read it as “$y$source is shmovable.”)

By the fixed-point lemma, there is a formula $!R_\Th{T}$source such that

In contrast to the proof of the first incompleteness theorem, here we claim that if $\Th{T}$source is consistent, $\Th{T}$source doesn't derive $!R_\Th{T}$source, and $\Th{T}$source also doesn't derive $\lnot !R_\Th{T}$source. (In other words, we don't need the assumption of $\omega$source-consistency.)

First, let's show that $\Th{T} \Proves/ !R_{\Th{T}}$source. Suppose it did, so there is a derivation of $!R_{\Th{T}}$source from $T$source; let $n$source be its Gödel number. Then $\Th{Q} \Proves \OPrf[\Th{T}](\num{n}, \gn{!R_{\Th{T}}})$source, since $\OPrf[\Th{T}]$source represents $\Prf[\Th{T}]$source in $\Th{Q}$source. Also, for each $k < n$source, $k$source is not the Gödel number of a derivation of $\lnot !R_{\Th{T}}$source, since $\Th{T}$source is consistent. So for each $k < n$source, $\Th{Q} \Proves \lnot \ORefut[\Th{T}](\num{k}, \gn{!R_{\Th{T}}})$source. By the lemma describing the finitely many numbers below a numeral, $\Th{Q} \Proves \lforall[z][(z < \num{n} \lif \lnot \ORefut[\Th{T}](z, \gn{!R_{\Th{T}}}))]$source. Thus,

but that's just $\ORProv[\Th{T}](\gn{!R_{\Th{T}}})$source. By the defining equivalence of the Rosser sentence, $\Th{Q} \Proves \lnot !R_{\Th{T}}$source. Since $\Th{T}$source extends $\Th{Q}$source, also $\Th{T} \Proves \lnot !R_{\Th{T}}$source. We've assumed that $\Th{T} \Proves !R_{\Th{T}}$source, so $\Th{T}$source would be inconsistent, contrary to the assumption of the theorem.

Now, let's show that $\Th{T} \Proves/ \lnot !R_{\Th{T}}$source. Again, suppose it did, and suppose $n$source is the Gödel number of a derivation of $\lnot !R_{\Th{T}}$source. Then $\Refut[\Th{T}](n, \Gn{!R_{\Th{T}}})$source holds, and since $\ORefut[\Th{T}]$source represents $\Refut[\Th{T}]$source in $\Th{Q}$source, $\Th{Q} \Proves \ORefut[\Th{T}](\num{n}, \gn{!R_{\Th{T}}})$source. We'll again show that $\Th{T}$source would then be inconsistent because it would also derive $!R_{\Th{T}}$source. Since

The sentence $\lnot \ORProv[\Th{T}](\gn{!R_{\Th{T}}})$source, i.e.,

We argue informally using logic, making use of facts about what $\Th{Q}$source derives. Suppose $x$source is arbitrary and $\OPrf[\Th{T}](x, \gn{!R_{\Th{T}}})$source. We already know that $\Th{T} \Proves/ !R_{\Th{T}}$source, and so for every $k$source, $\Th{Q} \Proves \lnot \OPrf[\Th{T}](\num{k}, \gn{!R_{\Th{T}}})$source. Thus, for every $k$source it follows that $\eq/[x][\num{k}]$source. In particular, we have (a) that $\eq/[x][\num{n}]$source. We also have $\lnot(\eq[x][\num{0}] \lor \eq[x][\num{1}] \lor \dots \lor \eq[x][\num{n-1}])$source and so by the lemma describing the finitely many numbers below a numeral, (b) $\lnot(x < \num{n})$source. By the trichotomy lemma for comparison with a numeral, $\num{n} < x$source. Since $\Th{Q} \Proves \ORefut[\Th{T}](\num{n}, \gn{!R_{\Th{T}}})$source, we have $\num{n} < x \land \ORefut[\Th{T}](\num{n}, \gn{!R_{\Th{T}}})$source, and from that $\lexists[z][(z < x \land \ORefut[\Th{T}](z,\gn{!R_{\Th{T}}}))]$source. Since $x$source was arbitrary we get, as required, that

Exercise on computable inseparability of provable and refutable sentences

Two sets $A$source and $B$source of natural numbers are said to be computably inseparable if there is no decidable set $X$source such that $A \subseteq X$source and $B \subseteq \Complement{X}$source ($\Complement{X}$source is the complement, $\Nat \setminus X$source, of $X$source). Let $\Th{T}$source be a consistent axiomatizable extension of $\Th{Q}$source. Suppose $A$source is the set of Gödel numbers of sentences provable in $\Th{T}$source and $B$source the set of Gödel numbers of sentences refutable in $\Th{T}$source. Prove that $A$source and $B$source are computably inseparable.

Digress

Incidentally, Gödel was lazy in the same way we are being now. At the end of the 1931 paper, he sketches the proof of the second incompleteness theorem, and promises the details in a later paper. He never got around to it; since everyone who understood the argument believed that it could be carried out (he did not need to fill in the details.)

Second incompleteness theorem for Peano arithmetic

Assuming $\Th{PA}$source is consistent, then $\Th{PA}$source does not derive $\OCon[\Th{PA}]$source.

General second incompleteness theorem

Let $\Th{T}$source be any consistent, axiomatized theory extending $\Th{Q}$source and let $\OProv[\Th{T}](y)$source be any formula satisfying derivability conditions P1--P3 for $\Th{T}$source. Then $\Th{T}$source does not derive $\OCon[T]$source.

Exercise deriving consistency from the Goedel sentence

Show that $\Th{PA}$source derives $!G_{\Th{PA}} \lif \OCon[\Th{PA}]$source.

Digress

The moral of the story is that no “reasonable” consistent theory for mathematics can derive its own consistency statement. Suppose $\Th{T}$source is a theory of mathematics that includes $\Th{Q}$source and Hilbert's “finitary” reasoning (whatever that may be). Then, the whole of $\Th{T}$source cannot derive the consistency statement of $\Th{T}$source, and so, a fortiori, the finitary fragment can't derive the consistency statement of $\Th{T}$source either. In that sense, there cannot be a finitary consistency proof for “all of mathematics.”

There is some leeway in interpreting the term “finitary,” and Gödel, in the 1931 paper, grants the possibility that something we may consider “finitary” may lie outside the kinds of mathematics Hilbert wanted to formalize. But Gödel was being charitable; today, it is hard to see how we might find something that can reasonably be called finitary but is not formalizable in, say, $\Th{ZFC}$source, Zermelo--Fraenkel set theory with the axiom of choice.

Loeb theorem

Let $\Th{T}$source be an axiomatizable theory extending $\Th{Q}$source, and suppose $\OProv[\Th{T}](y)$source is a formula satisfying conditions P1--P3 from the section on the second incompleteness theorem. If $\Th{T}$source derives $\OProv[\Th{T}](\gn{!A}) \lif !A$source, then in fact $\Th{T}$source derives $!A$source.

Explain

The heuristic for the proof of Löb's theorem is a clever proof that Santa Claus exists. (If you don't like that conclusion, you are free to substitute any other conclusion you would like.) Here it is:

1. Let $X$source be the sentence, “If $X$source is true, then Santa Claus exists.”

2. Suppose $X$source is true.

3. Then what it says holds; i.e., we have: if $X$source is true, then Santa Claus exists.

4. Since we are assuming $X$source is true, we can conclude that Santa Claus exists, by modus ponens from (2) and (3).

5. We have succeeded in deriving (4), “Santa Claus exists,” from the assumption (2), “$X$source is true.” By conditional proof, we have shown: “If $X$source is true, then Santa Claus exists.”

6. But this is just the sentence $X$source. So we have shown that $X$source is true.

7. But then, by the argument (2)--(4) above, Santa Claus exists.