I have read Gödel's original paper (1930 - reprinted into J.van Heijenoort (editor), From Frege to Gödel: A Source Book in Mathematical Logic, 1879-1931, 1967) but I'm still unsatisfied with my understanding of it.
Modern logic textbooks usually prove the theorem following Henkin's construction.
One of the peculiarity of Henkin's proof is that the "completeness" aspect (i.e.if A is valid it is provable) is somewhat of a by-product of model existence.
Gödel's proof use (natural) numbers. This is obvious (with insight) today that we know about Gödel's philosophical realism.
Hankin's construction avoid numbers but use the "syntactical stuff" to build the model. But this (according to my understanding) is not really different; in order to "run" the construction we need countable many symbols, and symbols are "abstract entities" (like numbers). I think that we really needs them : we cannot replace them with "physical" tally marks. So my question :
In what sense we can minimize the "ontological" import of the theorem ?
In a previous effort I asked for some clarifications to a distinguished scholar and I received this answer : "About the completeness proof, it is a theorem of orthodox mathematics, and does not pretend to be nominalistic."