Logical independence: Difference between revisions
Add Wade's new 385 champ |
No edit summary |
||
| (6 intermediate revisions by 2 users not shown) | |||
| 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 [[wikipedia:Zermelo–Fraenkel_set_theory|Zermelo–Fraenkel set theory]] (ZF), this value is known to be in the range: | 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 [[wikipedia:Zermelo–Fraenkel_set_theory|Zermelo–Fraenkel set theory]] (ZF), this value is known to be in the range: | ||
<math display="block">6 \le N_{ZF} \le | <math display="block">6 \le N_{ZF} \le 432</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 | 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 and sound, then it cannot prove whether or not it is consistent, hence it cannot prove whether or not this specific TM halts. | ||
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>. | 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> and <math>N_{PA} \le 10</math>, where <math>PA</math> refers to the theory of [https://en.wikipedia.org/wiki/Peano%20axioms Peano Arithmetic]. | ||
== Axiom of Choice == | == Axiom of Choice == | ||
| Line 66: | Line 66: | ||
| | | | ||
|- | |- | ||
| | |432 | ||
| | |19 Aug 2025 | ||
|Andrew J. Wade | |Andrew J. Wade | ||
|[https:// | |[https://codeberg.org/ajwade/turing_machine_explorer/commit/33b30300054242201a95679aacf7e74312bd8803b0df9a85d2314095efd6804e git commit] | ||
| | | | ||
|} | |||
(For Peano Arithmetic, the ZF independent machines are an upper bound) | |||
{| class="wikitable" | |||
|+History of Peano Arithmetic (PA) independent TMs | |||
!States | |||
!Date | |||
!Discoverer | |||
!Source | |||
!Verification | |||
|- | |||
|372 | |||
|February 2026 | |||
|@LegionMammal978 | |||
|[https://github.com/LegionMammal978/turing_machine_explorer/blob/main/pa.py Github NQL] | |||
|} | |} | ||
== References == | == References == | ||
<references /> | <references /> | ||
Latest revision as of 00:31, 13 February 2026
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 Zermelo–Fraenkel set theory (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 and sound, then it cannot prove whether or not it is consistent, hence it cannot prove whether or not this specific TM halts.
Scott Aaronson conjectured in his Busy Beaver Frontier survey[1] that and , where refers to the theory of Peano Arithmetic.
Axiom of Choice
Due to Shoenfield's absoluteness theorem, it is known that any TM proven non-halting in ZFC can also be proven non-halting in ZF (and the converse is trivially true), therefore
Therefore we refer to ZF and throughout this article since adding the Axiom of Choice does not have any effect on Turing machine decidability.
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 or self-reported by the individuals who discovered them.
| 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) | |
| 549 | 16 July 2025 | Andrew J. Wade | Github NQL (commit) | |
| 432 | 19 Aug 2025 | Andrew J. Wade | git commit |
(For Peano Arithmetic, the ZF independent machines are an upper bound)
| States | Date | Discoverer | Source | Verification |
|---|---|---|---|---|
| 372 | February 2026 | @LegionMammal978 | Github NQL |
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.