7
$\begingroup$

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?

$\endgroup$

2 Answers 2

Reset to default
6
$\begingroup$

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.

$\endgroup$
4
$\begingroup$

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.

$\endgroup$
6
  • $\begingroup$ It is very disappointing! Isn't it? :-( $\endgroup$
    – Name
    Oct 3, 2015 at 14:21
  • 1
    $\begingroup$ What about computably axiomatisable theories? $\endgroup$
    – Zhen Lin
    Oct 3, 2015 at 14:23
  • $\begingroup$ I mean when you look at Henkins' approach in this (and other similar) non-constructive constructions, you really feel that there could be many other constructive ways to solve the problem but suddenly you understand that there is none and the issue will remain unsolved forever! The worst part of the problem is that choice plays a critical role here! $\endgroup$
    – Name
    Oct 3, 2015 at 14:39
  • 3
    $\begingroup$ @ZhenLin: In the sense of second-order arithmetic, and reverse mathematics, if I recall correctly the completeness theorem is only using the weak Koenig lemma. $\endgroup$
    – Asaf Karagila ♦
    Oct 3, 2015 at 14:44
  • 4
    $\begingroup$ Yes, the completeness theorem is equivalent to $\mathsf{WKL}_0$ over $\mathsf{RCA}_0$. On the pure computability side, we know that in general there is no computable nonstandard model of Peano arithmetic, but there are computable axiomatizations of PA + "$c$ is a nonstandard number". So we can't hope for computable models for effective theories, in general. On the other hand, if we assume the theory is decidable, then we can make a computable model. $\endgroup$
    – Carl Mummert
    Oct 3, 2015 at 15:03

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .