3 ms·
> 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
by 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 agoRegarding 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.