Download Metamath book

38
CHAPTER 2. USING THE METAMATH PROGRAM
tr $f term r $.
ts $f term s $.
wp $f wff P $.
wq $f wff Q $.
$( Define "term" and "wff" $)
tze $a term 0 $.
tpl $a term ( t + r ) $.
weq $a wff t = r $.
wim $a wff ( P -> Q ) $.
$( State the axioms $)
a1 $a |- ( t = r -> ( t = s -> r = s ) ) $.
a2 $a |- ( t + 0 ) = t $.
$( Define the modus ponens inference rule $)
${
min $e |- P $.
maj $e |- ( P -> Q ) $.
mp $a |- Q $.
$}
$( Prove a theorem $)
th1 $p |- t = t $=
$( Here is its proof: $)
tt tze tpl tt weq tt tt weq tt a2 tt tze tpl
tt weq tt tze tpl tt weq tt tt weq wim tt a2
tt tze tpl tt tt a1 mp mp
$.
A “database” is a set of one or more ascii source files. Here’s a brief
description of this Metamath database (which consists of this single source
file), so that you can understand in general terms what is going on. To
understand the source file in detail, you should read Chapter 4.
The database is a sequence of “tokens,” which are normally separated by
spaces or carriage returns. The only tokens that are built into the Metamath
language are those beginning with $. These tokens are called “keywords.”
All other tokens are user-defined, and their names are arbitrary.
As you might have guessed, the Metamath token $( starts a comment
and $) ends a comment.
The Metamath tokens $c, $v, $e, $f, $a, and $p specify “statements”
that end with $. .
The Metamath tokens $c and $v each declare a list of user-defined tokens,
called “math symbols,” that the database will reference later on. All of the
math symbols they define you have seen earlier except the turnstile symbol
|- (`), which is commonly used by logicians to mean “a proof exists for.”
For us the turnstile is just a convenient symbol that distinguishes expressions
that are axioms or theorems from expressions that are terms or wffs.
The $c statement declares “constants” and the $v statement declares