Non Higher-Order Formulation of Gödels Incompletness Theorem 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?
 A: 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. 
A: 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
Link
