# Can we enumerate finite sequences which have no halting continuation?

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.

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