metamath - Formal proof verifier and proof assistant

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.

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

       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.

       $vsymbols$.
              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.

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

       label$fconstantvariable$.
              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$econstantsymbols$.
              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.

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

       label$aconstantsymbols$.
              Axiomatic assertion.

       label$pconstantsymbols$=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.

       metamath - Formal proof verifier and proof assistant

[1] Norman Megill: Metamath, A Computer Language for Pure Mathematics.

Metamath                                           2018-02-04                                        metamath(1)

metamath[commands|file]