4
$\begingroup$

I was just having a look at Gödels incompletness theorem as found in:
https://www.ii.uni.wroc.pl/~kosciels/pi/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.

Edit 12.05.2018: There is one more higher order axiom in Gödels formalization of his subject logic, burried in footnote 21 in the original paper. See also here:
How do we get the converse of extensionality in Gödel's 1931 system?

  • 0
    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](http://mathoverflow.net/questions/24874/what-is-the-reverse-mathematics-of-first-order-logic-and-propositional-logic/24882#24882) 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.)2011-03-13

2 Answers 2

10

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.

  • 1
    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.2011-02-13
0

I only found the following more technical explanation
what is going on in Gödels proof (from (*) p.160):

(b) Gödel's First Incompleteness Theorem and Related Topics Fixed points theorems are particularly fruitful when applied to formulas related to the set of all T-proofs or the set of all T-provable formulas (where T is a theory containing Q). If T is rich enough to make arithmetization possible (IΣ_1 subset T suffices) then it is natural to work with the formalized proof predicate Proof* (see Chap. I, Sect. 4); but for Gödel's first incompleteness theorem it suffices that T contain Q and that the set of all proofs is Δ_1 and hence has a Σ_1 binumeration. (Gödel's second incompleteness theorem is more delicate and to prove it we have to guarantee some provability conditions, see below.) The theorems are proved in a constructive way, i.e. we give examples of sentences that are independent (neither provable nor refutable). Since these examples are both famous and useful we give their names (Gödel's formula, Rosser's formula).

Lets only look at the first incompletness theorem.
I guess working with the weak requirement T contains
Q only works when we switch to the meta-meta level.

Bye

(*) Metamathematics of First-Order Arithmetic Petr Hájek, and Pavel Pudlák Perspectives in Mathematical Logic, Volume 3 Berlin: Springer-Verlag, 1998. 2nd printing http://projecteuclid.org/DPubS?service=UI&version=1.0&verb=Display&handle=euclid.pl/1235421926