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.

  • 2
    $\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 at 2:21
  • $\begingroup$ Please do not post the same question on multiple sites. Thank you! $\endgroup$ – D.W. Mar 15 at 23:20

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.

  • $\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 at 1:09

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.