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

<p>If you look at <em>totality</em> in place of <em>halting</em>, 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.</p>

CC BY-SA 3.0
2014-03-05T18:16:34.160Z
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?
Super8
CC BY-SA 3.0
2014-03-06T00:01:38.050Z
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.
Kaveh
CC BY-SA 3.0
2014-03-06T23:46:51.710Z
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?
Super8
CC BY-SA 3.0
2014-03-06T23:55:30.337Z
@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.
Kaveh
CC BY-SA 3.0
2014-03-07T00:30:58.037Z
Ok, I hadn't realized the problem, I will try finding a better definition on my own then.
Super8
CC BY-SA 3.0
2014-03-07T01:35:51.237Z
@Super8, there is a discussion of the issue with ordinal analysis in Girard's book Proof Theory and Logical Complexity.
Kaveh
CC BY-SA 3.0
2014-03-05T18:00:07.617Z
2014-03-05T18:06:46.877Z
2014-03-05T18:06:46.877Z
Kaveh
<p>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. </p>

<p>This might have some connection with <a href="http://en.wikipedia.org/wiki/Proof-theoretic_ordinal" rel="nofollow">ordinal analysis</a>. 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}$?</p>

CC BY-SA 3.0
2014-03-05T16:21:17.670Z
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.
Yonatan N
CC BY-SA 3.0
2014-03-05T16:25:19.647Z
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.
Super8
CC BY-SA 3.0
2014-03-05T16:29:44.000Z
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](http://cs.stackexchange.com/questions/18424/is-there-a-tm-that-halts-on-all-inputs-but-that-property-is-not-provable) cs.se
vzn
CC BY-SA 3.0
2014-03-05T16:30:19.407Z
You can construct a Turing machine $M$ that computes the [Goodstein's sequence](https://en.wikipedia.org/wiki/Goodstein_sequence#Goodstein_sequences) $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)](http://faculty.baruch.cuny.edu/lkirby/accessible_independence_results.pdf)
Marzio De Biasi
CC BY-SA 3.0
2014-03-05T16:36:48.893Z
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.
Super8
CC BY-SA 3.0
2014-03-05T17:06:09.007Z
This [question on CS Stack Exchange](http://cs.stackexchange.com/q/18424/9550) is related.
David Richerby
<turing-machines><proof-theory><halting-problem>
Turing machines whose termination is unprovable?
Super8
# Turing machines whose termination is unprovable?

(Asked by: username_0 on 2014-03-05)

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](http://en.wikipedia.org/wiki/Proof-theoretic_ordinal). 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}$?

**Tags:** turing-machines, proof-theory, halting-problem
> **Comments:**
> **username_1**: 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.  
> **username_0**: 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.  
> **username_2**: 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](http://cs.stackexchange.com/questions/18424/is-there-a-tm-that-halts-on-all-inputs-but-that-property-is-not-provable) cs.se  
> **username_3**: You can construct a Turing machine $M$ that computes the [Goodstein's sequence](https://en.wikipedia.org/wiki/Goodstein_sequence#Goodstein_sequences) $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)](http://faculty.baruch.cuny.edu/lkirby/accessible_independence_results.pdf)  
> **username_0**: 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.  
> **username_4**: This [question on CS Stack Exchange](http://cs.stackexchange.com/q/18424/9550) is related.  

---

## 1 answers

### Answer by username_5 on 2014-03-05. Score: 9

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.

> **Comments:**
> **username_0**: 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?  
> **username_5**: 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.  
> **username_0**: 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?  
> **username_5**: @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.  
> **username_0**: Ok, I hadn't realized the problem, I will try finding a better definition on my own then.  
> **username_5**: @Super8, there is a discussion of the issue with ordinal analysis in Girard's book Proof Theory and Logical Complexity.  

---

