# 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?

-
One theory is T=(PA+(axiom PA is incomplete)) – user1708 Jan 22 '11 at 13:24

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).

-
Thanks a lot, Andres! But did I understand correctly: The incompleteness of PA can rigorously be proved (in a FO context, just with a - maybe infinite - set of axioms and modus ponens) in a theory that is strictly weaker than PA? Or did I misread your answer? – Hans Stricker Jan 20 '11 at 15:45
Or did I make stronger and too strong assumptions in my comment than in my question? (You are not explicit about FO-ness and rules of inference.) – Hans Stricker Jan 20 '11 at 16:09
Hans: one of the key points in Andres' answer that I think you missed is that the incompleteness isn't proven in PA - rather, 'PA's consistency implies its incompleteness' is the statement proven. To apply Modus Ponens and then prove proper incompleteness you (obviously?) need a theory stronger than PA to prove the left side of the implication, but the implication itself can be proven in a weaker theory. – Steven Stadnicki Jan 20 '11 at 16:55
And yes, all the theories here are first order (even the "second order systems" I talk about can be formalized in a first order setting using what is called a two-sorted language). – Andrés E. Caicedo Jan 20 '11 at 19:57
@Steven: Did you mean "that the incompleteness isn't proven in PA" or "that the incompleteness isn't proven for PA"? And how do I see which theory I need to prove the left side (consistency)? – Hans Stricker Jan 21 '11 at 9:11