Can we enumerate finite sequences which have no halting continuation? Note: this question has been cross-posted to Math.SE, after about a week here.

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 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.
Not an answer, but too long to be a comment:


  Specifically, as I understand it the Completeness 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.")


I'm not a logician so I don't know if the latter statement is true, but it's definitely not a restatement of the first statement.

The statement you quoted from Wikipedia says if you have countably many axioms and they're consistent then there exists at least one model of the theory with countably many elements. 

What Godel's completeness theorem says that if a statement is true then it has a proof.

What you're missing to bridge the two is "a statement true in every countable model is true in every model."  I don't know if this is true or not (logicians would probably know off the tops of their heads).