.\" t -*- coding: UTF-8 -*-
.\" Man page for metamath
.\"
.\" Copyright (C) 2018 Aaron Puchert.
.\"
.\" This program is free software; you can redistribute it and/or modify
.\" it under the terms of the GNU General Public License as published by
.\" the Free Software Foundation; either version 2 of the License, or
.\" (at your option) any later version.
.\"
.\" This program is distributed in the hope that it will be useful,
.\" but WITHOUT ANY WARRANTY; without even the implied warranty of
.\" MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
.\" GNU General Public License for more details.
.\"
.\" You should have received a copy of the GNU General Public License
.\" along with this program; if not, write to the Free Software
.\" Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
.\"
.TH metamath 1 "2018-02-04" Metamath "User Manuals"
.SH NAME
metamath \- Formal proof verifier and proof assistant
.SH SYNOPSIS
.BI "metamath [ " "commands" " | " "file" " ]"
.SH DESCRIPTION
.B metamath
is a formal proof verifier and proof assistant for the Metamath language.
It can be initialized via a series of
.I commands
or with a data base
.IR file ,
which can then be explored interactively.
.PP
For details about the Metamath language and the command-line interface, type
.B help
into the command prompt, or read the Metamath book [1], which should have been
installed along with the package.
.SH 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
.BR ${ ", " $} ", " $c ", " $v ", " $f ", " $e ", " $d ", " $a ", " $p ", "
.BR $. ", " $= ", " $( ", " $) ", " $[ ", and " $] .
The latter four are called auxiliary or preprocessing keywords. A
.I 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
.I symbol
token may consist of any combination of the 93 printable
.BR ascii (7)
characters other than
.BR $ .
All tokens are case-sensitive.
.TP
.BI $( " comment " $)
Comments are ignored.
.TP
.BI $[ " file " $]
Include the contents of a
.IR file .
.TP
.BI ${ " 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.
.TP
.BI $v " symbols " $.
Declare
.I 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.
.TP
.BI $c " symbols " $.
Declare
.I symbols
as constants. A constant must be declared in the outermost block and may not be
declared a second time.
.TP
.IB "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
.B $f
statement before it may be used in a
.BR $e ", " $a ", or " $p
statement. There may not be two active
.B $f
statements containing the same variable.
.TP
.IB "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.
.TP
.BI $d " variables " $.
Disjoint variable restriction. For distinct active
.IR variables ,
it forbids the substitution of one variable with another.
.TP
.IB "label " $a " constant symbols " $.
Axiomatic assertion.
.TP
.IB "label " $p " constant symbols " $= " proof " $.
Provable assertion. The
.I proof
is a sequence of statement
.IR label s.
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
.BR $p " and " $=
keywords of the
.B $p
statement. For details, see section 4.3 in [1].
Proofs are most easily written using the interactive prompt in
.BR metamath .
.SH FILES
.I /usr/share/metamath
.RS
Data base files for several formal theories.
.SH SEE ALSO
.B "[1]"
Norman Megill:
.UR http://us.metamath.org/downloads/metamath.pdf
Metamath, A Computer Language for Pure Mathematics
.UE .