Is there a constructive approach as a replacement of Henkin's construction?

Question

Henkin's proof for Goedel's completeness theorem that is based on the Henkin construction using term models built by constants is not constructive.

My question is whether there is any constructive approach as a replacement of Henkin's construction? If not, is it possible to prove that there is no such constructive proof at all?

Answer 1

Since the completeness theorem for first-order logic, in its generality, is equivalent to the Boolean Prime Ideal theorem, and the latter is not provable without the axiom of choice... the answer is no.

There is no way to fully write down a constructive algorithm in that case.

Answer 2

On the pure computability side, classically, we know that there are effective theories that are consistent but have no computable model. For example, there are no computable nonstandard models of PA, but there is an effective axiomatization of PA + "$c$ is a nonstandard number".

So we cannot hope, in general, to have a computable model for each effective theory. If there was a fully constructive proof of the completeness theorem, on the other hand, then we would expect the completeness theorem to be "computably true", because it is impossible in most systems of constructive mathematics to prove the existence of a subset of $\mathbb{N}$ without that subset being computable (this is a consequence of the technique of "realizability" in proof theory).

We can ask how uncomputable the models constructed by the completeness theorem need to be, if they don't need to be computable. In general, the set of countable models of an effective theory is always a $\Pi^0_1$ class, and so the low basis theorem shows that if an effective theory is consistent then it has a model $X$ such that the Turing jump of $X$ is $\emptyset'$, which is the smallest the jump could be.

In general, a Turing degree is called a PA degree if it is able to compute an element of every nonempty $\Pi^0_1$ class. Equivalently, and nonobviously, these are the degrees that can compute the theory of a complete extension of Peano arithmetic. So it turns out that the problem of being able to find a model of each constent effective theory is no worse than the problem of being able to find a completion of Peano arithmetic.

In the context of Reverse Mathematics in second-order arithmetic, the existence of a completion of PA, and the completeness theorem for countable first-order theories, are both equivalent to $\textsf{WKL}_0$ over $\textsf{RCA}_0$. This is really just a reflection of the computability theoretic facts above, though.