7

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?

Community
  • 1
Christopher King
  • 10,365
  • 1
    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 07 '15 at 02: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 07 '15 at 03:05
  • @columbus8myhw Or it won't and you need choice to prove it. The converse must also be true though. – Christopher King Aug 07 '15 at 03:06
  • 1
    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 07 '15 at 03:10
  • @PyRulez You just said what I said… – Akiva Weinberger Aug 07 '15 at 03:13
  • @columbus8myhw Oh, I mean it will halt, but it is as powerful as choice. This is the same as saying the negation of choice is as powerful as it not halting. – Christopher King Aug 07 '15 at 03:15
  • 1
    @PyRulez If it does halt, can't they both prove it? Just simulate the machine until it halts. – Akiva Weinberger Aug 07 '15 at 03:16

2 Answers2

7

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

Asaf Karagila
  • 393,674
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.

Xoff
  • 10,310