Some questions about “deep” implications of Gödel's Completeness Theorem (if any)

Question

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 ?

Answer 1

First, the standard proof of the completeness theorem is indeed nonconstructive, and necessarily so. It is known that there are computable consistent sets of axioms that do not have computable models. Therefore, any proof that every consistent set of axioms has a model will have to use techniques that allow for the creation of noncomputable sets.

Gödel's original proof does not help in this respect. Indeed, it is somewhat less amenable to a constructive interpretation, because it relies on a kind of Skolem functions, which move us into higher types, while Henkin's method does not require Skolemization. There is a good description of Gödel's original argument in this paper by Jeremy Avigad.

Second: there are indeed completeness theorems for intuitionistic logic. But the semantics are very different in that setting, because the logics are not amenable to 2-valued truth functions. In fact, the situation is more complicated in non-classical logic. In classical first-order logic, we have essentially only one semantics, the one that uses first-order structures. There are minor variations, but they all come down to the same thing. In intuitionistic logic, there are several quite different semantics: topological semantics, Kripke models, and realizability are three important ones. There are some connections between these, to be sure, but they vary far more than just different presentations of the same thing, as with classical first-order logic.

There is also an issue with intuitionistic logic that some actual intuitionists (or constructivists, more generally) do not accept that their reasoning can be adequately captured in any formal system. They resist the urge to formalize their work, and so they would not accept that any completeness theorem for a formalized intuitionistic logic is applicable to their own reasoning.