6

If, given Turing machine T, "T halts" or "T doesn't halt" could be derived from axioms of ZFC, halting problem would be in R. As it isn't, there must exist a Turing machine for which truth or falsehood of halting is independent of ZFC.

I want to see it. Is such machine known?

Karolis Juodelė
  • 9,702
  • 1
  • 25
  • 39
  • What do you mean by "the halting problem would be in RE. As it isn't..." Usually, we show the set of halting programs is r.e. but it is not recursive. Functions are not called "r.e.", sets are, and the set of halting turing machines is definitely r.e. – Thomas Andrews Aug 03 '13 at 13:15

1 Answers1

5

Let $T$ be the Turing machine which looks for a proof of a contradiction in ZFC. If ZFC is consistent, then whether or not $T$ halts will be independent of ZFC. (Indeed, if not, then this would contradict Gödel's incompleteness theorem!)

Zhen Lin
  • 90,111
  • No, if ZFC is consistent, then $T$ won't halt. – Thomas Andrews Aug 03 '13 at 13:43
  • @ThomasAndrews, see Gödel's incompleteness theorems – Karolis Juodelė Aug 03 '13 at 13:45
  • @KarolisJuodelė I know Godel. If ZFC is consistent, $T$ cannot halt, because $T$ halts when it finds an inconsistency. – Thomas Andrews Aug 03 '13 at 13:47
  • @ThomasAndrews, then we have that "T halts" is both, independent from ZFC and decidable? – Karolis Juodelė Aug 03 '13 at 13:50
  • The statement was "If ZFC is consistent, then..." That was false. But the question of whether ZFC is consistent could be undecidable. @KarolisJuodelė – Thomas Andrews Aug 03 '13 at 13:51
  • @ZhenLin, even though I've probably used such arguments myself, I'm not sure what a program that iterates over all proofs in ZFC actually looks like. Could you give a sketch of an implementation? – Karolis Juodelė Aug 03 '13 at 13:55
  • A proof can be easily encoded as a finite string of characters. Note that if you can prove any inconsistency, you can prove that $1=0$. So iterate over all natural numbers, check if it encodes a valid proof, and then check if it proves $1=0$. If so, you halt, otherwise you keep iterating. (This is why the axioms of any system need to be r.e. themselves, so we can check any step of a proof witha program.) – Thomas Andrews Aug 03 '13 at 14:00
  • @ThomasAndrews Whether or not $T$ halts depends on the set-theoretic universe. In a model of $\mathrm{ZFC} + \lnot \mathrm{Con}(\mathrm{ZFC})$, $T$ will halt, and in a model of $\mathrm{ZFC} + \mathrm{Con}(\mathrm{ZFC})$, $T$ will not halt. Since both of these theories are consistent if ZFC is, it must be the case that the halting of $T$ is independent of ZFC. – Zhen Lin Aug 03 '13 at 16:07
  • @ZhenLin Wait, ZFC is consistent with ZFC being inconsistent? Mind Blown – Christopher King Aug 07 '15 at 03:03
  • 3
    @ThomasAndrews : Indeed if ZFC is consistent, then an algorithm doing an exhaustive search for a contradiction in ZFC will not halt. But that's not the same as saying you can prove in ZFC that it will not halt. Nor could you prove in ZFC that it will. So if ZFC is consistent, then it will not halt, and morevoer its halting or non-halting is independent of ZFC. – Michael Hardy Aug 07 '15 at 03:16
  • 1
    @PyRulez I think the deal is that, in ZFC+$\lnot$Con(ZFC), there are sets that the model thinks are finite but are actually infinite. The reason the model thinks they're finite is because a set is infinite iff there's an injection from it to a proper subset of itself, and injections are types of sets. So the model thinks the "finite" set is finite because the required injection isn't in the model. In any case, $\lnot$Con(ZFC) means there's a natural number that codes a proof of a contradiction in ZFC. There is, it's just that the "number" is infinitely big. – Akiva Weinberger Aug 07 '15 at 03:39
  • 1
    And the machine $T$ will halt, it just takes a "finite" (infinite) amount of time. – Akiva Weinberger Aug 07 '15 at 03:40
  • Don't you need to assume that $\mathsf{ZFC} + \mathrm{Con}(\mathsf{ZFC})$ is consistent (not just $\mathsf{ZFC}$)? I think that's technically a slightly stronger assumption. In particular from what I know "both of these theories are consistent if ZFC is" is not true. – Izaak van Dongen Mar 02 '24 at 21:59