What's the theory in which incompleteness of PA is proved?

Maybe this is a dumb question, but I have to admit that it is not really clear to me what the theory is, in which incompleteness of PA and stronger theories is proved. The texts I did study so far are often not really explicit about that.

What's the (minimal) theory in which incompleteness of PA and stronger theories is proved?

Solution 1:

Let PRA be the theory of Primitive recursive arithmetic. This is a subtheory of PA, and it suffices to prove the incompleteness theorem. It is perhaps not the easiest theory to work with, but the point is that a proof of incompleteness can be carried out in a significantly weaker system than the theories to which incompleteness actually applies. It is sometimes argued that Hilbert's notion of finitism is (as precisely as possible) captured by PRA, so in that sense, this is the ideal setting for proving the incompleteness of PA or related systems.

You may benefit from reading the nice book Metamathematics of first order arithmetic by Hájek and Pudlák, where these matters are carefully discussed, as well as some of the numerous essays by Harvey Friedman, available at his homepage.

Let me point out that what one proves in PRA is that either PA is inconsistent or else, it cannot prove its own consistency (and therefore it is incomplete). If we actually want to prove that PA is incomplete, we need to reason within a system where Con(PA), the formal statement asserting the consistency of PA, is assumed. (Of course, Con(PA) is not a theorem of PA, so in a sense this is a strong assumption.) Similarly, PRA suffices to formalize the incompleteness of much stronger systems, and even, to formalize the equiconsistency results of set theory.

Some people prefer to be able to reason with sets (i.e., semantically, rather than with formal proofs, that are syntactic objects) in a less cumbersome fashion than via coding. Then, rather than working with PRA, it is convenient to work with a weak subsystem of second order arithmetic. Typically, WKL${}_0$ (A system that allows us to prove a weak version of König's lemma that finite branching infinite trees have infinite branches) is the chosen system to carry out the formalization of the incompleteness proofs. A good place to learn about this and second order arithmetic in general is the wonderful book by Stephen Simpson.

Let me mention that subsystems of second order arithmetic are understood to be the natural theories to carry out investigations on reverse mathematics, i.e., they provide precisely the setting one wants in order to study questions about what formal systems suffice to prove a theorem (such as the incompleteness of PA, in this case).