Week 7: Definitions and soundness

A Metamath definition is an axiom to the verifier, so a wrong one can make the database inconsistent without any proof failing. What the extra check is and which tool runs it.

19 April 2027

A definition in Metamath is written as an axiom, and the proof verifier cannot tell the two apart. The Metamath Proof Explorer’s note on definitions says so directly: “The only way to add a definition to a database is to introduce it as a new axiom.” Its example is the number 2. Change df-2 from 2 = ( 1 + 1 ) to the self-referential 2 = ( 1 + 2 ) and 0 = 1 becomes provable, while the verifier, which sees only one more $a statement, “is perfectly content to use it as a new fact and does not issue an error message.”

So a proof check is not enough: the five verifiers that re-check set.mm on every change only ask whether each proof follows from the statements before it. The Metamath Zero README puts it as one of Metamath’s soundness issues: “Definitions are just axioms in Metamath. There are tools in the Metamath ecosystem to check that definitions are conservative, but they are not built in to the verifier”.

What the check is

The same note gives the standard. A definition is sound if it is eliminable (any theorem using the defined symbol can be rewritten as an equivalent one without it) and conservative (after that rewriting, the theorem is still provable from the original axioms). In plain words: the new symbol is an abbreviation you could always expand away, and expanding it adds nothing the axioms could not already prove.

Which tool performs it

set.mm’s own documentation says “definitions are checked by mmj2”. The Proof Explorer note records that Mario Carneiro added the check to mmj2 and that it verifies “all but four definitions”: df-bi, df-clab, df-cleq and df-clel “need to be justified with metalogic outside of mmj2’s capabilities.”

In mmj2’s batch documentation the check “runs a soundness check on all axioms in the database, except those specified in the list.” The recommended exclusions are ax-*,df-bi,df-clab,df-cleq,df-clel, “which will always fail the check.” The RunParm SetMMDefinitionsCheckWithExclusions is deprecated in favour of RunMacro,definitionCheck,... with the same arguments, which is what Wednesday’s lab runs.

The definition exercise is set this week: a definition that passes this check, one that fails it, and a write-up of what the check caught.

Read

Teaching team