I'm trying to refresh my knowledge about mathematical logic and I'm still unsatisfied with my insight of Gödel's Completeness Theorem.
I've studied Henkin's version and I think I've mastered it. Some textbooks (e.g.Ian Chiswell & Wilfrid Hodges, Mathematical Logic (2007), introduce Henkin's construction with sentential logic, I think in order to "introduce" the student to the construction "testing" it in a simplified environment.
1) Make it sense trying to adapt Gödel's original proof to sentential calculus in order to understand the specific details necessary to prove it for f-o logic ?
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. We have "extreme" cases, like Boolos & Burgess & Jeffrey, Computability and Logic (5th ed - 2007), where the Model Existence give Compactness in advance of the introduction of any proof systems, and the Completeness Theorem is "fairly missing". In this way, the non-constructive aspects of the theorem are "maximized".
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 :
2) 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."
I've not studied Intuitionistic logic, but I know that there are semantics for it.
3) Are there "completeness" (linking semantics to proof systems) theorems for f-o intuitionistic logic ? What about their non-constructive aspects (if any) ?
What is the opinion of constructivistic mathematicians (not necessarily intuitionists) about Gödel's or Henkin's proof, and what about corresponding result (if any) for intuistionistic f-o logic ?