Logical independence

Theory	BB(n) is independent
ZF+Berkeley cardinal	1399
ZF+subtle cardinal	493
Zermelo-Fraenkel set theory	215
New Foundations	210
Peano arithmetic
PRA	—
EFA	—
IΔ₀	—

For any recursively enumerable and arithmetically sound axiomatic theory T, there exists an integer $N_T$ such that T cannot prove the values of BB(n) for any $n\ge N_T$. For Zermelo–Fraenkel set theory (ZF), this value is known to be in the range:

$$6\le N_{ZF}\le 215$$

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.

Harvey Friedman spoke of embedding consistency statements within turing machines in a 2004 posting on the "Foundations of Mathematics" mailing list. Scott Aaronson conjectured in his Busy Beaver Frontier survey that $N_{ZF}\le 20$ and $N_{PA}\le 10$, where $PA$ refers to the theory of 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 $PA$ + “BB(n) = b” can prove the consistency of T, where b is the true value of BB(n).

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

$$N_{ZFC}=N_{ZF}$$

Therefore we refer to ZF and $N_{ZF}$ throughout this article since adding the Axiom of Choice does not have any effect on Turing machine decidability.

History

In a broad sense, the concept of a mechanical or computable procedure that was equivalent to the consistency of a formal theory was discovered by Kurt Gödel's incompleteness theorem, which is notable for introducing a meta-mathematical encoding of the statement that "T can prove statement S" (the provability predicate) which is used in all these machines. This was further clarified by Alan Turing and Alonzo Church's work on a formal definition of computability.

Although not a traditional turing machine, in 2012 Merlin Carl and Boris Z. Moroz constructed a Diophantine Equation which had solutions if and only if NBG (Von Neumann–Bernays–Gödel set theory) is inconsistent. NBG is a conservative extension of ZFC, so solving this equation is independent of ZFC.

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. The results before 2026 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 432 machines use a compiler built by Andrew J. Wade. Many machines after 2026 have been generated by AI without a formal compiler.

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.

History of ZF independent TMs

States	Date	Discoverer	Source	Verification
7910	May 2016	Adam Yedidia and Scott Aaronson	Yedidia and Aaronson 2016
1919	15 May 2016	Stefan O'Rear	Github NQL file, Metamath Group Announcement
748	May 2016	Stefan O’Rear	Github NQL, Busy Beaver Frontier
745	July 2023	Johannes Riebel	Riebel 2023 Bachelor Thesis
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
335	11 Oct 2026	Jeff Ketchersid	discord message
254	13 Oct 2026	Mira with use of ChatGPT, formalized by Jeff Ketchersid with Claude	Github	Rocq file
230	19 Oct 2026	Elliot Glazer with use of ChatGPT, formalized with GPT and Claude	Github	Rocq file
215	21 Oct 2026	Vladimir Reshetnikov formalized with Claude	Github	Rocq file

The transition table of the ZF machine with 254 states. The initial state is 1.

Wade's 432-state champion also omits the axiom of regularity, as ZF-regularity is also equiconsistent with ZF.

New Foundations (NF)

New Foundations is a formal theory created by W.V.O. Quine in 1937, based around the principle of stratified comprehension of sets. It is known to be stronger than Peano Arithmetic and second-order arithmetic, but weaker than ZF.

History of New Foundations (NF) independent TMs

States	Date	Discoverer	Source	Verification
210	8 November 2026	@wlad-svennik		[1]

The formalized proof for this machine's NF-undecidability is formalized as an external Lean metatheorem rather than a completed PA-internal derivation. As of this publication, a fresh independent clean build and community review have not been reported.

Peano Arithmetic (PA)

For Peano Arithmetic, the ZF and NF independent machines are upper bounds. In general, a machine that is independent of a theory will also be independent of any theory with strictly lower consistency strength. For the theories in this article, Con(ZFC+Subtle)->Con(ZFC)->Con(NF)->Con(PA).

History of Peano Arithmetic (PA) independent TMs

States	Date	Discoverer	Source	Verification
372	11 February 2026	@LegionMammal978 (Matthew House)	Github

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.

Large cardinals

These tables are for theories stronger than ZFC.

History of ZFC + "There exist arbitrarily large subtle cardinals" independent TMs

States	Date	Discoverer	Source	Verification
493	25 February 2026	@LegionMammal978	Github

This machine takes Wade's ZF champion and adds the axiom of Choice and a statement from Harvey Friedman (Proposition 4.3 of "Primitive Independence Results") 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 "$0^{\mathrm{♯}}$ exists" on the large cardinal hierarchy on Wikipedia.

Note: The initial machine produced in 2016 by Yedidia and Aaronson is designed to halt iff a certain statement created by Harvey Friedman is true. According to Friedman (without a published proof), this statement is independent of the theory "Stationary Ramsey Property" or SRP, which is equiconsistent with the theory $ZFC+\{\text{``There is a }k\text{-subtle cardinal``}\mid k\in \mathbb{\mathbb{N}}\}$ which is also between the strength of "strongly unfoldable" and "$0^{\mathrm{♯}}$ exists" on the large cardinal hierarchy. However, the theory used by the BB(493) machine is also independent of this theory.

History of ZF + "There exists a Berkeley cardinal" independent TMs

States	Date	Discoverer	Source	Verification
1399	8 November 2026	@Meganeuridae	Github	Rocq file

Berkeley cardinals are perhaps the strongest family of large cardinals considered, initially proposed by Hugh Woodin at a lecture at UC Berkeley as an axiom that was "obviously inconsistent".^{[citation needed]} However, no inconsistency has been found and many people now believe it may be consistent. Berkeley cardinals are known to be inconsistent with the axiom of choice.