What Happens When You Iterate Gödel’s Theorem?

Let \mathrm{PA} be Peano Arithmetic.  Gödel’s Second Incompleteness Theorem says that no consistent theory T extending \mathrm{PA} can prove its own consistency. (I’ll write \mathrm{Con}(T) for the statement asserting T‘s consistency; more on this later.)

In particular, \mathrm{PA} + \mathrm{Con}(\mathrm{PA}) is stronger than \mathrm{PA}.  But certainly, given that we believe that everything \mathrm{PA} proves is true, we believe that \mathrm{PA} does not prove a contradiction, and hence is consistent.  Thus, we believe that everything that (\mathrm{PA} + \mathrm{Con}(\mathrm{PA})) proves is true.  But by a similar argument, we believe that everything that (\mathrm{PA} + \mathrm{Con}(\mathrm{PA} + \mathrm{Con}(\mathrm{PA}))) proves is true.  Where does this stop?  Once we believe that everything \mathrm{PA} proves is true, what, exactly, are we committed to believing?

This is from Chapters 13–15 of Torkel Franzén’s book Inexhaustibility, which is admirably clear and well-written.

First off, let \mathrm{PA}_0 be \mathrm{PA}, and let \mathrm{PA}_{n+1} be \mathrm{PA}_n+\mathrm{Con}(\mathrm{PA}_n).  By the considerations above, we accept that each \mathrm{PA}_n is sound.  (A theory being sound means that everything it proves is true.)

So, if we therefore let \mathrm{PA}_\omega = \bigcup_{n\in\mathbb{N}}\mathrm{PA}_n, then we accept that \mathrm{PA}_\omega is sound.  We could therefore define \mathrm{PA}_{\omega + 1} to be \mathrm{PA}_\omega + \mathrm{Con}(\mathrm{PA}_\omega) and we would have to accept that as sound as well, but in making this definition we run up against our first snag.

The snag is this: In order to express a sentence of the form \mathrm{Con}(T) in the language of number theory, we much choose some recursively enumerable presentation of T, and which recursively enumerable presentation we choose matters.  For example, if we add to any given presentation of T the stipulation that we are adding, for all x,y,z > 0 and n > 2 such that x^n + y^n = z^n the axiom 0 = 1, then we haven’t actually added any new axioms, but if we construct the statement \mathrm{Con}(T) with T presented the second way, \mathrm{Con}(T) will imply Fermat’s Last Theorem, while \mathrm{Con}(T) constructed from the original presentation of T may not.

As you might guess from the above, we are going to want to construct \mathrm{PA}_\alpha for ordinals \alpha.  When \alpha is a successor ordinal, it is clear how to get a “reasonable” presentation of \mathrm{PA}_\alpha from a reasonable presentation of \mathrm{PA}_\beta (where \beta + 1 = \alpha), but if \alpha is a limit ordinal, in general it won’t be clear (although it is clear for \alpha = \omega).

So how can we solve this problem?

The first step is to use a more computable representation of ordinals, namely ordinal notations. An ordinal notation is a number n\in\mathbb{N} with the following property: It is either 0, or for every m\in\mathbb{N}, the output of the nth Turing machine on input m is an ordinal notation.  (What this recursive definition really means is that the set of ordinal notations is the smallest set satisfying the above property.)

Given an ordinal notation n, we let the ordinal it represents, |n|, be defined by |0| = 0 and |n| = \sup_{m\in\mathbb{N}} (|\phi_n(m)|+1), where \phi_n(m) denotes the output of the nth Turing machine on input m.

We can now uniformly pick presentations of \mathrm{PA}_a for ordinal notations a by letting \mathrm{PA}_0 = \mathrm{PA} and \mathrm{PA}_a be presented as the union of \mathrm{PA}_{\phi_a(m)} + \mathrm{Con}(\mathrm{PA}_{\phi_a(m)}) over m\in\mathbb{N}, where the consistency statements are constructed using the presentations given by induction.

Unfortunately, this doesn’t prevent us from doing the trick mentioned above: For any true \Pi_1 sentence \phi, there is an ordinal notation a such that |a| = 1 and \mathrm{PA}_a proves \phi.  The catch is that a will be quite an unusual notation for 1, and we’re not really justified in taking \mathrm{PA}_a to be a consistency extension of \mathrm{PA} because \mathrm{PA} doesn’t “know” that a is an ordinal notation.

