Metamath - A Generic Proof Checker

A Generic Proof Checker

Metamath has no specific logic embedded and can simply be regarded as a device to apply inference rules to formulas. Simplicity is the master concept in the design of Metamath: the language of Metamath, employed to state the definitions, axioms, inference rules and theorems is only composed of a handful of keywords, and all the proofs are checked using one simple algorithm based on the substitution of variables (with optional provisos for what variables must remain distinct after a substitution is made). This "substitution" is just the simple replacement of a variable with an expression and not the proper substitution described in works on predicate calculus.

Even if Metamath is used for mathematical proof checking, its algorithm is so general we can extend the field of its usage. In fact Metamath could be used with every sort of formal systems: the checking of a computer program could be considered (even if Metamath's low level would make it difficult); it could possibly even be a syntactic checker for a natural language (same remark). Because Metamath has a very generic concept of what a proof is (namely a tree of formulas connected by inference rules) and no specific logic is embedded in the software, Metamath can be used with species of logic as different as Hilbert-style logics or sequents-based logics or even with lambda calculus. In contrast, it is largely incompatible with logical systems which uses other things than formulas and inference rules. The original natural deduction system (due to Gerhard Gentzen), which uses an extra stack, is an example of a system that cannot be implemented with Metamath. In the case of natural deduction however it is possible to append the stack to the formulas (transforming the natural deduction formulas into a sort of sequent) so that Metamath's requirements are met.

What makes Metamath so generic is its substitution algorithm. This algorithm makes no assumption about the used logic and only checks the substitutions of variables are correctly done.

So here is a detailed example of how this algorithm works. Steps 1 and 2 of the theorem 2p2e4 in set.mm are depicted left. Let's explain how Metamath uses its substitution algorithm to check that step 2 is the logical consequence of step 1 when you use the theorem opreq2i. Step 2 states that . It is the conclusion of the theorem opreq2i. The theorem opreq2i states that if, then . This theorem would never appear under this cryptic form in a textbook but its literate formulation is banal: when two quantities are equal, one can replace one by the other in an operation. To check the proof Metamath attempts to unify with . There is only one way to do so: unifying with, with, with and with . So now Metamath uses the premise of opreq2i. This premise states that . As a consequence of its previous computation, Metamath knows that should be substituted by and by . The premise becomes and thus step 1 is therefore generated. In its turn step 1 is unified with df-2. df-2 is the definition of the number 2 and states that 2 = ( 1 + 1 ). Here the unification is simply a matter of constants and is straightforward (no problem of variables to substitute). So the verification is finished and these two steps of the proof of 2p2e4 are correct.

There is however some complications that are not shown on the picture. When Metamath unifies with it has to check that the syntactical rules are respected. In fact has the type class thus Metamath has to check that is also typed class This is done using the same sort of unification described in the paragraph above.

The above explanation may let suppose that formulas are stored by Metamath. In fact nothing of that sort exists. Metamath only stores the conclusion and the premises of the proven theorem and the list of the names of the theorems used by the proof and nothing more. But since it is possible, with the substitution algorithm, to generate the conclusion from the premises nothing more is required.