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) ?