However, we can make a reasonable definition for what it means for \mathrm{PA} (or any extension) to prove that a number a is an ordinal notation.  (This is actually not trivial, since \mathrm{PA} can only talk about numbers, but the set of ordinal notations was defined to be the least set satisfying a certain property.)  We can then define an autonomous consistency extension of \mathrm{PA} as follows: \mathrm{PA} is an autonomous consistency extension of itself, and if T is an autonomous consistency extension of \mathrm{PA}, and T proves that a is an ordinal notation, then T_a is an autonomous consistency extension of \mathrm{PA}.

The autonomous consistency extensions of \mathrm{PA} have some claim to being exactly those that we recognize to be consistency extensions of \mathrm{PA} solely on the basis that we accept \mathrm{PA}.  But that isn’t really completely satisfying.  There’s nothing stopping us from letting T_A be the union of the autonomous consistency extensions of \mathrm{PA} and considering T_A + \mathrm{Con}(T_A).  Similarly, we got the set of autonomous consistency extensions of \mathrm{PA} by starting with \mathrm{PA} and then closing under finite applications of a particular operation, but we could also have considered transfinite applications of that operation.

Does there exist a theory (which we believe is true) which will prove anything any reasonable iterated consistency extension of \mathrm{PA} proves?  It turns out there is.  Let \mathrm{PA}^{\Sigma-REF} be the theory obtained by adding to \mathrm{PA} the axiom that for any \Sigma_1 sentence \phi (that is, sentence of the form \exists x_1\cdots \exists x_n \psi(x_1,\ldots, x_n) where all of \psi‘s quantifiers are bounded), if \mathrm{PA} proves \phi, then \phi is true.

This property is called \Sigma_1-soundness, and the axiom formalizing it is called a reflection axiom.  If T is \Sigma_1-sound, then so is T + \mathrm{Con}(T), since if T + \mathrm{Con}(T) proved a false \Sigma_1 statement \phi, then T would prove the false \Sigma_1 statement \neg \mathrm{Con}(T) \vee \phi (false because \Sigma_1-soundness implies consistency).  Similarly, any union of a chain of \Sigma_1-sound theories must be \Sigma_1-sound.

Because we can formalize the above argument in \mathrm{PA}, \mathrm{PA}^{\Sigma-REF} proves that every autonomous consistency extension of \mathrm{PA} is \Sigma_1-sound.  Therefore, it proves that every autonomous consistency extension of \mathrm{PA} is consistent.  Therefore (since essentially autonomous consistency extensions of \mathrm{PA} say nothing besides the fact that lower autonomous consistency extensions are consistent), \mathrm{PA}^{\Sigma-REF} extends each autonomous consistency extension of \mathrm{PA}.

Okay, so adding axioms asserting that \mathrm{PA} is \Sigma_1-sound takes us beyond all the autonomous consistency extensions of \mathrm{PA}.  But what happens if add to \mathrm{PA}^{\Sigma-REF} axioms asserting that \mathrm{PA}^{\Sigma-REF} is \Sigma_1-sound?  This is called a reflection extension, and we can form autonomous iterated reflection extensions just as we can autonomous iterated consistency extensions.

Is there any theory (which we believe is true) which goes beyond all the autonomous reflection extensions the same way that \mathrm{PA}^{\Sigma-REF} goes beyond all the autonomous consistency extensions of \mathrm{PA}?  There is. The theory \mathrm{PA}^{\Sigma-REF} asserts that all \Sigma_1 sentences that \mathrm{PA} proves are true.   But it’s actually the case that all sentences that \mathrm{PA} proves are true.

By a result of Tarski’s we can’t define truth of an arithmetical formula in \mathrm{PA}, but we can define it by adding a new predicate \mathrm{True} to the language of \mathrm{PA}, together with suitable axioms.  The resulting theory \mathrm{PA}^{\mathit{True}}, extends every autonomous reflection extension of \mathrm{PA}.

