Independence from ZFC: Difference between revisions
No edit summary |
|||
| Line 45: | Line 45: | ||
|Rohan Ridenour | |Rohan Ridenour | ||
|[https://github.com/CatsAreFluffy/metamath-turing-machines Github NQL] ([https://github.com/CatsAreFluffy/metamath-turing-machines/commit/6fc33bef6ba8885d26aed94c83e88bdabbedb0f1 commit]) | |[https://github.com/CatsAreFluffy/metamath-turing-machines Github NQL] ([https://github.com/CatsAreFluffy/metamath-turing-machines/commit/6fc33bef6ba8885d26aed94c83e88bdabbedb0f1 commit]) | ||
|- | |||
|588 | |||
|12 July 2025 | |||
|andrew-j-wade | |||
|[https://github.com/andrew-j-wade/metamath-turing-machines Github NQL] ([https://github.com/andrew-j-wade/metamath-turing-machines/commit/30d2e3194866615f68dd2f5101cb300fb039adca commit]) | |||
|- | |||
|585 -> 582 -> 565 -> 564 | |||
|13 July 2025 | |||
|andrew-j-wade | |||
|[https://github.com/andrew-j-wade/metamath-turing-machines Github NQL] ([https://github.com/andrew-j-wade/metamath-turing-machines/commit/826291bbc854d6ec9a4c62a93449778fefe48dd6 585 commit], [https://github.com/andrew-j-wade/metamath-turing-machines/commit/8b44516aa9f4943162bdf3dd84decbb4d38b5e3e 582 commit], [https://github.com/andrew-j-wade/metamath-turing-machines/commit/6741347b0e203a796e246d793bfd0d6bd8ea9f5c 565 commit], [https://github.com/andrew-j-wade/metamath-turing-machines/commit/b371d266eb8988d5175ab09ee1466bf70b847551 564 commit]) | |||
|- | |||
|559 | |||
|15 July 2025 | |||
|andrew-j-wade | |||
|[https://github.com/andrew-j-wade/metamath-turing-machines Github NQL] ([https://github.com/andrew-j-wade/metamath-turing-machines/commit/ef54215d391c9c6d28dfe75acf02889ab479b114 commit]) | |||
|- | |||
|549 | |||
|16 July 2025 | |||
|andrew-j-wade | |||
|[https://github.com/andrew-j-wade/metamath-turing-machines Github NQL] ([https://github.com/andrew-j-wade/metamath-turing-machines/commit/5d676aec074a94f598959cb3b7733a8f7781762f commit]) | |||
|} | |} | ||
== References == | == References == | ||
<references /> | <references /> | ||
Revision as of 06:45, 21 July 2025
For any computable and arithmetically sound axiomatic theory T, there exists an integer such that T cannot prove the values of BB(n) for any . For ZF, this value is known to be in the range:
This lower bound comes from the fact that BB(5) has been proven in Rocq. The upper bound comes from an explicit TM which enumerates all possible proofs in ZF and halts if it finds a proof 0 = 1. Assuming ZF is consistent, then it cannot prove its own consistency, hence it cannot prove whether this specific TM halts and thus cannot prove the value of BB(636).
Scott Aaronson conjectured in his Busy Beaver Frontier survey[1] that .
History
There is no one authoritative source on the history of TMs independent of ZF, this is our best understanding of the history of TMs found. Mostly these are taken from Scott Aaronson's blog announcements and Busy Beaver Frontier.
| States | Date | Discoverer | Source | Verification |
|---|---|---|---|---|
| 7910 | May 2016 | Adam Yedidia and Scott Aaronson | Yedida and Aaronson 2016[2] | |
| 748 | May 2016 | Stefan O’Rear | Github NQL file, Busy Beaver Frontier[1] | |
| 745 | July 2023 | Johannes Riebel | Riebel 2023 Bachelor Thesis[3] | |
| 643 | July 2024 | Rohan Ridenour | Github NQL, Aaronson Announcement | |
| 636 | 31 August 2024 | Rohan Ridenour | Github NQL (commit) | |
| 588 | 12 July 2025 | andrew-j-wade | Github NQL (commit) | |
| 585 -> 582 -> 565 -> 564 | 13 July 2025 | andrew-j-wade | Github NQL (585 commit, 582 commit, 565 commit, 564 commit) | |
| 559 | 15 July 2025 | andrew-j-wade | Github NQL (commit) | |
| 549 | 16 July 2025 | andrew-j-wade | Github NQL (commit) |
References
- ↑ 1.0 1.1 Scott Aaronson. 2020. The Busy Beaver Frontier. SIGACT News 51, 3 (August 2020), 32–54. https://doi.org/10.1145/3427361.3427369
- ↑ A. Yedidia and S. Aaronson. A relatively small Turing machine whose behavior is independent of set theory. Complex Systems, (25):4, 2016. https://arxiv.org/abs/1605.04343
- ↑ Riebel, Johannes (March 2023). The Undecidability of BB(748): Understanding Gödel's Incompleteness Theorems (PDF) (Bachelor's thesis). University of Augsburg.