metamath(1)

1metamath(1)                      User Manuals                      metamath(1)
2
3
4

NAME

6       metamath - Formal proof verifier and proof assistant
7

SYNOPSIS

9       metamath [ commands | file ]
10

DESCRIPTION

12       metamath  is  a formal proof verifier and proof assistant for the Meta‐
13       math language.  It can be initialized via a series of commands or  with
14       a data base file, which can then be explored interactively.
15
16       For details about the Metamath language and the command-line interface,
17       type help into the command prompt, or read the Metamath book [1], which
18       should have been installed along with the package.
19

LANGUAGE

21       A  Metamath  database  consists  of a sequence of three kinds of tokens
22       separated by white space (which is any sequence of one  or  more  white
23       space characters). The set of keyword tokens is ${, $}, $c, $v, $f, $e,
24       $d, $a, $p, $., $=, $(, $), $[, and $].  The  latter  four  are  called
25       auxiliary or preprocessing keywords. A label token consists of any com‐
26       bination of letters, digits, and the characters hyphen, underscore, and
27       period.   The  label of an assertion is used to refer to it in a proof.
28       A math symbol token may consist of any combination of the 93  printable
29       ascii(7) characters other than $.  All tokens are case-sensitive.
30
31       $( comment $)
32              Comments are ignored.
33
34       $[ file $]
35              Include the contents of a file.
36
37       ${ statements $}
38              Scoped  block  of  statements. A math symbol becomes active when
39              declared and stays active until the end of the block in which it
40              is declared.
41
42       $v symbols $.
43              Declare  symbols  as variables. A variable may not be declared a
44              second time while it is active, but it may be declared again (as
45              a variable, but not as a constant) after it becomes inactive.
46
47       $c symbols $.
48              Declare symbols as constants. A constant must be declared in the
49              outermost block and may not be declared a second time.
50
51       label $f constant variable $.
52              Variable-type hypothesis to specify the  nature  or  type  of  a
53              variable  (such as `let x be an integer.'). A variable must have
54              its type specified in a $f statement before it may be used in  a
55              $e,  $a,  or $p statement. There may not be two active $f state‐
56              ments containing the same variable.
57
58       label $e constant symbols $.
59              Logical hypothesis, expressing a logical truth (such as  `assume
60              x  is prime') that must be established in order for an assertion
61              requiring it to also be true.
62
63       $d variables $.
64              Disjoint variable restriction. For distinct active variables, it
65              forbids the substitution of one variable with another.
66
67       label $a constant symbols $.
68              Axiomatic assertion.
69
70       label $p constant symbols $= proof $.
71              Provable assertion. The proof is a sequence of statement labels.
72              This label sequence serves as a set  of  instructions  that  the
73              Metamath  program  uses  to  construct  a  series of math symbol
74              sequences. The construction must ultimately result in  the  math
75              symbol  sequence contained between the $p and $= keywords of the
76              $p statement. For details, see section 4.3 in [1].   Proofs  are
77              most easily written using the interactive prompt in metamath.
78

FILES

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

NAME

SYNOPSIS

DESCRIPTION

LANGUAGE

FILES

SEE ALSO