The set.mm Axiom Table

every axiomatic assertion in set.mm, and how much rests on it

A formal library's foundation is usually described rather than counted. This is the count: all 3,004 axiomatic assertions in set.mm, each with how many of the library's 47,621 theorems reach it.

The three kinds have to be kept apart or the total means nothing. 118 are logical or set-theoretic axioms, 1,329 are definitions, and 1,344 are well-formedness constructors carrying no mathematical content — wi says an implication is a formula. All three are $a statements and a naive count adds them together.

Measured with gonzalgo · Metamath set.mm · proof closure of all 47,621 theorems, taken from the database's own proof structure

Showing the first 120 of 3,004 rows. The tail is mostly definitions used by a handful of theorems. The full set is in the JSON and the CSV.

entry points counts theorems whose own proof names this statement directly, as opposed to reaching it through another theorem. amplification is dependents per entry point, left blank where nothing cites it directly. Do not rank on amplification. It is a property of how the library was factored, not of the mathematics, and the Entry-Point Table gives the argument. theorems depending counts theorems whose proof closure reaches this statement, so it includes everything inherited through other theorems rather than only direct citations. A count of 0 means no theorem in the library reaches it at all.

Get the data

setmm-axioms.json · setmm-axioms.csv · CC-BY-4.0 · version 2026-08-13

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

Every figure comes from set.mm's own proof structure. Method: 10.5281/zenodo.21769846.

The concentration

ax-mp, modus ponens, is reached by 47,562 theorems — 99.9% of the library. ax-gen reaches 44,537. The top of this table is not a ranking so much as a description of what it means to be a logical foundation: nearly everything rests on nearly all of it.

The interesting part is how fast it falls away. Past the propositional and first-order core the counts drop into the hundreds and then the single digits, which is why a measure of what a theorem rests on is worth computing rather than assuming.

Declared and never reached

213 of these statements are reached by no theorem in the library, and 8 of them are axioms: ax-10d, ax-11d, ax-7d, ax-8d, ax-9d1, ax-9d2, ax-wl-clel, ax-wl-cleq. A declared axiom nothing depends on is not a defect, a database can state a principle for completeness, or keep one for a development that was never built out, but it is the kind of fact that is easier to measure than to remember.

One proof step, ninety-three percent of the library

ax-4 is cited directly in exactly one proof and reached by 44,501 theorems — 93.4% of set.mm. That is the whole case for computing provenance rather than reading a changelog: the set of theorems that use an axiom and the set that depend on it are almost disjoint, and only one of them is visible by inspection.

Where the 1,447 comes from

The Entry-Point Table reports 1,447 axioms used for set.mm. That figure is the 118 axioms plus the 1,329 definitions that at least one theorem reaches, and it excludes both the syntax constructors and everything nothing reaches. This table is where that number decomposes.