In terms of what arithmetical sentences they can prove, \mathrm{PA}^{\mathit{True}} is an equivalent theory to \mathrm{ACA} (edit: not \mathrm{ACA}_0), which is the theory of second-order arithmetic, with a comprehension axiom for all arithmetic formulas.  This is essentially because sets of numbers in \mathrm{ACA} are interchangeable with formulas in the language of \mathrm{PA} with one free variable in \mathrm{PA}^{\mathit{True}}.

And, of course, we then get autonomous iterated truth extensions of \mathrm{PA}, in analogy to the autonomous iterated reflection extensions and the autonomous iterated consistency extensions.  Here there is again a natural theory which extends all the autonomous iterated truth extensions, a theory called \Pi^1_1-\mathrm{CA}: it’s a theory of second-order arithmetic, like \mathrm{ACA}, but it allows comprehension for \Pi^1_1-formulas (formulas with a universal set quantifier in front), instead of just arithmetic formulas.

Of course, we can now start again, taking consistency or reflection extensions of \Pi^1_1-\mathrm{CA}.  But, as Franzén says:

[E]xtending \mathrm{PA} to \Pi^1_1-CA opens the door to a number of possible extensions that go beyond reflection.  In particular, we can extend a theory by introducing axioms about sets of higher type—meaning sets of sets of natural numbers, sets of sets of sets of natural numbers, and so on—and by introducing stronger comprehension principles for sets of a given type. … Axiomatic set theories like \mathrm{ZF} give powerful first-order theories which prove everything provable in such iterated autonomous extensions. … In this connection the term “reflection” reappears and takes on a new meaning. … [This] leads to a further indefinite sequence of extensions of set theory, and furthermore, “axioms of infinity” [i.e., large cardinal axioms], have been formulated which can be reasonably argued to be stronger, as far as arithmetical theorems are concerned, than any such extension by set-theoretic reflection.

About these ads

7 Comments

Filed under Uncategorized

7 responses to “What Happens When You Iterate Gödel’s Theorem?

  1. That’s nice to see these thematic connections between things like ordinal notations and the theories used in reverse mathematics.

    You say that ACA0 is conservative over autonomous iterated reflection extensions, and Pi1-1 CA is conservative over autonomous iterated truth extensions. Is WKL0 conservative over autonomous iterated consistency extensions?

  2. On the matter of consistency, it seems fitting to link to an old post from Paul Taylor to the categories mailing list, exactly ten years ago today:

    http://www.mta.ca/~cat-dist/catlist/1999/zf-010499

  3. Pingback: New to the blogroll « Secret Blogging Seminar

  4. Todd: Thanks for the amusing link!

    Kenny: Thanks for your comment! First off, I made a mistake: I meant ACA, not ACA_0 (the former allows you to do induction on any formula, the latter only on formulas of the form “x is in S”.) ACA_0 is actually conservative over PA, so it doesn’t go anywhere up this hierarchy.

    Secondly, it’s not that ACA is conservative over autonomous iterated reflection extensions, it’s that it’s an extension of all of them, with the additional property that we believe that it’s true.

    If you had something that was conservative over some set of iterated reflection extensions, it would be reasonable to say that that theory was a reflection extension itself, and you could therefore take “one more step”. So, it’s hard to say that you have a theory which you know to be the union of all theories you know (or could know) to be reflection extensions. But there’s no problem with saying that you have a theory (which you believe to be true) which you know to be stronger than all theories which you know (or could know) to be reflection extensions.

    With regards to your second question about where WKL is in all of this, I actually have no idea.

  5. In the second-to-last paragraph, everywhere I said “theory”, I meant “recursively enumerable theory”.

  6. anonymous

    I think the forcing argument in SoSA that $WKL_0$ and $RCA_0$ have the same first order part (namely $I\Sigma_1$) can be used to show the same for $RCA$ and $WKL$.

  7. anon

    “However, we can make a reasonable definition for what it means for \mathrm{PA} (or any extension) to prove that a number a is an ordinal notation. (This is actually not trivial, since \mathrm{PA} can only talk about numbers, but the set of ordinal notations was defined to be the least set satisfying a certain property.) ”

    This is surprising, considering that the ordinal notations do not form an arithmetical, or even hyperarithmetical set. Would you mind explaining how it can be done?

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s