# Non Higher-Order Formulation of Gödels Incompletness Theorem

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.

-
An approach to Gödel's theorem in first order logic which maintains essentially the same proof states that first-order Peano Arithmetic is not complete (there are theorems independent of the axioms) and any axiomatic extension of it which is $\omega$-consistent is likewise not complete. The $\omega$-consistency requirement is rendered redundant if one uses Rosser's trick (essentially creating a sentence that instead of asserting it's own unprovability states that its negation is proven with a proof-number smaller that its own proof-number). – Apostolos Feb 8 '11 at 14:21
Sorry, I misread your question. The mention of axioms of higher order logic have to do with the logical system that Gödel proves incomplete rather than with the axioms he will use. My knowledge on the history of mathematics is limited but I think that Gödel's proof was about Russell's theory of types which was a system that used higher order logic. I haven't read the original paper to know exactly what part of a logical system Gödel used. But (regarding your question) Gödel's theorem can be very easily turned into a theorem of first-order ZFC. – Apostolos Feb 8 '11 at 16:03
@Jan: I'm sorry, I don't know about that. – Apostolos Feb 8 '11 at 17:30
I asked a similar question on MO some time ago, and got several nice answers. – Sebastian Reichelt Mar 6 '11 at 23:49
Sorry, I may have misread your question in the same way that Apostolos has, and apparently also Carl Mummert. :-) Because I just found this MO post where he says that PRA is sufficient as a metatheory. (Regarding the doubts you express below: Note that you can often encode "higher-order" mathematical objects as numbers.) – Sebastian Reichelt Mar 13 '11 at 17:34

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.

-
Yes, universal quantifiers over the natural numbers are finitistically unproblematic. For example, this is the only type of quantification in primitive recursive arithmetic, which is generally considered to be a finitistic theory, and which is strong enough to serve as a metatheory for the incompleteness theorems. – Carl Mummert Feb 13 '11 at 0:28