metamath - Formal proof verifier and proof assistant
metamath [ commands | file
]
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.
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.
/usr/share/metamath
Data base files for several formal theories.