NAME

       metamath - Formal proof verifier and proof assistant

SYNOPSIS

       metamath [ commands | file ]

DESCRIPTION

       metamath is a formal proof verifier and proof assistant for the Metamath language.  It can be initialized
       via a series of commands or with a data base file, which can then be explored interactively.

       For details about the Metamath language and the  command-line  interface,  type  help  into  the  command
       prompt, or read the Metamath book [1], which should have been installed along with the package.

LANGUAGE

       A  Metamath  database  consists of a sequence of three kinds of tokens separated by white space (which is
       any sequence of one or more white space characters). The set of keyword tokens is ${, $}, $c, $v, $f, $e,
       $d,  $a, $p, $., $=, $(, $), $[, and $].  The latter four are called auxiliary or preprocessing keywords.
       A label token consists of any combination of letters, digits, and the characters hyphen, underscore,  and
       period.  The label of an assertion is used to refer to it in a proof.  A math symbol token may consist of
       any combination of the 93 printable ascii(7) characters other than $.  All tokens are case-sensitive.

       $( comment $)
              Comments are ignored.

       $[ file $]
              Include the contents of a file.

       ${ statements $}
              Scoped block of statements. A math symbol becomes active when declared and stays active until  the
              end of the block in which it is declared.

       $v symbols $.
              Declare symbols as variables. A variable may not be declared a second time while it is active, but
              it may be declared again (as a variable, but not as a constant) after it becomes inactive.

       $c symbols $.
              Declare symbols as constants. A constant must be declared in the outermost block and  may  not  be
              declared a second time.

       label $f constant variable $.
              Variable-type  hypothesis  to  specify  the  nature  or  type  of a variable (such as `let x be an
              integer.'). A variable must have its type specified in a $f statement before it may be used  in  a
              $e, $a, or $p statement. There may not be two active $f statements containing the same variable.

       label $e constant symbols $.
              Logical  hypothesis,  expressing  a  logical  truth  (such  as  `assume  x is prime') that must be
              established in order for an assertion requiring it to also be true.

       $d variables $.
              Disjoint variable restriction. For distinct active variables, it forbids the substitution  of  one
              variable with another.

       label $a constant symbols $.
              Axiomatic assertion.

       label $p constant symbols $= proof $.
              Provable  assertion. The proof is a sequence of statement labels.  This label sequence serves as a
              set of instructions that the Metamath program uses to construct a series of math symbol sequences.
              The  construction  must ultimately result in the math symbol sequence contained between the $p and
              $= keywords of the $p statement. For details, see section 4.3 in  [1].   Proofs  are  most  easily
              written using the interactive prompt in metamath.

FILES

       /usr/share/metamath
              Data base files for several formal theories.

SEE ALSO

       [1]     Norman     Megill:     Metamath,     A     Computer     Language     for     Pure     Mathematics
       ⟨http://us.metamath.org/downloads/metamath.pdf⟩.