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

Question

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?

Answer 1

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$.

Answer 2

Short answer : no

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.