0
$\begingroup$

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.

$\endgroup$

3 Answers 3

1
$\begingroup$

The language of your question confuses me a bit ("if a finite sequence does not have any continuation which encodes a halting program" - what exactly does that mean?), but I think the following is likely to clarify the situation:

Let's take as our "base theory" first-order Peano arithmetic, $\mathsf{PA}$. We could use pretty much any reasonable theory here, but $\mathsf{PA}$ has the advantage of being broadly known, so I'll use it. Let $(M_e)_{e\in\mathbb{N}}$ be some fixed usual enumeration of Turing machines. The following is indeed true:

  • The set $$\mathsf{MustHalt}=\{n\in\mathbb{N}: \mbox{Every model of $\mathsf{PA}$ thinks $M_n$ halts on input $n$}\}$$ is c.e., by the completeness theorem.

  • The set $$\mathsf{Can\mbox{'}tHalt}=\{n\in\mathbb{N}: \mbox{No model of $\mathsf{PA}$ thinks $M_n$ halts on input $n$}\}$$ is also c.e. by the completeness theorem, and disjoint from $\mathsf{MustHalt}$ (I'm assuming $\mathsf{PA}$ is consistent here obviously).

  • However, the set $$\mathsf{MightHalt}=\mathbb{N}\setminus(\mathsf{MustHalt}\cup\mathsf{Can\mbox{'}tHalt})$$ is not c.e.; indeed, $\mathsf{MustHalt}$ and $\mathsf{Can\mbox{'}tHalt}$ are computably inseparable, and $\mathsf{MightHalt}$ is co-c.e.-complete exactly as each of the former is c.e.-complete.

The second bulletpoint above is, perhaps, an affirmative answer to your question. But the third bulletpoint should stress the difficulty of drawing strong conclusions from that: the c.e.-ness of halting prevention is not, actually, that sweeping a phenomenon (indeed by Godel's incompleteness theorem it can't possibly be).

$\endgroup$
0
$\begingroup$

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.

This is untrue, which may be a part of your confusion: in certain countable (but non-standard) models of arithmetic, even the interpretation of operators like $+$ and $\times$ may be non-computable, see for example Tennenbaum's theorem.

$\endgroup$
1
  • 1
    $\begingroup$ I so want to use this as the excuse for my next arithmetic screw-up. $\endgroup$ Feb 13, 2019 at 19:50
-1
$\begingroup$

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

$\endgroup$
4
  • 1
    $\begingroup$ By my understanding, your "missing link" is provided by the Lowenheim-Skolem Theorem: any statement not true in some model is also not true in some countable model. $\endgroup$
    – user271667
    Feb 10, 2019 at 1:40
  • $\begingroup$ My "restatement" uses the following logic: given any first-order statement $S$ which holds in all countable models of a countable first-order theory $T$, the theory $T\wedge\neg S$ has no models, therefore is not syntactically consistent, which is a finitely-provable fact $\endgroup$
    – user271667
    Feb 10, 2019 at 1:55
  • $\begingroup$ Not enough of a logician to keep up. You may want to try this question on math.SE where there are more actual logicians hanging around. $\endgroup$ Feb 11, 2019 at 13:51
  • $\begingroup$ Thanks, I'll probably wait a few days then try that $\endgroup$
    – user271667
    Feb 11, 2019 at 15:47

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.