THE CHOICE STRENGTH TABLE

not whether a theorem uses choice, but how much of it

“Depends on choice” is usually reported as one bit. set.mm declares three choice principles as separate axioms, so for this library it does not have to be.

Of 47,621 theorems, 1,528 reach one (3.21%). 583 need full choice. 879 need only countable choice. 66 need only dependent choice. The weaker principle carries more of the library than the strong one does.

Measured with gonzalgo · Metamath set.mm · proof closure of all 47,621 theorems against ax-ac, ax-ac2, ax-cc and ax-dc

Showing the first 120 of 1,528 rows. Grouped by principle, strongest first. The full set is in the JSON and the CSV.

strongest partitions these theorems: a theorem reaching full choice is counted there even if it also reaches the weaker principles. The raw memberships overlap and are in the data — 583 reach full choice, 1016 reach countable, 88 reach dependent, with 137 theorems in both full and countable alone.

Get the data

choice-strength.json · choice-strength.csv · CC-BY-4.0 · version 2026-08-12

One of the gonzalgo indexes — standing measurements of what formal libraries rest on, remeasured as the libraries move. Cite the series as 10.5281/zenodo.21900625, which resolves to the current deposit.

Reproduce it

pip install gonzalgo
gonzalgo mm set.mm

Method: 10.5281/zenodo.21769846.

The weaker axiom does more work

1016 theorems reach countable choice against 583 reaching choice proper. Countable choice is the weaker principle and it is load-bearing for more of this library, which is not what a single choice-dependence figure would suggest.

It also changes what a repair would mean. A theorem resting only on countable choice is already closer to a constructive setting than the same theorem resting on full choice, and reporting both as “classical” erases the distinction the database went to the trouble of making.

Why this differs from the Kernel Index figure

The Kernel Index reports set.mm at 1.22%, which is 583 theorems reaching full choice over 47,621. Counting every choice principle gives 1,528, or 3.21%. Neither number is wrong; they answer different questions, and this table is where the difference is visible rather than implicit.

Lean has no counterpart to this row. Classical.choice is a single axiom with no weaker sibling in the core, so a Lean library cannot be stratified this way at all — the distinction exists here because set.mm's authors declared the principles separately.