During my research on various theorem provers, today I stumbled upon Metamath.
To me, what was interesting about it was its simplicity. You start by defining a formal system, i.e. variables, symbols, axioms, inference rules. Then you build new theorems based on the formal system.
The core concept behind Metamath is substitution, and it’s using RPN notation to build hypothesis on the stack and then rewrite them using the inference rules to reach conclusion.
The program is written in C, and I compiled it on both OS X and my Android phone. It’s pretty light-weight and compiles in a few milliseconds, and it’s also interesting that you can take it anywhere you want on your phone.
Metamath has no special syntax. It will tokenize a file that we give to it, and tokens that start with $ are Metamath tokens, while everything else are user-defined tokens.
Here is a list of built-in Metamath tokens:
- To define constants, use the
$ctoken. - To define variables, use the
$vtoken. - To define types of variables, use the
$ftoken. - To define essential hypothesis, use the
$etoken. - To define axioms, use the
$atoken. - To define proofs, use the
$ptoken. - To start proving in
$pstatement, use the$=token. - To end the statements above, use the
$.token. - To insert comments, use the
$(and$)tokens. - To define a block (has effect on scoping), use the
${and$}tokens. Note that only$aand$ptokens will remain outside the scope.
That’s basically it. The package has included demo example and an example for the MU puzzle as well. There are other systems as well (Peano, Set).
There are some basic rules as well:
- A hypothesis is either a
$eor a$fstatement - For every variable in
$e,$aor$p, we must have a$passertion, i.e. every variable in an essential hypothesis/axiom/proof must have a floating hypothesis (type) - A
$f,$e, or$dstatement is active from the place it occurs until the end of the block it occurs in. A$aor$pstatement is active from the place it occurs through the end of the database.
For the complete syntax you can refer to the Metamath book.
Now for the example we’ll use, start by creating a test.mm file. We’ll define a formal system and demonstrate the usage of modus ponens to come up with a new theorem, based on our initial axioms.
$( Declare the constant symbols we will use $)
$c -> ( ) wff |- I J $.
$( Declare the variables we will use $)
$v p q $.
$( Specify properties of the variables, i.e. they are wff formulas $)
wp $f wff p $.
wq $f wff q $.
$( Define "mp", for the modus ponens inference rule $)
${
mp1 $e |- p $.
mp2 $e |- ( p -> q ) $.
mp $a |- q $.
$}
$( Define our initial axioms. I and J are well-formed formulas,
we have a proof for I and we have conditional for I -> J $)
wI $a wff I $.
wJ $a wff J $.
wim $a wff ( p -> q ) $.
$( Prove that we can deduce J from the initial axioms. Note how we use
block scope here, since we don't want the hypothesis proof_I and
proof_I_imp_J to be visible outside of this scope. $)
${
$( Given I and I -> J $)
proof_I $e |- I $.§
proof_I_imp_J $e |- ( I -> J ) $.
$( Prove that we can deduce J $)
proof_J $p |- J $=
wI $( Stack: [ 'wff I' ] $)
wJ $( Stack: [ 'wff I', 'wff J' ] $)
$( Note that we had to specify wff for I and J before using mp,
since the types have to match, as set on line 8 and 9 $)
proof_I $( Stack: [ 'wff I', 'wff J', '|- I' ] $)
proof_I_imp_J $( Stack: [ 'wff I', 'wff J', '|- I', '|- ( I -> J )' ] $)
mp $( Stack: [ '|- J' ] $)
$.
$}
To verify our file, we run ./metamath 'read test.mm' 'verify proof *' exit.
Note how we had to separate wff from |-. Otherwise, if we just used |-, then all well formed formulas would be proven to be true, which doesn’t make much sense.
In addition to this, the reason why we have implication -> and turnstile provable assertion |- is that the former is a wff (i.e. statement in the object language) and works on propositions, while the latter is not a wff but rather a statement in the meta language and works on proofs.
The arrow -> is usually used to denote an “internalization” of the meaning of turnstile, into the object language. This allows us, in some sense (depending on the meaning ascribed to ->) to represent the relationships between hypotheses and conclusions in the object language, whereas without it it becomes difficult to reason about on a higher-order level (e.g. most systems do not allow A, (A |- B) |- B).
For more complete examples, you can check out:
- logic.mm – where I define a basic logical system that contains definitions for and-elim and and-intro and proves some theorems.
- peano.mm – where I define successor for natural numbers and prove some theorems about ordering of them.
Due to its minimalistic design, when compared to Coq it has no Calculus of Constructions, Inductive Types, etc.
To conclude, I think it’s a fun program to play with, but since it has no “real” framework, I don’t think it’s as industry ready as Coq.
bor0's reflective blog 