# Is there a turing machine for which halting is equivalent to the Axiom of Choice or its negation?

As seen in "A Turing machine for which halting is outside ZFC", Gödel's incompletness theorem can that there a turing machines for which halting can not be decided. My question is, is there a turing machine $T$, such that the statement "$T$ halts" is equivalent to the axiom of choice or its negation in ZF set theory?

• I don't know enough to answer but I'm certain the answer is no because axiom of choice does not affect statements that are made about finite objects. – user21820 Aug 7 '15 at 2:56
• Let me make sure I understand the question — you're asking for a machine $T$ that won't halt but you need Choice to prove it? – Akiva Weinberger Aug 7 '15 at 3:05
• @columbus8myhw Or it won't and you need choice to prove it. The converse must also be true though. – PyRulez Aug 7 '15 at 3:06
• I don't know much about model theory, but I'm pretty sure that $L$ has the same natural numbers as $V$. So, $T$ halts iff it halts in $L$ (right?), which means that if ZFC proves $T$ doesn't halt then so does ZF. ($L$ is the constructible universe, and $V$ is the set-theoretic universe. $L$ is a model of ZFC, even if $V$ doesn't have Choice.) I don't know of this is right, though. – Akiva Weinberger Aug 7 '15 at 3:10
• @PyRulez If it does halt, can't they both prove it? Just simulate the machine until it halts. – Akiva Weinberger Aug 7 '15 at 3:16

No, this is impossible.

While $\operatorname{Con}\sf (ZFC)$ is an arithmetic statement which can therefore be used to construct a Turing machine which will not provably half in $\sf ZFC$, the axiom of choice is not even remotely a statement about the integers. So there is no chance that this is going to happen.

Slightly more formally, though, recall that if $\varphi$ is a first-order statement about the integers, then $V\models\omega\models\varphi"$ if and only if $L\models\omega\models\varphi"$. Since the axiom of choice is true in $L$, if there was such Turing machine, it would have to halt in $L$ and therefore halt in $V$. So the axiom of choice would be true in $V$, and therefore provable from $\sf ZF$.

When consistency is involved, you can go to non-standard models where $\operatorname{Con}\sf (ZFC)$ is false. But with the axiom of choice this is not going to work, since whenever $M$ is a model of $\sf ZF$, then $M$ and $L^M$ have the same ordinals, so the same $\omega$.

At first, you must understand that, for any machine $M$, the proposition "$M$ halts" is false or provable. It comes from the fact that this formula is like $$\exists n\in\mathbb N \;\varphi(n)$$ with $\varphi$ primitive, and so you can always exhibit the $n$ such that $\varphi(n)$ is true, if it exists.
So each time "$M$ halts" is not provable, it means that $M$ does not halt (in a standard model of integers where, as usual, all integers are finite and can be exhibited). **
Now, "$M$ doesn't halt" may be not provable too (from Gödel's incompleteness theorem). If you agree with the previous point, it always implies that $M$ doesn't halt : the non provability of such a formula always implies that this formula is true (if you don't have a proof of its negation).
So, of course, it can't be equivalent to $AC$ which is neither true or false in $ZF$ and does not implies or prevents a non standard model of integers.
Another way to understand that it is not possible is to note that the formula of AC is much more complex than a formula for the halt of a machine ($\Pi_2^1$ vs $\Pi_1^0$ I think). It would not make sens for AC to be equivalent to such a simpler formula.
** Keep in mind that the incompletness theorem also implies that non provable formula can be true in a model and false in another one. However, if $n$ exists and is finite, you can always make a proof such as : "$n$ is the solution and here is the computation of $\phi(n)$ that proves it" and that will be a valid finite proof. It means that models where the formula is true ($M$ halts) and not provable require some infinite integers. However non standard models of $\mathbb N$ are quite difficult in $ZF$ and I did not find a simple way to understand them like you can in Peano's arithmetic.