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

In particular, is stronger than .  But certainly, given that we believe that everything proves is true, we believe that does not prove a contradiction, and hence is consistent.  Thus, we believe that everything that proves is true.  But by a similar argument, we believe that everything that proves is true.  Where does this stop?  Once we believe that everything 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  be , and let  be .  By the considerations above, we accept that each is sound.  (A theory being sound means that everything it proves is true.)

So, if we therefore let , then we accept that is sound.  We could therefore define to be 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 in the language of number theory, we much choose some recursively enumerable presentation of , and which recursively enumerable presentation we choose matters.  For example, if we add to any given presentation of the stipulation that we are adding, for all and such that the axiom , then we haven’t actually added any new axioms, but if we construct the statement with presented the second way, will imply Fermat’s Last Theorem, while constructed from the original presentation of may not.

As you might guess from the above, we are going to want to construct for ordinals .  When is a successor ordinal, it is clear how to get a “reasonable” presentation of from a reasonable presentation of (where ), but if is a limit ordinal, in general it won’t be clear (although it is clear for ).

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 with the following property: It is either 0, or for every , the output of the th Turing machine on input 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 , we let the ordinal it represents, , be defined by and , where denotes the output of the th Turing machine on input .

We can now uniformly pick presentations of for ordinal notations by letting and be presented as the union of over , 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 sentence , there is an ordinal notation such that and proves .  The catch is that will be quite an unusual notation for 1, and we’re not really justified in taking to be a consistency extension of because doesn’t “know” that is an ordinal notation.

However, we can make a reasonable definition for what it means for (or any extension) to prove that a number is an ordinal notation.  (This is actually not trivial, since 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 as follows: is an autonomous consistency extension of itself, and if is an autonomous consistency extension of , and proves that is an ordinal notation, then is an autonomous consistency extension of .

The autonomous consistency extensions of have some claim to being exactly those that we recognize to be consistency extensions of solely on the basis that we accept .  But that isn’t really completely satisfying.  There’s nothing stopping us from letting be the union of the autonomous consistency extensions of and considering .  Similarly, we got the set of autonomous consistency extensions of by starting with 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 proves?  It turns out there is.  Let be the theory obtained by adding to the axiom that for any sentence (that is, sentence of the form where all of ‘s quantifiers are bounded), if proves , then is true.

This property is called -soundness, and the axiom formalizing it is called a reflection axiom.  If is -sound, then so is , since if proved a false statement , then would prove the false statement (false because -soundness implies consistency).  Similarly, any union of a chain of -sound theories must be -sound.

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

Okay, so adding axioms asserting that is -sound takes us beyond all the autonomous consistency extensions of .  But what happens if add to axioms asserting that is -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 goes beyond all the autonomous consistency extensions of ?  There is. The theory asserts that all sentences that proves are true.   But it’s actually the case that all sentences that proves are true.

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

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

And, of course, we then get autonomous iterated truth extensions of , 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 : it’s a theory of second-order arithmetic, like , but it allows comprehension for -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 .  But, as Franzén says:

[E]xtending to 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 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.