2
$\begingroup$

Note: this is a cross-post from CS.SE, since I haven't gotten an answer there.

I am trying to deepen my understanding of the relationship between the Halting Problem and Godel's Completeness Theorem (not Incompleteness).

Specifically, as I understand it the Completeness Theorem, together with the Lowenheim-Skolem Theorem, guarantees a finite proof for any first-order logical statement which holds in all countable models of a first-order theory. (This is my restatement of Wikipedia's "Every syntactically consistent, countable first-order theory has a finite or countable model.")

Since the statement "Program $P_n$ (encoded by integer $n$) does not halt" can presumably be stated in first-order logic and cannot in general be proven, we need to understand why (for given $n$) it does not hold in all countable models.

Intuitively, I expect that any countable model can be encoded as an infinite program for a Turing machine, eg by listing the countable set of first-order propositions. Likewise, I expect that any such "infinite Turing machine" can be identified with a countable first-order theory, by the Church-Turing thesis plus induction.

So, just as the Completeness Theorem fails to "solve" arithmetic because of non-standard models with infinite integers (which eg satisfy otherwise unsatisfiable Diophantine equations), I'm speculating that it fails for Turing machines because of non-standard models with "infinite programs".

But by my understanding statements which are true in all models (including non-standard / infinite ones) should still be provable. So I expect that if some finite set of axioms, which "pins down" some finite set of digits of a potentially infinite program, is enough to prevent the possibility of halting, we should be able to prove it.

Or in other words, if a finite sequence does not have any continuation which encodes a halting program, that should be provable.

Does my logic hold? Or what am I misunderstanding?

The reason this is not trivially wrong by Rice's Theorem is that it's a property of the program itself, rather than the language recognized by that program, which is $\emptyset$ for the programs I'm talking about.

$\endgroup$
2
  • 3
    $\begingroup$ Since you're looking at statements "Program $P_n$ does not halt" with specified $n$, you're not dealing with an infinite program. But you might get, in some nonstandard model, an infinitely long halting computation. (More precisely, that's a nonstandard element of your model that satisfies, in that model, the formula saying it's a halting computation of $P_n$.) $\endgroup$
    – Andreas Blass
    Feb 13, 2019 at 2:21
  • $\begingroup$ Please do not post the same question on multiple sites. Thank you! $\endgroup$
    – D.W.
    Mar 15, 2019 at 23:20

1 Answer 1

Reset to default
0
$\begingroup$

The answer to your question has to be no. The finite sequences that do encode a machine that halts form a recursively enumerable set that is not recursive, so its complement (finite sequences encoding a machine that does not halt) cannot be either recursively enumerable or recursive.

$\endgroup$
1
  • $\begingroup$ I agree we cannot enumerate programs that do not halt, that is simply the halting problem. My question is about a subset of non-halting programs, that also cannot be made to halt by extending them. $\endgroup$
    – user3461142
    Feb 13, 2019 at 1:09

You must log in to answer this question.

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