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?

Solution 1:

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.

Solution 2:

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.