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.

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-12

One of the gonzalgo indexes — standing measurements of what formal libraries rest on, remeasured as the libraries move.

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.

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.