<p>Take the "current mathematical system" $S$ and an undecidable sentence $P$ for $S$. Consider the Turing machine $T$ which enumerates all theorems of $S$ and halts if it ever enumerates either $P$ or $\lnot P$. System $S$ cannot decide whether $T$ halts.</p>

<p>Note that such a $T$ does not halt.</p>

CC BY-SA 3.0
2016-06-29T22:28:38.437Z
See [here](http://www.scottaaronson.com/blog/?p=2725), [here](http://www.scottaaronson.com/blog/?p=2741) and [here](https://github.com/sorear/metamath-turing-machines/blob/master/sample_out/zf.tm) for discussion of some specific $2$-symbol Turing machines with ZFC-independent halting problem, recently created in essentially the manner you describe. It appears that the number of states required for such a machine is now at $1919$, and quite sure to decrease further.
r.e.s.
CC BY-SA 3.0
2015-01-23T06:01:39.907Z
2015-01-23T06:01:39.907Z
Andrej Bauer
<p>Is there a simple example of a Turing machine $M$, such that whether $M$ halts or not on the empty input cannot be proved within the current mathematical system?</p>

<p>Specifically, I'm curious whether there exists an example simple enough that the state transition of the Turing machine can be drawn as a reasonably-sized diagram.</p>

CC BY-SA 3.0
2015-01-23T00:53:24.157Z
look at the answers of this thread: http://cstheory.stackexchange.com/questions/20978/what-is-the-smallest-turing-machine-where-it-is-unknown-if-it-halts-or-not/
Denis
CC BY-SA 3.0
2015-01-23T18:34:42.147Z
one can take any halting problem with arbitrary input and encode that into the start/ initialization states of the TM to write the input to the tape. so Turings classic problem applies here with simple adjustment. it is known from some research on "small TMs" the halting problem is encodable in some fairly small TMs.
vzn
<turing-machines>
Simple example of halting-unprovable Turing machine
Qian Yu
# Simple example of halting-unprovable Turing machine

(Asked by: username_0 on 2015-01-23)

Is there a simple example of a Turing machine $M$, such that whether $M$ halts or not on the empty input cannot be proved within the current mathematical system?

Specifically, I'm curious whether there exists an example simple enough that the state transition of the Turing machine can be drawn as a reasonably-sized diagram.

**Tags:** turing-machines

> **Comments:**
> **username_1**: look at the answers of this thread: http://cstheory.stackexchange.com/questions/20978/what-is-the-smallest-turing-machine-where-it-is-unknown-if-it-halts-or-not/  
> **username_2**: one can take any halting problem with arbitrary input and encode that into the start/ initialization states of the TM to write the input to the tape. so Turings classic problem applies here with simple adjustment. it is known from some research on "small TMs" the halting problem is encodable in some fairly small TMs.  

---

## 1 answers

### Answer by username_3 on 2015-01-23. Score: 3

Take the "current mathematical system" $S$ and an undecidable sentence $P$ for $S$. Consider the Turing machine $T$ which enumerates all theorems of $S$ and halts if it ever enumerates either $P$ or $\lnot P$. System $S$ cannot decide whether $T$ halts.

Note that such a $T$ does not halt.

> **Comments:**
> **username_4**: See [here](http://www.scottaaronson.com/blog/?p=2725), [here](http://www.scottaaronson.com/blog/?p=2741) and [here](https://github.com/sorear/metamath-turing-machines/blob/master/sample_out/zf.tm) for discussion of some specific $2$-symbol Turing machines with ZFC-independent halting problem, recently created in essentially the manner you describe. It appears that the number of states required for such a machine is now at $1919$, and quite sure to decrease further.  

---

