# What axioms Gödel is using, if any?

Gödel states and proves his celebrated Incompleteness Theorem (which is a statement about all axiom systems). What is his own axiom system of choice? ZF, ZFC, Peano or what? He surely needs one, doesn't he?

• You can find online several transaltions: here and here. Jan 23 '18 at 19:50
• And here the German original. Jan 23 '18 at 19:52
• His original paper only proved the existence of undecidable propositions in one axiom system (PM - that of the Principia Mathematica), but it used a very generic process to make that proof work, so it is obvious that it can be made to work on a wide class of systems. That isn't the question you quite asked, but it does contain an assumption that he was proving a more general result than he was. Jan 23 '18 at 21:28
• This question is better than it seems. Gödel has some kind of hidden assumption. I have two possible candidates but the more likely one to be correct is hard to state, kind of like the "in a finite number of steps" limitation of trisecting an angle. Jan 24 '18 at 2:47
• Although he didn't use one at the time, modern treatments can use PRA, if one likes. Jan 24 '18 at 3:07

Gödel's paper was written in the same way as essentially every other mathematical paper. To prove a theorem about a formal system does not require one to prove that theorem within a formal system. Gödel argued in his paper that the incompleteness theorem should be viewed as a result in elementary number theory, and he certainly proved the incompleteness theorem to the same standard of rigor as other results in that area.

Of course, we now know that the incompleteness theorem can be proved in extremely weak systems, such as PRA (primitive recursive arithmetic), a theory much weaker than Peano arithmetic. But, at the time that Gödel wrote his paper, the definition of PRA had never been formulated.

Even Gödel's theorem, as he stated it at the time, was for a particular formal system "$P$" rather than for effective formal systems in general, because the definition of an "effective formal system" had not yet been compellingly formulated. Remarkably, it took well into the 20th century before many of the the now-standard concepts of logic were clearly understood.

• I partly disagree with the historical details. See van Heijenoort's edition of Gödel (1931). Page 599 for the "syntactical specifications" of the formal system $\text P$; page 600 for the axioms; page 602 for the definition of recursive function (now primitive recursive; see footnote 34, page 603: the quantifiers are implicitly bounded). Recursive number theory was well know to members of Hilbert's school, following Skolem (1923) (reprinted in van Heijenoort, page 312), and "codified" into Hilbert and Bernays (1934). Jan 24 '18 at 9:06
• Gödel certainly did use a specific system $P$ in his paper; at that point,however, he did not formulate a general notion of an effective formal system and prove the incompleteness theorem for that class of systems. I would be interested to know the first time that the theory PRA was fully specified in print (by which I mean giving a modern definition of a first-order theory of arithmetic including a precise definition of the signature and axioms). Jan 24 '18 at 12:28
• In his 1934 lectures at IAS, Gödel said, "due to A.M. Turing’s work a precise and unquestionably adequate definition of the general concept of formal system can now be given, the existence of undecidable arithmetical propositions and the non-demonstrability of the consistency of a system in the same system can now be proved rigorously for every consistent formal system containing a certain amount of finitary number theory." I have always read that with emphasis on the "now", indicating that Gödel did not feel he had a precise definition of the "general concept of formal system" in 1931. Jan 24 '18 at 12:31

As a footnote to Carl Mummert's terrific answer, it is worth adding the following remark.

Yes, Gödel was giving an informal mathematical proof "from outside" (as it were) about certain formal systems. And yes, he is not explicit about what exactly his proof requires to go through.

However, it was very important to him at the time that his proof used only very elementary constructive reasoning that would be acceptable even to e.g. intuitionists who did not accept full classical mathematics, and equally to Hilbertian finitists who put even more stringent limits on what counted as quite indisputable mathematical reasoning. (After all, he couldn't effectively challenge Hilbert's program by using reasoning that wouldn't be accepted as unproblematic by a Hilbertian!)

So although Gödel doesn't explicitly set out what exactly he is assuming, we are supposed to be able to see by inspection that nothing worryingly infinitary or otherwise suspect is going on, and that -- although his construction of the Gödel sentence for his system $P$ is beautifully ingenious -- once we spot the trick, the reasoning that shows that the sentence is formally undecidable in $P$ is as uncontentious as can be (even by the lights of very contentious intuitionists or finitists!), so falls way short of what it would require the oomph of classical ZF (or even full classical PA) to formalize.