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⟩.