The halting problem solved if there is an effective positive test for first-order entailment?

Question

given any Turing machine m and any input n, we can construct a finite set of sentences ∆ and a corresponding sentence H, halting sentence, such that ∆ ⊨ H iff TMm eventually halts on input n. Thus if there were an effective method for determining that ∆ ⊭ H then we could solve the halting problem and thereby refute the Church-Turing Thesis. If we know that there is an effective positive test for first-order entailment, can we solve the halting problem by considering the negation of the halting sentence, viz. ∆ ⊨ ¬H?

Answer 1

There is an effective positive test for first order entailment: enumerate proofs until you find one. And no, this doesn’t solve the halting problem. There is no guarantee that we can prove that a non-halting machine doesn’t halt. (In other words, no guarantee that $\Delta\models \lnot H$ in the first place.)

Answer 2

I'm not sure what you mean by “entailment”. But I think the answer to your questions is essentially ‘yes’. Say we're given a turing machine $M$ and a string $s$. Suppose we could construct a set $\Delta_{M,s}$ of first-order formulas that expresses the statement “Machine $M$ halts on input $s$”. That is, $$\Delta_{M,s} \vDash H(M, s). $$

We can in fact construct such a set of formulas; that's not the problem. Doing this is straightforward! Then if we could prove the formulas, we would know that the machine halted.

The problem is, the formulas don't help, because we there is no way to find out (in general) whether $\Delta_{M,s}$ is provable, or not.

There is a procedure that will tell us if $\Delta_{M,s}$ is provable: enumerate every possible proof, and check each one to see if the thing it proves is $\Delta_{M,s}$. But if $\Delta_{M,s}$ is not provable, this procedure fails to halt. So it's no better in general than just running the machine and waiting to see if it halts.

Is there a procedure that is guaranteed to tell us if $\Delta_{M,s}$ is not provable? In particular cases there is; just try to prove the negation of $\Delta_{M,s}$, and if you succeed, then $\Delta_{M,s}$ is false and therefore not provable. Then we would know that $M$ won't halt. But this doesn't work in general because we may not be able to prove either $\Delta_{M,s}$ or its negation.

And how do we know that such cases exist? Easy: if either $S$ or $\lnot S$ was provable for every $S$, we would be able to solve the halting problem, and we know we can't.

---

I'm not sure if this will help or just cause more confusion, but this comment I wrote elsewhere might give you something to think about:

It might be instructive to consider the simpler relation $HN(m,i,n)$ which holds if machine $m$, given input $i$, halts after exactly $n$ steps. Clearly this relation is decidable: Simulate $m$ for at most $n$ steps, or until it halts. If it halts on the $n$th step, the answer is yes; if it halts too soon, or not by the $n$th step, the answer is no. But the decidability of $HN$ doesn't help you decide if $m$ halts, because that question is not $HN(m,i,n)$ for any fixed $n$, but rather $∃n.HN(m,i,n)$…

If you want to think about what your $\Delta$ actually looks like, thinking about $HN(m,i,n)$ might be a good place to start. And you should consider the possibility that you might be able to prove $\lnot HN(m,i,0), \lnot HN(m,i,1), \ldots$ for every $n$, but still not be able to prove what you need, which is $\forall n.\lnot HN(m,i,n)$.