5 ms·

It's not "okay" because such a system proves that various particular Turing machines halt when, in fact, those machines do not halt. See https://news.ycombinat

It's not "okay" because such a system proves that various particular Turing machines halt when, in fact, those machines do not halt. See https://news.ycombinator.com/item?id=27847719 https://news.ycombinator.com/item?id=27847719. But to be a bit more specific, ¬Con(ZFC) says that the Turing machine that searches for a contradiction in ZFC does indeed halt. However (in all likelihood) such a machine does not actually halt, in the sense that it does not halt in 1 step, and it does not halt in 2 steps, and it does not halt in 3 steps, etc., and indeed (in all likelihood) for each numeral n, ZFC even proves that the machine does not halt in n steps. (Now there is a small possibility that maybe such a machine does halt in some particular number of steps. If it does actually halt, that means it has found a proof that ZFC is inconsistent. But this scenario is even worse, because it means that ZFC itself is not only unsound, but inconsistent, (and hence ZFC+¬Con(ZFC) is also inconsistent). In particular ZFC+¬Con(ZFC) being inconsistent means it proves that every Turing machine halts, which is even more wrong in general, even if it happens to be right about this particular machine.)

a1369209993 5y ago
> such a system proves that various particular Turing machines halt when, []in fact[], those machines do not halt. Er, no. The fact is that there is no fact of the matter as to whether those particular Turing machines either a: do not halt at all, or b: halt after a (colloquially) infinite number of steps. (A implication of there being no fact of the matter is that, empirically, we can't tell the difference by running them, but we can't tell the difference for a machine that halts in 2^(2^(2^256)) steps (or not at all) either, so that's not very interesting on it's own.) (As you note, we don't actually know that (for example) a Turing machines looking for contradictions in ZFC is one of those particular machines; indeed I'm not sure offhand if we actually know of any specific example of such a machine. But that's presumably not the issue here.)
- rssoconnor 5y ago
  ZFC+¬Con(ZFC) either wrongly proves that the machine that searches for an inconsistency in ZFC halts, or it wrongly proves that `while(true)` halts. Either way ZFC+¬Con(ZFC) is wrong about something.
  - ummonk 5y ago
    Why is it wrong to say that the machine halts?
    - deleted 5y ago
      [deleted]
    - rssoconnor 5y ago
      ZFC+¬Con(ZFC) definitely proves that the machine that searches for an inconsistency in ZFC halts. That is a direct consequnce of ¬Con(ZFC). Keep in mind that by "proves" I'm only saying that there exists a logical deduction from the axioms. I'm not saying that it is true or false. Remember that logical deductions are "truth preserving", but we can only conclude that the conclusions are true if the axioms at the start are all true. So again, we have a proof in some sketchy axiom system that the machine that searches for an inconsistency in ZFC halts. The question is whether that conclusion is a true statement or not, whether that machine actually does or does not halt. You can start up that program on your laptop while we consider it. Maybe it will halt during our discussion. I also want to point out that whether that conclusion is a true statement or not has no bearing on whether the deduction system was sound to begin with. Unsound systems can prove true statement, simply by accident rather than by design. Case (1) that machine doesn't really halt, then ZFC+¬Con(ZFC) proves an untrue statement, and we thus the system is unsound. Case (2) that machine does really halt. Then this particular conclusion wasn't untrue, but we have another problem. We can take the output of that machine, decode it, and we have a proof of an inconsistency in ZFC. Again this is just a deduction, it doesn't mean that math is wrong or the world ends. Just that the ZFC axiom system is so unsound that it is inconsistent, and it has some untrue axioms. Nevertheless we can use such a proof and derive a proof that ZFC prove `while(true)` halts, and in turn transform that into a proof in ZFC+¬Con(ZFC) that `while(true)` halts. And it is definitely the case that `while(true)` doesn't halt. So in this case we have found a different but still untrue statement that ZFC+¬Con(ZFC) proves. Our conclusion is the same: ZFC+¬Con(ZFC) is unsound. So in either case `ZFC+¬Con(ZFC)` proves some machine halts that doesn't. I haven't concluded which of the two machines it is wrong about though I have my personal suspicions, but it is definitely wrong about one of them.

a1369209993 5y ago

> such a system proves that various particular Turing machines halt when, []in fact[], those machines do not halt. Er, no. The fact is that there is no fact of the matter as to whether those particular Turing machines either a: do not halt at all, or b: halt after a (colloquially) infinite number of steps. (A implication of there being no fact of the matter is that, empirically, we can't tell the difference by running them, but we can't tell the difference for a machine that halts in 2^(2^(2^256)) steps (or not at all) either, so that's not very interesting on it's own.) (As you note, we don't actually know that (for example) a Turing machines looking for contradictions in ZFC is one of those particular machines; indeed I'm not sure offhand if we actually know of any specific example of such a machine. But that's presumably not the issue here.)

rssoconnor 5y ago
ZFC+¬Con(ZFC) either wrongly proves that the machine that searches for an inconsistency in ZFC halts, or it wrongly proves that `while(true)` halts. Either way ZFC+¬Con(ZFC) is wrong about something.
- ummonk 5y ago
  Why is it wrong to say that the machine halts?
  - deleted 5y ago
    [deleted]
  - rssoconnor 5y ago
    ZFC+¬Con(ZFC) definitely proves that the machine that searches for an inconsistency in ZFC halts. That is a direct consequnce of ¬Con(ZFC). Keep in mind that by "proves" I'm only saying that there exists a logical deduction from the axioms. I'm not saying that it is true or false. Remember that logical deductions are "truth preserving", but we can only conclude that the conclusions are true if the axioms at the start are all true. So again, we have a proof in some sketchy axiom system that the machine that searches for an inconsistency in ZFC halts. The question is whether that conclusion is a true statement or not, whether that machine actually does or does not halt. You can start up that program on your laptop while we consider it. Maybe it will halt during our discussion. I also want to point out that whether that conclusion is a true statement or not has no bearing on whether the deduction system was sound to begin with. Unsound systems can prove true statement, simply by accident rather than by design. Case (1) that machine doesn't really halt, then ZFC+¬Con(ZFC) proves an untrue statement, and we thus the system is unsound. Case (2) that machine does really halt. Then this particular conclusion wasn't untrue, but we have another problem. We can take the output of that machine, decode it, and we have a proof of an inconsistency in ZFC. Again this is just a deduction, it doesn't mean that math is wrong or the world ends. Just that the ZFC axiom system is so unsound that it is inconsistent, and it has some untrue axioms. Nevertheless we can use such a proof and derive a proof that ZFC prove `while(true)` halts, and in turn transform that into a proof in ZFC+¬Con(ZFC) that `while(true)` halts. And it is definitely the case that `while(true)` doesn't halt. So in this case we have found a different but still untrue statement that ZFC+¬Con(ZFC) proves. Our conclusion is the same: ZFC+¬Con(ZFC) is unsound. So in either case `ZFC+¬Con(ZFC)` proves some machine halts that doesn't. I haven't concluded which of the two machines it is wrong about though I have my personal suspicions, but it is definitely wrong about one of them.