10
$\begingroup$

I have a naive question: does there exist a Turing machine whose termination is true but unprovable by any natural, consistent and finitely axiomatizable theory? I ask for a mere existence proof rather than a specific example.

This might have some connection with ordinal analysis. Indeed, for a Turing machine $M$, we can define $O(M)$ as the least ordinal of a consistent theory proving its termination (or the infimum of these ordinals). So I guess it would be equivalent to ask whether there exists $M$ such that $O(M) \geq \omega_1^{CK}$?

Improve this question
$\endgroup$
6
  • 1
    $\begingroup$ Shouldn't the quantification work the other way around? Simply adding in TM X halts as an axiom would be consistent for any X that actually halts on all inputs (and finite if you do it for only the TM in question). With the quantifiers reversed, how about a TM that halts if the input is not a proof of consistency for the axiomatic system and enters an infinite loop otherwise. $\endgroup$
    – Yonatan N
    Commented Mar 5, 2014 at 16:21
  • $\begingroup$ Your suggestion is interesting, thanks. I was aware of your concern when formulating the question, that's why I added "natural" in the requirements. Of course, the problem is whether we can give a formal definition of "naturalness" that would rule out this artificial construction. $\endgroup$
    – Super8
    Commented Mar 5, 2014 at 16:25
  • 1
    $\begingroup$ think the answer is no because if its halting, then one just runs the machine and it will halt in a finite number of steps, and thats a proof, and that fact can be converted to any reasonably powerful proof system. on other hand think it is possible to encode/convert/translate godel's unprovable thm into a non-halting machine for which non-halting is unprovable. this question is similar, is there a TM that halts on all inputs but the property is not provable cs.se $\endgroup$
    – vzn
    Commented Mar 5, 2014 at 16:29
  • 1
    $\begingroup$ You can construct a Turing machine $M$ that computes the Goodstein's sequence $G(n)$ of the input $n$ and halts when it reaches $0$.The halting of $M$ cannot be proved in Peano arithmetic; i.e. Goodstein’s Theorem is not provable using the Peano axioms of arithmetic. See Laurie Kirby, Jeff Paris, Accessible independence results for Peano arithmetic (1982) $\endgroup$
    – Marzio De Biasi
    Commented Mar 5, 2014 at 16:30
  • $\begingroup$ Thanks, I did not know those entries. What I'm asking is stronger though, I'd like unprovability wrt to any reasonable theory (rather than a specific theory such as PA). I'm not sure if the question has a definite answer though. $\endgroup$
    – Super8
    Commented Mar 5, 2014 at 16:36

2 Answers 2

Reset to default
9
$\begingroup$

Termination of a Turing machine (on a fixed input) is a $\Sigma^0_1$ sentence and all usual first-order arithmetic theories are complete for $\Sigma^0_1$ sentences, i.e. all true $\Sigma^0_1$ statements are provable in these theories.

If you look at totality in place of halting, i.e. a TM halts on all inputs, then that is a $\Pi^0_2$-complete sentence and for any computably axiomatizable consistent theory which is strong enough (e.g. extends say Robinson's $Q$ theory) there is a TM whose totality cannot be proven in that theory.

Improve this answer
$\endgroup$
6
  • $\begingroup$ Yes, I was looking for totality, as of course the problem is trivial for a fixed input. I'll think about your claim and how to prove it, but at this point I don't see how considering "computably axiomatizable" theories rules out the aforementioned problem? Also, in your statement the TM depends on the considered theory, can we get my stronger statement by some kind of diagonalization? $\endgroup$
    – Super8
    Commented Mar 5, 2014 at 18:16
  • $\begingroup$ Here is an easy way: the set of provably total computable functions of such a theory is c.e., the set of total computable functions is not c.e., or alternatively you can diagonalize against the provably total functions of the theory. $\endgroup$
    – Kaveh
    Commented Mar 6, 2014 at 0:01
  • $\begingroup$ On second thought, I suggest considering a restriction of the problem as follows. Given an ordinal notation system $\sigma$ representing an ordinal $\alpha$, we can define a corresponding "elementary theory" $\mathcal{T}(\alpha,\sigma)$ that allows transfinite induction up to $\alpha$. Given a TM $M$, we would then define $O(M)$ as the smallest ordinal $\alpha$ such that the termination of $M$ can be proved by a theory $\mathcal{T}(\alpha,\sigma)$ (i.e. the notation system can be freely chosen). Does this definition make sense? $\endgroup$
    – Super8
    Commented Mar 6, 2014 at 23:46
  • $\begingroup$ @Super8, I am not sure. Generally the association of ordinals to theories is not canonical, there are various ways to associate to do it. You can start with a weak theory like PRA and add induction over computable ordinals with nice fundamental sequences, etc. but I am not sure why you would like to do so. $\endgroup$
    – Kaveh
    Commented Mar 6, 2014 at 23:55
  • $\begingroup$ Ok, I hadn't realized the problem, I will try finding a better definition on my own then. $\endgroup$
    – Super8
    Commented Mar 7, 2014 at 0:30
3
$\begingroup$

I'm not a logic expert, but I believe the answer is no. If the Turing machine halts, and the system is strong enough, you ought to be able to write out the full computation history of the Turing machine on its input. When one verifies that the result of the computation is a terminating sequence of transitions, one can see that the machine halts. Regardless of how you formalize Turing machines in your theory, you ought to be able to show in any reasonable theory that a machine that halts does in fact halt. By way of analogy, think of trying to prove that a finite sum is equal to what it is equal to; e.g., prove that 5+2+3+19+7+6=42, or 5+5+5=15. Just as this is always possible as long as the number of steps is finite, so too is proving the result of a finite computation.

Just as an additional obvious point--even if your theory is inconsistent, you can still show that the machine halts, actually even if it doesn't, since you can prove any wff in an inconsistent theory, regardless of whether or not it is actually true.

Improve this answer
$\endgroup$
2
  • $\begingroup$ I agree with your first point, see my reply below. Regarding your second point, an inconsistent theory will also prove the termination of an (actually nonterminating) TM, whence the restriction to consistent theories. $\endgroup$
    – Super8
    Commented Mar 5, 2014 at 18:20
  • $\begingroup$ I think we are saying the same thing; I just noticed that you said "consistent" in the question, sorry for missing that. I think Kaveh's answer covers all the same things and is more elegantly written, anyway. $\endgroup$
    – user1338
    Commented Mar 5, 2014 at 19:14

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.