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?