Metamath - The Metamath Language

The Metamath Language

While the large database of proved theorems follows conventional ZFC set theory, the Metamath language is a metalanguage, suitable for developing a wide variety of formal systems.

The set of symbols that can be used for constructing formulas is declared using $c and $v statements; for example:

$( Declare the constant symbols we will use $) $c 0 + = -> ( ) term wff |- $. $( Declare the metavariables we will use $) $v t r s P Q $.

The grammar for formulas is specified using a combination of $f and $a statements; for example:

$( Specify properties of the metavariables $) tt $f term t $. tr $f term r $. ts $f term s $. wp $f wff P $. wq $f wff Q $. $( Define "wff" (part 1) $) weq $a wff t = r $. $( Define "wff" (part 2) $) wim $a wff ( P -> Q ) $.

Axioms and rules of inference are specified with $a statements along with ${ and $} for block scoping; for example:

$( State axiom a1 $) a1 $a |- ( t = r -> ( t = s -> r = s ) ) $. $( State axiom a2 $) a2 $a |- ( t + 0 ) = t $. ${ min $e |- P $. maj $e |- ( P -> Q ) $. $( Define the modus ponens inference rule $) mp $a |- Q $. $}

The metamath program can convert statements to more conventional TeX notation; for example, the modus ponens axiom from set.mm:

Using one construct, $a statements, to capture syntactic rules, axiom schemas, and rules of inference provides a level of flexibility similar to higher order logical frameworks without a dependency on a complex type system.

Theorems (and derived rules of inference) are written with $p statements; for example:

$( Prove a theorem $) th1 $p |- t = t $= $( Here is its proof: $) tt tze tpl tt weq tt tt weq tt a2 tt tze tpl tt weq tt tze tpl tt weq tt tt weq wim tt a2 tt tze tpl tt tt a1 mp mp $.

Note the inclusion of the proof in the $p statement. It abbreviates the following detailed proof:

1 tt $f term t 2 tze $a term 0 3 1,2 tpl $a term ( t + 0 ) 4 3,1 weq $a wff ( t + 0 ) = t 5 1,1 weq $a wff t = t 6 1 a2 $a |- ( t + 0 ) = t 7 1,2 tpl $a term ( t + 0 ) 8 7,1 weq $a wff ( t + 0 ) = t 9 1,2 tpl $a term ( t + 0 ) 10 9,1 weq $a wff ( t + 0 ) = t 11 1,1 weq $a wff t = t 12 10,11 wim $a wff ( ( t + 0 ) = t -> t = t ) 13 1 a2 $a |- ( t + 0 ) = t 14 1,2 tpl $a term ( t + 0 ) 15 14,1,1 a1 $a |- ( ( t + 0 ) = t -> ( ( t + 0 ) = t -> t = t ) ) 16 8,12,13,15 mp $a |- ( ( t + 0 ) = t -> t = t ) 17 4,5,6,16 mp $a |- t = t

The "essential" form of the proof elides syntactic details, leaving a more conventional presentation:

1 a2 $a |- ( t + 0 ) = t 2 a2 $a |- ( t + 0 ) = t 3 a1 $a |- ( ( t + 0 ) = t -> ( ( t + 0 ) = t -> t = t ) ) 4 2,3 mp $a |- ( ( t + 0 ) = t -> t = t ) 5 1,4 mp $a |- t = t