Logical independence - Revision history

Tlonuqbar: in-between result

2026-10-26T23:00:54Z

in-between result

← Older revision		Revision as of 23:00, 26 October 2026
Line 83:		Line 83:
	\|Andrew J. Wade		\|Andrew J. Wade
	\|[https://codeberg.org/ajwade/turing_machine_explorer/commit/33b30300054242201a95679aacf7e74312bd8803b0df9a85d2314095efd6804e git commit]		\|[https://codeberg.org/ajwade/turing_machine_explorer/commit/33b30300054242201a95679aacf7e74312bd8803b0df9a85d2314095efd6804e git commit]
			\|
			\|-
			\|335
			\|11 Oct 2026
			\|Jeff Ketchersid
			\|[https://discord.com/channels/960643023006490684/1331570843829932063/1559077555158392844 discord message]
	\|		\|
	\|-		\|-

KinataKnight: Updated the record in the intro.

2026-10-25T04:48:03Z

Updated the record in the intro.

← Older revision		Revision as of 04:48, 25 October 2026
Line 2:		Line 2:
	For any recursively enumerable 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 recursively enumerable 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 ~~230~~</math>		<math display="block">6 \le N_{ZF} \le 215</math>

	This lower bound comes from the fact that [[BB(5)]] has been proven in Rocq.<ref group="footnote">The fact that this theorem has been proven in Rocq technically does not imply that the theorem must be provable in ZF, because the consistency strength of Rocq is actually higher than that of ZF. However, the BB(5) proof does not use any techniques that could not be formalized within ZF.</ref> 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.		This lower bound comes from the fact that [[BB(5)]] has been proven in Rocq.<ref group="footnote">The fact that this theorem has been proven in Rocq technically does not imply that the theorem must be provable in ZF, because the consistency strength of Rocq is actually higher than that of ZF. However, the BB(5) proof does not use any techniques that could not be formalized within ZF.</ref> 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.

KinataKnight: /* History */ Adding links to History of ZF records table and the new record.

2026-10-25T04:33:05Z

History: Adding links to History of ZF records table and the new record.

← Older revision		Revision as of 04:33, 25 October 2026
Line 93:		Line 93:
	\|230		\|230
	\|19 Oct 2026		\|19 Oct 2026
	\|Elliot Glazer		\|[https://x.com/ElliotGlazer Elliot Glazer] with use of ChatGPT, formalized with GPT and Claude
	\|[https://github.com/elliotglazer/k230-rocq Github]		\|[https://github.com/elliotglazer/k230-rocq Github]
	\|[https://github.com/elliotglazer/k230-rocq Rocq file]		\|[https://github.com/elliotglazer/k230-rocq Rocq file]
			\|-
			\|215
			\|21 Oct 2026
			\|[[wikipedia:Cleo_(mathematician)\|Vladimir Reshetnikov]] formalized with Claude
			\|[https://github.com/VladimirReshetnikov/ProveIt/tree/c9dc79323429112c698100f3226a6e4d56c8b782/Computability/BusyBeaver/Research/ZFC/k225-formal Github]
			\|[https://github.com/VladimirReshetnikov/ProveIt/tree/c9dc79323429112c698100f3226a6e4d56c8b782/Computability/BusyBeaver/Research/ZFC/k225-formal/verification/k215 Rocq file]
	\|}		\|}
	[[File:ZFC Machine 254.png\|thumb\|The transition table of the machine with 254 states. The initial state is 1.]]		[[File:ZFC Machine 254.png\|thumb\|The transition table of the machine with 254 states. The initial state is 1.]]

1something at 23:50, 20 October 2026

2026-10-20T23:50:43Z

← Older revision		Revision as of 23:50, 20 October 2026
Line 2:		Line 2:
	For any recursively enumerable 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 recursively enumerable 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 ~~254~~</math>		<math display="block">6 \le N_{ZF} \le 230</math>

	This lower bound comes from the fact that [[BB(5)]] has been proven in Rocq.<ref group="footnote">The fact that this theorem has been proven in Rocq technically does not imply that the theorem must be provable in ZF, because the consistency strength of Rocq is actually higher than that of ZF. However, the BB(5) proof does not use any techniques that could not be formalized within ZF.</ref> 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.		This lower bound comes from the fact that [[BB(5)]] has been proven in Rocq.<ref group="footnote">The fact that this theorem has been proven in Rocq technically does not imply that the theorem must be provable in ZF, because the consistency strength of Rocq is actually higher than that of ZF. However, the BB(5) proof does not use any techniques that could not be formalized within ZF.</ref> 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.

Tlonuqbar: progress city

2026-10-19T22:23:22Z

progress city

← Older revision		Revision as of 22:23, 19 October 2026
Line 22:		Line 22:
	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. The Aaronson-Yedida machine used a compiler called ''Laconic'', which was then updated with NQL or "Not Quite Laconic", while the current champion machines use a compiler built by Andrew J. Wade.		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. The Aaronson-Yedida machine used a compiler called ''Laconic'', which was then updated with NQL or "Not Quite Laconic", while the current champion machines use a compiler built by Andrew J. Wade.

	Note that ~~these~~ results ~~also~~ have ~~not undergone formal~~ verification, with the 7910 machine in particular relying on a result from Harvey Friedman that has no published proof.		Note that only the results with a linked formal verification are known to have such a verification, with the 7910 machine in particular relying on a result from Harvey Friedman that has no published proof.
	{\| class="wikitable"		{\| class="wikitable"
	\|+History of ZF independent TMs		\|+History of ZF independent TMs
Line 90:		Line 90:
	\|[https://github.com/jeff87654/busy-beaver/tree/zf-254/ZF/m254 Github]		\|[https://github.com/jeff87654/busy-beaver/tree/zf-254/ZF/m254 Github]
	\|[https://github.com/jeff87654/busy-beaver/tree/zf-254/ZF/m254 Rocq file]		\|[https://github.com/jeff87654/busy-beaver/tree/zf-254/ZF/m254 Rocq file]
			\|-
			\|230
			\|19 Oct 2026
			\|Elliot Glazer
			\|[https://github.com/elliotglazer/k230-rocq Github]
			\|[https://github.com/elliotglazer/k230-rocq Rocq file]
	\|}		\|}
	[[File:ZFC Machine 254.png\|thumb\|The transition table of the machine with 254 states. The initial state is 1.]]		[[File:ZFC Machine 254.png\|thumb\|The transition table of the machine with 254 states. The initial state is 1.]]
Line 110:		Line 116:
	\|		\|
	\|}		\|}
	This machine takes Wade's ZF champion and replaces the set theory axioms with one axiom schema of "adjunction + separation", which has been shown to interpret PA.<ref>https://mathoverflow.net/questions/508137/interpreting-pa-with-only-adjunction-separation/508161</ref>		This machine takes Wade's ZF champion and replaces the set theory axioms with one axiom schema of "adjunction + separation", which has been shown to interpret PA.<ref>https://mathoverflow.net/questions/508137/interpreting-pa-with-only-adjunction-separation/508161</ref> However,

	=== Large cardinals ===		=== Large cardinals ===

Tlonuqbar: 254 is definitely more verified than 432

2026-10-18T07:30:15Z

254 is definitely more verified than 432

← Older revision		Revision as of 07:30, 18 October 2026
Line 2:		Line 2:
	For any recursively enumerable 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 recursively enumerable 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 ~~432~~</math>		<math display="block">6 \le N_{ZF} \le 254</math>

	This lower bound comes from the fact that [[BB(5)]] has been proven in Rocq.<ref group="footnote">The fact that this theorem has been proven in Rocq technically does not imply that the theorem must be provable in ZF, because the consistency strength of Rocq is actually higher than that of ZF. However, the BB(5) proof does not use any techniques that could not be formalized within ZF.</ref> 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.		This lower bound comes from the fact that [[BB(5)]] has been proven in Rocq.<ref group="footnote">The fact that this theorem has been proven in Rocq technically does not imply that the theorem must be provable in ZF, because the consistency strength of Rocq is actually higher than that of ZF. However, the BB(5) proof does not use any techniques that could not be formalized within ZF.</ref> 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.

GrishaKir: /* History */

2026-10-15T13:02:58Z

History

← Older revision		Revision as of 13:02, 15 October 2026
Line 91:		Line 91:
	\|[https://github.com/jeff87654/busy-beaver/tree/zf-254/ZF/m254 Rocq file]		\|[https://github.com/jeff87654/busy-beaver/tree/zf-254/ZF/m254 Rocq file]
	\|}		\|}
			[[File:ZFC Machine 254.png\|thumb\|The transition table of the machine with 254 states. The initial state is 1.]]
	Wade's 432-state champion also omits the [[wikipedia:Axiom_of_regularity\|axiom of regularity]], as ZF-regularity is also equiconsistent with ZF.		Wade's 432-state champion also omits the [[wikipedia:Axiom_of_regularity\|axiom of regularity]], as ZF-regularity is also equiconsistent with ZF.

Tlonuqbar: idk how to mention AI in discoveries

2026-10-14T06:13:46Z

idk how to mention AI in discoveries

← Older revision		Revision as of 06:13, 14 October 2026
Line 87:		Line 87:
	\|254		\|254
	\|13 Oct 2026		\|13 Oct 2026
	\|[https://x.com/_mira___mira_ Mira], formalized by [https://github.com/jeff87654 Jeff Ketchersid] with ~~use of ChatGPT and~~ Claude		\|[https://x.com/_mira___mira_ Mira] with use of ChatGPT, formalized by [https://github.com/jeff87654 Jeff Ketchersid] with Claude
	\|[https://github.com/jeff87654/busy-beaver/tree/zf-254/ZF/m254 Github]		\|[https://github.com/jeff87654/busy-beaver/tree/zf-254/ZF/m254 Github]
	\|[https://github.com/jeff87654/busy-beaver/tree/zf-254/ZF/m254 Rocq file]		\|[https://github.com/jeff87654/busy-beaver/tree/zf-254/ZF/m254 Rocq file]

Tlonuqbar: these are admittedly AI led proofs and formalizations

2026-10-14T06:13:04Z

these are admittedly AI led proofs and formalizations

← Older revision		Revision as of 06:13, 14 October 2026
Line 87:		Line 87:
	\|254		\|254
	\|13 Oct 2026		\|13 Oct 2026
	\|[https://x.com/_mira___mira_ Mira], formalized by [https://github.com/jeff87654 Jeff Ketchersid]		\|[https://x.com/_mira___mira_ Mira], formalized by [https://github.com/jeff87654 Jeff Ketchersid] with use of ChatGPT and Claude
	\|[https://github.com/jeff87654/busy-beaver/tree/zf-254/ZF/m254 Github]		\|[https://github.com/jeff87654/busy-beaver/tree/zf-254/ZF/m254 Github]
	\|[https://github.com/jeff87654/busy-beaver/tree/zf-254/ZF/m254 Rocq file]		\|[https://github.com/jeff87654/busy-beaver/tree/zf-254/ZF/m254 Rocq file]

Tlonuqbar: new result

2026-10-14T06:12:18Z

new result

← Older revision		Revision as of 06:12, 14 October 2026
Line 84:		Line 84:
	\|[https://codeberg.org/ajwade/turing_machine_explorer/commit/33b30300054242201a95679aacf7e74312bd8803b0df9a85d2314095efd6804e git commit]		\|[https://codeberg.org/ajwade/turing_machine_explorer/commit/33b30300054242201a95679aacf7e74312bd8803b0df9a85d2314095efd6804e git commit]
	\|		\|
			\|-
			\|254
			\|13 Oct 2026
			\|[https://x.com/_mira___mira_ Mira], formalized by [https://github.com/jeff87654 Jeff Ketchersid]
			\|[https://github.com/jeff87654/busy-beaver/tree/zf-254/ZF/m254 Github]
			\|[https://github.com/jeff87654/busy-beaver/tree/zf-254/ZF/m254 Rocq file]
	\|}		\|}