4 ms·

The thread is about programs. Existing programs do exist. There are problems not solvable by Turing machines, like the meaning of life, but this thread is not a

by bmacho 3y ago

The thread is about programs. Existing programs do exist. There are problems not solvable by Turing machines, like the meaning of life, but this thread is not about them. GGP was talking about programs halting, not halting, and "something else", which GGP called "undecidable". There are programs that ZFC cannot prove if they halt or not. For example, searching for a contradiction in ZFS is such a program. Its undecidability means that there is no sequence of axioms of ZFC that ends with "this program halts" or "this program does not halt". But then this program does not halt, since its halting would mean that ZFC can prove that this program halts. In any case, programs can halt or not halt. There are programs that ZFC cannot prove that they halt or not, but those programs do not halt.

SAI_Peregrinus 3y ago
> But then this program does not halt, since its halting would mean that ZFC can prove that this program halts. That step is not logically consistent. It could halt, it's just that ZFC can't prove it will ever do so. For example, the program which computes the 8000th busy beaver number halts (per definition of the busy beaver function), but is undecidable in ZFC[1]. An undecidable program can halt. An undecidable program can run forever. But whatever axiom system is being used to decide that can't prove which (without running the program, potentially for an infinite number of steps). [1] https://scottaaronson.blog/?p=2725 https://scottaaronson.blog/?p=2725
- deleted 3y ago
  [deleted]
- bmacho 3y ago
  > For example, the program which computes the 8000th busy beaver number I don't believe that there exist such a program.
  - SAI_Peregrinus 3y ago
    Why not? That implies that an 8000 state Turing machine which eventually halts when started with a blank tape doesn't exist. If any of them do (and it's trivial to simulate one), then exactly such a program can exist.
    - bmacho 3y ago
      Well, there can indeed exist a program that writes out the number BB(8000). (In the sense that it is consistent with ZFC that there is a program that writes out the number of steps of the smallest contradiction in ZFC.) What I don't believe that there exist a program that is a proper counter-example, that is, its halting is undecidable in ZFC, and it halts. Exactly because what I wrote earlier.

by bmacho 3y ago

SAI_Peregrinus 3y ago

> But then this program does not halt, since its halting would mean that ZFC can prove that this program halts. That step is not logically consistent. It could halt, it's just that ZFC can't prove it will ever do so. For example, the program which computes the 8000th busy beaver number halts (per definition of the busy beaver function), but is undecidable in ZFC[1]. An undecidable program can halt. An undecidable program can run forever. But whatever axiom system is being used to decide that can't prove which (without running the program, potentially for an infinite number of steps). [1] https://scottaaronson.blog/?p=2725 https://scottaaronson.blog/?p=2725

deleted 3y ago
[deleted]
bmacho 3y ago
> For example, the program which computes the 8000th busy beaver number I don't believe that there exist such a program.
- SAI_Peregrinus 3y ago
  Why not? That implies that an 8000 state Turing machine which eventually halts when started with a blank tape doesn't exist. If any of them do (and it's trivial to simulate one), then exactly such a program can exist.
  - bmacho 3y ago
    Well, there can indeed exist a program that writes out the number BB(8000). (In the sense that it is consistent with ZFC that there is a program that writes out the number of steps of the smallest contradiction in ZFC.) What I don't believe that there exist a program that is a proper counter-example, that is, its halting is undecidable in ZFC, and it halts. Exactly because what I wrote earlier.