4 ms·

The frequency illusion is funny—I just learned about the ordinals and now I’m seeing articles pop up about them everywhere. It’s only mentioned briefly in a fo

The frequency illusion is funny—I just learned about the ordinals and now I’m seeing articles pop up about them everywhere. It’s only mentioned briefly in a footnote in the article, but one of the most mind-blowing concepts related to ordinals is called the Goldstein sequences. These are basically sequences that start at an arbitrary natural number n and follow some simple rules (like the Collatz conjecture) to go from one item in a Goodstein sequence to the next. Much like the sequences in the Collatz conjecture, the Goodstein sequences can reach incredibly (extraordinarily) high numbers before eventually coming back down and terminating at zero. However, unlike the Collatz conjecture, the statement that all Goodstein sequences eventually terminate at zero for any starting value n has been proven. But here’s the remarkable part: the proof that all sequences eventually terminate requires axioms “beyond” what you think of as involved in standard arithmetic. Specifically, we require the ordinals and transfinite induction to prove that all sequences terminate (i.e., there is a proof that Peano Arithmetic cannot prove that all sequences terminate; ZFC can however). What this means is that you can create an extraordinarily tiny Turing machine (or a Python script that’s about 10 lines of code) whose halting behavior requires these bizarre axioms that most non-mathematicians have never heard of to prove. That is just nuts to me for some reason.

tjf801 2y ago
do you have a source on the tiny goodstein sequence machine? that sounds like a really interesting read
feoren 2y ago
> you can create an extraordinarily tiny Turing machine (or a Python script that’s about 10 lines of code) whose halting behavior requires these bizarre axioms that most non-mathematicians have never heard of to prove Two comments: (1) How can it be that we need bizarre axioms if ZFC can prove it? Or is it just that we know of a "direct" proof using bizarre axioms, but not one in ZFC? Isn't proving that a proof exists in ZFC enough to consider it proven in ZFC? (2) This is related to the reason why BusyBeaver(4) was easy to prove, BusyBeaver(5) only known recently, and BusyBeaver(745) is known to be independent of ZFC. For any set of axioms, there's some n and q where BusyBeaver(n) == q is true but not able to be proven in those axioms. Weird stuff starts happening once you get n large enough to encode the axioms themselves in the turing machine.
- Xcelerate 2y ago
  Regarding 1), I meant bizarre to non-mathematicians. Most people are familiar with arithmetic and perhaps even geometry proofs, but not so much with proofs that involve ordinals and multiple levels of infinity. That such a simple program requires more than (Peano) arithmetic to prove statements about its behavior seems very unintuitive, at least to me. 2) Yeah that’s actually how I discovered Goodstein sequences. I saw some post on HN about tiny Turing machines that halt iff ZFC is consistent and wanted to learn more.

tjf801 2y ago

do you have a source on the tiny goodstein sequence machine? that sounds like a really interesting read

feoren 2y ago

> you can create an extraordinarily tiny Turing machine (or a Python script that’s about 10 lines of code) whose halting behavior requires these bizarre axioms that most non-mathematicians have never heard of to prove Two comments: (1) How can it be that we need bizarre axioms if ZFC can prove it? Or is it just that we know of a "direct" proof using bizarre axioms, but not one in ZFC? Isn't proving that a proof exists in ZFC enough to consider it proven in ZFC? (2) This is related to the reason why BusyBeaver(4) was easy to prove, BusyBeaver(5) only known recently, and BusyBeaver(745) is known to be independent of ZFC. For any set of axioms, there's some n and q where BusyBeaver(n) == q is true but not able to be proven in those axioms. Weird stuff starts happening once you get n large enough to encode the axioms themselves in the turing machine.

Xcelerate 2y ago
Regarding 1), I meant bizarre to non-mathematicians. Most people are familiar with arithmetic and perhaps even geometry proofs, but not so much with proofs that involve ordinals and multiple levels of infinity. That such a simple program requires more than (Peano) arithmetic to prove statements about its behavior seems very unintuitive, at least to me. 2) Yeah that’s actually how I discovered Goodstein sequences. I saw some post on HN about tiny Turing machines that halt iff ZFC is consistent and wanted to learn more.