What axioms are used to prove Gödel's Incompleteness Theorems?

Question

I understand Gödel'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.

Answer 1

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

Answer 2

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, RCA₀, 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, RCA₀ suffices for a large amount of mathematics.

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

Answer 3

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.

Answer 4

A very detailed, low-level proof of Gödel's incompleteness theorems is

• S. Świerczkowski, Finite sets and Gödel’s incompleteness theorems, Dissertationes Mathematicae 422 (2003), 1-58, https://eudml.org/doc/285944

It's based on the theory of hereditarily finite sets, which is closely related to PA.

Answer 5

Looking at this question again, it seems to reveal misconceptions about how mathematics is done in general and how it was done by Gödel. The key phrase is "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?"

Although mathematics can be formalised, it isn't usually, and Gödel's work was no exception. He makes no explicit reference to any axioms or rules of inference except with respect to the formal system that his theorem is about. The very notion of an algorithm was unclear in 1931. The Church–Turing thesis was still many years away. Gödel relied on well-known and elementary properties of arithmetic and ordinary mathematical reasoning to arrive at his conclusions.

You also remark "ZFC refers to all sorts of things I don't believe exist (e.g. non recursively enumerable sets, choice functions for uncountable families...)". The word "exist" is ambiguous here, but almost everything in mathematics is problematical once you think deeply about it: non-computable real numbers, planes (infinite in extent, perfectly flat, infinitely thin), parallel lines.