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.
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.