Independence from ZFC: Difference between revisions
Jump to navigation
Jump to search
(Created page with "'''Independence from ZFC''' refers to whether the computation of BB(n) is independent of ZFC.") |
(Create article and add rough history) |
||
| Line 1: | Line 1: | ||
For any computable and arithmetically sound axiomatic theory T, there exists an integer <math>N_T</math> such that T cannot prove the values of BB(n) for any <math>n \ge N_T</math>. For ZF, this value is known to be in the range: | |||
<math display="block">6 \le N_{ZF} \le 643</math> | |||
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(643). | |||
Scott Aaronson conjectured in his Busy Beaver Frontier survey<ref name=":0">Scott Aaronson. 2020. [https://www.scottaaronson.com/papers/bb.pdf The Busy Beaver Frontier]. SIGACT News 51, 3 (August 2020), 32–54. https://doi.org/10.1145/3427361.3427369</ref> that <math>N_{ZF} \le 20</math>. | |||
== 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. | |||
{| class="wikitable" | |||
|+History of ZF independent TMs | |||
!States | |||
!Date | |||
!Discoverer | |||
!Source | |||
!Verification | |||
|- | |||
|7910 | |||
|May 2016 | |||
|Adam Yedidia and Scott Aaronson | |||
|Yedida and Aaronson 2016<ref>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</ref> | |||
| | |||
|- | |||
|748 | |||
|May 2016 | |||
|Stefan O’Rear | |||
|[https://github.com/sorear/metamath-turing-machines/blob/master/zf2.nql Github NQL file], Busy Beaver Frontier<ref name=":0" /> | |||
| | |||
|- | |||
|745 | |||
|July 2023 | |||
|Johannes Riebel | |||
|Riebel 2023 Bachelor Thesis<ref>Riebel, Johannes (March 2023). ''[https://www.ingo-blechschmidt.eu/assets/bachelor-thesis-undecidability-bb748.pdf The Undecidability of BB(748): Understanding Gödel's Incompleteness Theorems]'' (PDF) (Bachelor's thesis). University of Augsburg.</ref> | |||
| | |||
|- | |||
|643 | |||
|July 2024 | |||
|Rohan Ridenour | |||
|[https://github.com/CatsAreFluffy/metamath-turing-machines Github NQL], [https://scottaaronson.blog/?p=8131 Aaronson Announcement] | |||
| | |||
|} | |||
== References == | |||
<references /> | |||
Revision as of 20:58, 30 June 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(643).
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 |
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.