What axioms are used to prove Godel's Incompleteness Theorems?

I understand Godel's Incompleteness Theorems to be statements about effectively generated formal systems, which basically makes them theorems about algorithms. This is cool, because despite being very abstract, they actually constrain my expectations about how computers and human beings can behave. But, being theorems, what formal system are they theorems in? That is, what formal language is used to express them, how do I interpret that language as being about algorithms, what axioms are assumed, and what rules of inference are used to derive the incompleteness theorems?

I ask because I am looking for a better answer than "ZFC", which has been given to me in person a few times now. ZFC refers to all sorts of things I don't believe exist (e.g. non recursively enumerable sets, choice functions for uncountable families...), at least not in the same way I believe in concrete things like computers and algorithms. I can see from skimming the proofs that I could probably make up a formal system in which the theorems could be expressed and proven, which did not refer to all the monstrosities of ZFC. I just want to know what standard, "simplest" formal system(s) can be used for this purpose.

• PRA, en.wikipedia.org/wiki/Primitive_recursive_arithmetic, suffices. Jan 6 '13 at 6:34
• Also, note that the theorems apply to Robinson Arithmetic, which is weaker than Peano. Jan 6 '13 at 7:55
• @Andrew Critch: The article on the incompleteness theorems in the Handbook of Mathematical Logic, by Smorynski, has the details. Look for the term "formalized incompleteness theorem". Jan 6 '13 at 23:21
• @Andrew: Historically, there's a good reason why PRA suffices. In the background was lurking Hilbert's program to dispel doubts about infinitary set-theoretic reasoning by proving the consistency of set theory by finitary means. Since Goedel was claiming to demonstrate the impossibility of a finitary consistency proof (though not, initially, of set theory), he had good reasons to restrict his own arguments to finitary ones, to forestall criticism of his own proof. Your suspicions about infinitary reasoning are not new! Jan 7 '13 at 4:08

As Andres Caicedo points out in his comment (to the Question), the modest fragment $\sf{PRA}$ (Primitive Recursive Arithmetic) of $\sf{PA}$ (Peano arithmetic) is already is able to verify the incompleteness theorems.

Indeed, the proof of the Gödel-Rosser incompleteness proof is entirely syntactic and can be readily implemented in a fragment of $\sf{PRA}$ known as $I\Delta_0 + exp$, where $I\Delta_0$ is the weakening of $PA$ in which the induction scheme is only available for $\Delta_0$-formulas, and $exp$ asserts the totality of the exponential function $2^x$ (it is well-known that $I\Delta_0$ is unable to prove the totality of the exponential function).

It is worth noting that in the above $I\Delta_0 + exp$ can be even reduced to $I\Delta_0 + \Omega_1$, where $\Omega_1$ is the axiom asserting the totality of the function $2^{\left| x\right|^2 }$, where $\left| x\right|$ denotes the length of the binary expansion of $x$. The theory $I\Delta_0 + \Omega_1$ is commonly viewed as the weakest fragment of $\sf{PA}$ in which one can develop a workable "theory of syntax".

PS. As pointed out by Jeřábek, the incompleteness theorems can be implemented in even weaker systems.

• Really $2^{|x|}$, not $2^{|x|^2}$? Jan 6 '13 at 12:54
• @Andrew: The second paragraph is not a quotation; the highlighting was used for journalistic reasons. The standard reference on the subject is the book "Metamathematics of First-Order Arithmetic" by Petr Hájek, and Pavel Pudlák (1998) [see the first chapter for $I\Delta_0 + exp$, and the last chapter for $I\Delta_0 + \Omega_1$]. This book is available on Project Euclid at projecteuclid.org/…. Jan 6 '13 at 16:15
• @Martin: Thanks, I fixed the def. of $\Omega_1$. The right one is between what I had written and what you suggested; see p.272 of the Hájek-Pudlák text mentioned in my comment to Andrew (it is in Ch. V of the book). Jan 6 '13 at 16:23
• @Ali: Goldstern is right. Your definition is an inessential variant of $x^2$, and is provably total in $I\Delta_0$. Jan 7 '13 at 14:22
• And of course, the incompleteness theorem is provable in much weaker fragments than $I\Delta_0+\Omega_1$, such as $\mathit{PV}_1$. Jan 7 '13 at 14:26

You might already know this, but if you're looking for foundations of mathematics which are so weak that they don't prove the existence of non-r.e. sets, then you should study Simpson's book Subsystems of Second-Order Arithmetic, the "bible" of reverse mathematics. The weakest system in that book, RCA0, has as a model the recursive sets, and suffices for Goedel's first incompleteness theorem and even a weak version of Goedel's completeness theorem. More importantly, RCA0 suffices for a large amount of mathematics.

Simpson's book of course also investigates what can't be proved in RCA0. For example, Brouwer's fixed point theorem is unprovable in RCA0, roughly speaking because one can construct a continuous recursive map from the square into itself that has no recursive fixed point.

• If the OP is averse not only to non-r.e. sets but also to non-recursive r.e. sets, then $\text{RCA}_0$ is indeed a good system for him to work with. His explicit mention of "non-r.e." leads me to suspect, though, that he might want to have all r.e. sets available, so he'd need a system where one cannot in general form the complement of a set of natural numbers. Jan 7 '13 at 1:37

Here's a different way of looking at things. Use FPA to denote second-order Peano Arithmetic minus the Successor Axiom (the axiom which says that every natural number has a successor). FPA is neither weaker nor stronger than IΔ0+Ω1, since the latter assumes the Successor Axiom but assumes a weaker form of induction.

FPA can prove the First Incompleteness Theorem. Undoubtedly, fragments of FPA can as well.

More interesting is when one clarifies the nature of the logical system under metalogical study. Usually, the syntax of first-order logic is defined so that one can always concatenate two strings to form a larger one. E.g. one uses this principle in the Deduction Theorem, which is one of the first metalogical theorems one tends to prove. But this assumption, essentially equivalent to the Successor Axiom, is not necessary, and one can refrain from making it.

In this environment (where the syntax is not assumed to be unboundedly long), one can say this: FPA can prove the First Incompleteness Theorem. But Godel's proof seems only to work in the case of FPA + Successor Axiom. In the case FPA + not Successor Axiom, one basically formalizes the idea that a proof is generally longer than any axiom. It does not appear that Godel's proof of the Second Completeness Theorem goes through, and I do not know whether this can be repaired.

• Cool; what's a reference where I can see this proven, or at least illustrated? Jan 6 '13 at 15:14
• – abo
Jan 6 '13 at 18:10
• @abo Link is broken. Aug 18 '21 at 21:09
• @user76284 A new link: researchgate.net/publication/354021536_THREE_THEOREMS_OF_GODEL
– abo
Aug 20 '21 at 4:25

A very detailed, low-level proof of Gödel's incompleteness theorems is "Finite sets and Gödel’s incompleteness theorems". It's based on the theory of hereditarily finite sets, which is closely related to PA.

• Several users consider this as a non-answer to the actual question. Dec 24 '13 at 23:26
• This is not a non-answer. Świerczkowski shows that the proof of Gödel's theorem can be formalized in a set-theoretic system much weaker than ZFC, and this proof was the starting point for Lawrence Paulson's formalization of the theorem in Isabelle/HOL. See Paulson's paper, "A Machine-Assisted Proof of Gödel's Incompleteness Theorems for the Theory of Hereditarily Finite Sets," which he seems to be too modest to mention himself. Dec 25 '13 at 1:51
• Thank you very much, @TimothyChow, for the clarification and information. Dec 25 '13 at 2:12
• The link in this answer no longer works. Apr 24 '19 at 13:20