Logical independence - Revision history

Tlonuqbar: more history

2026-09-05T21:59:04Z

more history

← Older revision		Revision as of 21:59, 5 September 2026
Line 31:		Line 31:
	\|Adam Yedidia and Scott Aaronson		\|Adam Yedidia and Scott Aaronson
	\|Yedidia 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>		\|Yedidia 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>
			\|
			\|-
			\|1919
			\|15 May 2016
			\|Stefan O'Rear
			\|[https://github.com/sorear/metamath-turing-machines/blob/master/machines/2016-zf-sorear-1919/zf.nql Github NQL file], [https://groups.google.com/g/metamath/c/OumBq83Ksqs/m/FogyOlLIBwAJ Metamath Group Announcement]
	\|		\|
	\|-		\|-
Line 36:		Line 42:
	\|May 2016		\|May 2016
	\|Stefan O’Rear		\|Stefan O’Rear
	\|[https://github.com/sorear/metamath-turing-machines/blob/master/machines/2017-zf-sorear-748/zf2.nql Github NQL ~~file~~], Busy Beaver Frontier<ref name=":0" />		\|[https://github.com/sorear/metamath-turing-machines/blob/master/machines/2017-zf-sorear-748/zf2.nql Github NQL], Busy Beaver Frontier<ref name=":0" />
	\|		\|
	\|-		\|-

Tlonuqbar: fixing deadlink

2026-08-02T08:19:20Z

fixing deadlink

← Older revision		Revision as of 08:19, 2 August 2026
Line 36:		Line 36:
	\|May 2016		\|May 2016
	\|Stefan O’Rear		\|Stefan O’Rear
	\|[https://github.com/sorear/metamath-turing-machines/blob/master/zf2.nql Github NQL file], Busy Beaver Frontier<ref name=":0" />		\|[https://github.com/sorear/metamath-turing-machines/blob/master/machines/2017-zf-sorear-748/zf2.nql Github NQL file], Busy Beaver Frontier<ref name=":0" />
	\|		\|
	\|-		\|-

Tlonuqbar: github name

2026-08-02T08:15:45Z

github name

← Older revision		Revision as of 08:15, 2 August 2026
Line 90:		Line 90:
	\|372		\|372
	\|11 February 2026		\|11 February 2026
	\|@LegionMammal978		\|@LegionMammal978 (Matthew House)
	\|[https://github.com/LegionMammal978/turing_machine_explorer/blob/main/pa.py Github]		\|[https://github.com/LegionMammal978/turing_machine_explorer/blob/main/pa.py Github]
	\|		\|

Tlonuqbar: /* History */ regularity equiconsistence

2026-07-29T04:53:02Z

History: regularity equiconsistence

← Older revision		Revision as of 04:53, 29 July 2026
Line 76:		Line 76:
	\|}		\|}

	Wade's 432-state champion also omits the [[wikipedia:Axiom_of_regularity\|axiom of regularity]].		Wade's 432-state champion also omits the [[wikipedia:Axiom_of_regularity\|axiom of regularity]], as ZF-regularity is also equiconsistent with ZF.

	For Peano Arithmetic, the ZF independent machines are an upper bound. In general, a machine that is independent of a theory will also be independent of any theory with strictly lower [[wikipedia:Equiconsistency#Consistency_strength\|consistency strength]]. For the theories in this article, Con(ZFC+Subtle)->Con(ZFC)->Con(PA).		For Peano Arithmetic, the ZF independent machines are an upper bound. In general, a machine that is independent of a theory will also be independent of any theory with strictly lower [[wikipedia:Equiconsistency#Consistency_strength\|consistency strength]]. For the theories in this article, Con(ZFC+Subtle)->Con(ZFC)->Con(PA).

C7X: More common phrasing /* Large cardinals */

2026-03-14T18:34:13Z

More common phrasing Large cardinals

← Older revision		Revision as of 18:34, 14 March 2026
Line 113:		Line 113:
	\|		\|
	\|}		\|}
	This machine takes Wade's ZF champion and adds the [[wikipedia:Axiom_of_choice\|axiom of Choice]] and a statement from Harvey Friedman (Proposition 4.3 of [https://bpb-us-w2.wpmucdn.com/u.osu.edu/dist/1/1952/files/2014/01/PrimitiveIndResults071302-189vmn0.pdf "Primitive Independence Results"])<ref>H. Friedman, "[https://bpb-us-w2.wpmucdn.com/u.osu.edu/dist/1/1952/files/2014/01/PrimitiveIndResults071302-189vmn0.pdf Primitive Independence Results]" (2002). Accessed February 2026.</ref> which Friedman showed ~~with ZFC~~ to be equivalent to "There exist arbitrarily large subtle cardinals".		This machine takes Wade's ZF champion and adds the [[wikipedia:Axiom_of_choice\|axiom of Choice]] and a statement from Harvey Friedman (Proposition 4.3 of [https://bpb-us-w2.wpmucdn.com/u.osu.edu/dist/1/1952/files/2014/01/PrimitiveIndResults071302-189vmn0.pdf "Primitive Independence Results"])<ref>H. Friedman, "[https://bpb-us-w2.wpmucdn.com/u.osu.edu/dist/1/1952/files/2014/01/PrimitiveIndResults071302-189vmn0.pdf Primitive Independence Results]" (2002). Accessed February 2026.</ref> which Friedman showed to be equivalent to "There exist arbitrarily large subtle cardinals" over ZFC.

	For reference, this theory is between the strength of "strongly unfoldable" and "<math>0^\sharp</math> exists" on the [[wikipedia:Large_cardinal\|large cardinal hierarchy]] on Wikipedia.		For reference, this theory is between the strength of "strongly unfoldable" and "<math>0^\sharp</math> exists" on the [[wikipedia:Large_cardinal\|large cardinal hierarchy]] on Wikipedia.

Tlonuqbar at 02:03, 12 March 2026

2026-03-12T02:03:13Z

← Older revision		Revision as of 02:03, 12 March 2026
Line 6:		Line 6:
	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.

	Harvey Friedman spoke of embedding consistency statements within turing machines in a [https://fomarchive.ugent.be/2004-March/008003.html 2004 posting] on the "Foundations of Mathematics" mailing list. Scott Aaronson conjectured in his [[Busy Beaver Frontier]] survey 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]. Scott also mentioned (crediting Oscar Cunningham for the observation) that if there is an n-state machine that is halts if and only if T is inconsistent, then <math>PA</math> + “BB(n) = b” can prove the consistency of T, where b is the true value of BB(n).<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>		Harvey Friedman spoke of embedding consistency statements within turing machines in a [https://fomarchive.ugent.be/2004-March/008003.html 2004 posting] on the "Foundations of Mathematics" mailing list. Scott Aaronson conjectured in his [[Busy Beaver Frontier]] survey 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]. Scott also mentioned (crediting Oscar Cunningham for the observation) that if there is an n-state machine that halts if and only if T is inconsistent, then <math>PA</math> + “BB(n) = b” can prove the consistency of T, where b is the true value of BB(n).<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>

	== Axiom of Choice ==		== Axiom of Choice ==

Tlonuqbar: simplify

2026-03-12T02:02:58Z

simplify

← Older revision		Revision as of 02:02, 12 March 2026
Line 6:		Line 6:
	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.

	Harvey Friedman spoke of embedding consistency statements within turing machines in a [https://fomarchive.ugent.be/2004-March/008003.html 2004 posting] on the "Foundations of Mathematics" mailing list. Scott Aaronson conjectured in his [[Busy Beaver Frontier]] survey 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]. Scott also mentioned (crediting Oscar Cunningham for the observation) that if there is an n-state machine that is ~~nonhalting~~ if and only if T is ~~consistent~~, then <math>PA</math> + “BB(n) = b” can prove the consistency of T, where b is the true value of BB(n).<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>		Harvey Friedman spoke of embedding consistency statements within turing machines in a [https://fomarchive.ugent.be/2004-March/008003.html 2004 posting] on the "Foundations of Mathematics" mailing list. Scott Aaronson conjectured in his [[Busy Beaver Frontier]] survey 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]. Scott also mentioned (crediting Oscar Cunningham for the observation) that if there is an n-state machine that is halts if and only if T is inconsistent, then <math>PA</math> + “BB(n) = b” can prove the consistency of T, where b is the true value of BB(n).<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>

	== Axiom of Choice ==		== Axiom of Choice ==

Tlonuqbar: clarifying

2026-03-12T01:54:42Z

clarifying

← Older revision		Revision as of 01:54, 12 March 2026
Line 6:		Line 6:
	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.

	Harvey Friedman spoke of embedding consistency statements within turing machines in a [https://fomarchive.ugent.be/2004-March/008003.html 2004 posting] on the "Foundations of Mathematics" mailing list. Scott Aaronson conjectured in his [[Busy Beaver Frontier]] survey 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]. Scott also mentioned (crediting Oscar Cunningham for the observation) that ~~for any theory T,~~ there ~~exists a number~~ n ~~such~~ that ~~the theory~~ <math>PA</math> + “BB(n) = b” can prove the consistency of T, where b is the true value of BB(n).<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>		Harvey Friedman spoke of embedding consistency statements within turing machines in a [https://fomarchive.ugent.be/2004-March/008003.html 2004 posting] on the "Foundations of Mathematics" mailing list. Scott Aaronson conjectured in his [[Busy Beaver Frontier]] survey 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]. Scott also mentioned (crediting Oscar Cunningham for the observation) that if there is an n-state machine that is nonhalting if and only if T is consistent, then <math>PA</math> + “BB(n) = b” can prove the consistency of T, where b is the true value of BB(n).<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>

	== Axiom of Choice ==		== Axiom of Choice ==

Tlonuqbar: correcting statement

2026-03-12T01:50:30Z

correcting statement

← Older revision		Revision as of 01:50, 12 March 2026
Line 6:		Line 6:
	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.

	Harvey Friedman spoke of embedding consistency statements within turing machines in a [https://fomarchive.ugent.be/2004-March/008003.html 2004 posting] on the "Foundations of Mathematics" mailing list. Scott Aaronson conjectured in his [[Busy Beaver Frontier]] survey 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]. Scott also mentioned (crediting Oscar Cunningham for the observation) ~~how if BB(n) is independent of some formal~~ theory T ~~for~~ a ~~value~~ n, the theory <math>PA</math> + “BB(n) = b” can prove the consistency of T, where b is the true value of BB(n).<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>		Harvey Friedman spoke of embedding consistency statements within turing machines in a [https://fomarchive.ugent.be/2004-March/008003.html 2004 posting] on the "Foundations of Mathematics" mailing list. Scott Aaronson conjectured in his [[Busy Beaver Frontier]] survey 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]. Scott also mentioned (crediting Oscar Cunningham for the observation) that for any theory T, there exists a number n such that the theory <math>PA</math> + “BB(n) = b” can prove the consistency of T, where b is the true value of BB(n).<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>

	== Axiom of Choice ==		== Axiom of Choice ==

Tlonuqbar: crediting oscar cunningham

2026-03-12T01:28:29Z

crediting oscar cunningham

← Older revision		Revision as of 01:28, 12 March 2026
Line 6:		Line 6:
	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.

	Harvey Friedman spoke of embedding consistency statements within turing machines in a [https://fomarchive.ugent.be/2004-March/008003.html 2004 posting] on the "Foundations of Mathematics" mailing list. Scott Aaronson conjectured in his [[Busy Beaver Frontier]] survey 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]. ~~Aaronson~~ also mentioned how if BB(n) is independent of some formal theory T for a value n, the theory <math>PA</math> + “BB(n) = b” can prove the consistency of T, where b is the true value of BB(n).<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>		Harvey Friedman spoke of embedding consistency statements within turing machines in a [https://fomarchive.ugent.be/2004-March/008003.html 2004 posting] on the "Foundations of Mathematics" mailing list. Scott Aaronson conjectured in his [[Busy Beaver Frontier]] survey 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]. Scott also mentioned (crediting Oscar Cunningham for the observation) how if BB(n) is independent of some formal theory T for a value n, the theory <math>PA</math> + “BB(n) = b” can prove the consistency of T, where b is the true value of BB(n).<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>

	== Axiom of Choice ==		== Axiom of Choice ==