Non Higher-Order Formulation of Gödels Incompletness Theorem

Question

I was just having a look at Gödels incompletness theorem as found in: http://www.research.ibm.com/people/h/hirzel/papers/canon00-goedel.pdf

I noticed that Gödel used a higher order logic. At least such a logic was introduced via the Axioms IV and V in the above paper:

Axiom IV (looks to me like comprehension, but is called reducibility axiom): $$\exists u \forall v(u(v) \leftrightarrow a)$$

Axiom V (looks to me like extensionality, but is called type-lift/set axiom): $$\forall x_1(x_2(x_1) \leftrightarrow y_2(x_1)) \rightarrow x_2 = y_2$$

It looks to me higher order, since it uses the formulation $p(x)$ for a kind of member-ship. What alternative formulations are there around of Gödels incompletness theorem that don't make use of higher order logic. Will they be free of variables ranging over sets?

Best Regards

P.S.: I am looking for proofs that preserve the original content of Gödels proof. So I am not looking for later discovered proofs eventually not based on the same paradox.

Answer 1

There is nothing inherently higher-order in Gödel's original proof. The object theory in the proof is "$P$", which is based on the system of type theory from Principia Mathematica, but in principle there is no difficulty applying exactly the same techniques to first-order systems such as Peano arithmetic. The metatheory in Gödel's paper is entirely finitistic.

There are two reasons that the paper was written this way. First, there is an obvious motivation when presenting a new technique to pick some "well known" system to empirically demonstrate the applicability of the results. Because the system of Principia was well known at the time, using that system made it clear that the results could be applied to systems of real interest.

Second, and more important, there was no general definition of a "formal system" at the time that Gödel published the paper in 1931. The notion of computability would not be discovered for a few more years. When he wrote the paper on the incompleteness theorems, Gödel originally planned to write a second part that would contain generalizations of his theorems to other systems. The final paragraph in Gödel's paper states (from "From Frege to Gödel"):

In the present paper, we have on the whole restricted ourselves to the system $P$, and we have only indicated the applications to other systems. The results will be stated and proved in full generality in a sequel to be published soon. In that paper, also, the proof of Theorem XI, only sketched here, will be given in detail

After the paper was published, the results were accepted more readily than Gödel had hoped. Once the notion of computability was developed a few years later by Church and Turing, everyone immediately recognized that this was the key property needed to give a general definition of "formal system", and that the same techniques that Gödel used for $P$ would apply to any effective formal system. Therefore, the second part of the paper was never written, because it was so clear how to apply the same techniques of the 1931 paper to any effective formal system.