Original proof of Gödel's completeness theorem compared to Henkin's proof May I have some clarification about original proof of Gödel's Completeness Theorem compared to "standard" Henkin's proof based on Model Existence Lemma ?
My understanding of Gödel's original proof is this :
1) Perform some syntactical transformation, in order to reduce the general problem to a particular class of wffs
2) Build an assignment of object to te free vars of the "reduced" formula in order to satisfy it. The assignment is built up using n-uples of natural number corresponding to index of the free vars.
3) The last step is made using some sort of König's Lemma.
From a "philosophical" perspective, Gödel made two assumptions (in line with his "platonism") : the existence of natural number and some properties of infinite sets (König's Lemma).
The Henkin proof needs (if I remember well) Zorn's Lemma and build up the model using only "syntactical objects" : the constants of the language as witnesses.
There are also other proofs (based on Ultrafilters) but they are (for me) less transparent then Henkin's one.
So it seems to me that the theorem needs a "big amount" of set theory. Is it true ? If so, this fact gives us some information about the foundational issue regarding first-order logic and higher-order logic (according to Quine : not "real" logic at all, but set theory in disguise) ?
thanks
 A: With regard to the amount of set theory required to prove the completeness theorem, the wikipedia page on The completeness theorem asserts:


When considered over a countable language, the completeness and compactness theorems are equivalent to each other and equivalent to a weak form of choice known as weak König's lemma, with the equivalence provable in RCA0 (a second-order variant of Peano arithmetic restricted to induction over Σ01 formulas). Weak König's lemma is provable in ZF, the system of Zermelo–Fraenkel set theory without axiom of choice, and thus the completeness and compactness theorems for countable languages are provable in ZF. However the situation is different when the language is of arbitrary large cardinality since then, though the completeness and compactness theorems remain provably equivalent to each other in ZF, they are also provably equivalent to a weak form of the axiom of choice known as the ultrafilter lemma. In particular, no theory extending ZF can prove either the completeness or compactness theorems over arbitrary (possibly uncountable) languages without also proving the ultrafilter lemma on a set of same cardinality, knowing that on countable sets, the ultrafilter lemma becomes equivalent to weak König's lemma.


