4 ms·

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) 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
    > if the axioms at the start are all true. Axioms are true by definition; that's what "axiom" means. (They might also be false, but (if and) only if your system is inconsistent.) > Case (1) that machine doesn't really halt This is not a state of affairs: all you know at any given time is that the machine hasn't halted yet (after some specific finite number of steps), or that it has aquired some termination-precluding invariant like a infinite loop (which you can detect only strictly less than all of).
    - rssoconnor 5y ago
      Axioms are most certainly not true by definition. Regardless, the particular technical definition of truth I'm using is Tarski's definition of truth[1]. We don't have to agree whether Tarski's definition is "correct", and I'm happy to qualify my use of the word "truth" here, but I'm referring to a specific technical definition here. [1] https://en.wikipedia.org/wiki/Semantic_theory_of_truth#Tarski's_theory_of_truth https://en.wikipedia.org/wiki/Semantic_theory_of_truth#Tarsk...

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
  > if the axioms at the start are all true. Axioms are true by definition; that's what "axiom" means. (They might also be false, but (if and) only if your system is inconsistent.) > Case (1) that machine doesn't really halt This is not a state of affairs: all you know at any given time is that the machine hasn't halted yet (after some specific finite number of steps), or that it has aquired some termination-precluding invariant like a infinite loop (which you can detect only strictly less than all of).
  - rssoconnor 5y ago
    Axioms are most certainly not true by definition. Regardless, the particular technical definition of truth I'm using is Tarski's definition of truth[1]. We don't have to agree whether Tarski's definition is "correct", and I'm happy to qualify my use of the word "truth" here, but I'm referring to a specific technical definition here. [1] https://en.wikipedia.org/wiki/Semantic_theory_of_truth#Tarski's_theory_of_truth https://en.wikipedia.org/wiki/Semantic_theory_of_truth#Tarsk...