sgo.to

Metamath

Sam Goto

These are my personal notes as I try to understand, parse and verify metamath.

I started by reading the book then a series of verifiers. I have found mmverify.py to be the easiest to follow, and much of the code here is inspired by it.

This is a metamath comment statement:

$( hello world $)

The $v statement declares a variable:

$v p $.

It starts with the keyword $v, followed by variables and ends with the $. keyword.

You can declare more than one variable by separating them by spaces:

$v p q $.

You can define a constants too, also separated by spaces, by using the $c statement:

While metamath calls these "constants", I think these are more easily understood as "tokens". I'm going to use "constants" for consistency, but these are used to define lexical tokens, as you can see from the choices and examples below.

$c ~ => ( ) $.

You can specify types for variables with the $f statement:

wp $f wff p $.

This says: q is a variable of type wff, and we refer to this statement by the label wp.

You can assert that q is also a wff:

wq $f wff q $.

You can define syntactically valid strings by using the $a statement:

We'll see later that the $a statement is going to be used for three different purposes: (a) specifying syntactically valid strings of symbols, (b) specifying mathematical axioms and (c) specifying definitions (e.g. what "2" refers to). Metamath defines the $j comment to give verifiers the ability to distinguish them to make programs more readable, but the verification algorithm doesn't know the difference between the uses of axioms.

wn $a wff ~ p $.

This says: if p is a wff, then the sequence of characters of ~ followed by p is a wff, and we call this axiom wn.

p must have been declared as a variable before with a $v statement, as well as its type too with a $f statement, which is how we enforce that p needs to be of a specific type.

Here is another example of another syntactical expansion / contraction expressed as an axiom:

wi $a wff ( p => q ) $.

This says: if p and q are wffs then so is (, p, =>, q, ).

This now gives us the pre-requisites to write our first theorem, its proof and how verification works:

t1 $p wff ~ q $= wq wn $.

This says: the string ~ followed by q is a wff, we call this theorem t1 and you can verify that this is the case by using the proof wq wn.

You verify a proof by following the steps provided: wq then wn.

The verification of the proof follows a reverse polish notation and can be computed with a stack. We start with an empty stack:

Each step must be a label that was declared before.

By convention, when processing a $f label, we push the variable type and name to the stack.

That happens to be the first step wq of our proof, so our stack looks like:

When we run into a $a label, which happens to be our next step wn, we start by computing what its signature looks like.

wn $a wff ~ p $.

We can compute how many variables the axiom takes by looping through the tokens in the axiom. In the case of wn that we are processing, ~ and p, and ~ was previously declared as a constant and p as a variable, so, 1.

For every variable found in the axiom, we:

  1. pop an entry out of the stack and
  2. check if the types match and, if so,
  3. assign the variable to the entry we poped

Once we loop through every step, we:

  1. Assert that the stack has only a single entry and
  2. The entry typographically matches the theorem.

If so, we add the theorem to our program too:

Ok, so far, what we have proved that ~ q is a wff: a valid sequence of characters that can be constructed mechanically from the rules we set so far.

Let's now start to prove mathematical theorems.

Before I do, there are a couple more constructions in metamath that I need to introduce:

  1. blocks and
  2. logical hypothesis

A block is a scoping mechanism: it allows you to create a new scope that inherits statements from its parent scope but also allow you to make new statements that are only locally available.

Blocks are somewhat analogous to what we see in programming languages and { and } keywords.

${
  $( a block ! $)
  $( it sets a new scope for statements $)
$}

Logical hypothesis allows you to state a logical assumption:

min $e |- p $.

This says: let's assume that the sequence p is of type |-, and we'll call that assumption min.

Sequences can be longer, here is an example:

maj $e |- ( p => q ) $.

This says: let's assume that the sequence (, p, =>, q followed by ) is of type |-, and we'll call that assumption maj.

Now, at this point, I was asking myself "what's up with the |- type? what's that?". IIUC, this is a construction "on top of metamath" rather built "into" metamath. That is, we picked a convention, which is to say wff is a type which refers to syntactically well formed formulas, and |- is a type which refers to statements that are mathematically entailed. Metamath has no idea what "wff" is and what "|-" is, it is entirely defined in userland.

Ok, now that we have introduced both blocks and logical hypothesis, lets make our first mathematical proof.

As with syntax, we start from axioms. Lets start with one of the axioms of propositional logic: modus ponens.

${
  min $e |- p $.
  maj $e |- ( p => q ) $.
  ax-mp $a |- q $.
$}

This $a axiom says:

  1. Assuming
    • p and q are variables (based on the prior $v statement)
    • p and q are wff (based on the prior wp and wq $f statements) and that
    • p is entailed |- (based on the min $e statement) and
    • (, p, =>, q, ) is entailed (based on the maj $e statement),
  2. q is entailed |- and
  3. We call this ax-mp.

This is taken axiomatically, with no further explanation needed: if the assumptions fit, the axiom holds.

Theorems, as opposed to axioms, need proof.

${
  mp2.1 $e |- p $.
  mp2.2 $e |- q $.
  mp2.3 $e |- ( p => ( q => r ) ) $.
  mp2 $p |- r $=
      wq wr mp2.2 wp wq wr wi mp2.1 mp2.3 ax-mp ax-mp $.
$}

This $p theorem says:

  1. Assuming
    • p, q and r are wff variables
    • mp2.1: p is entailed |-
    • mp2.2: q is entailed |-
    • mp2.3: ( p => ( q => r ) ) is entailed |-
  2. r is entailed |-
  3. The proof is wq wr mp2.2 wp wq wr wi mp2.1 mp2.3 ax-mp ax-mp.
  4. We call this mp2

We verify the proof the same way we verified it before, by going the steps one by one:

wq is a $f statement, so we push q to the stack:

wr is also $f statement, so we push r to the stack:

mp2.2 is a logical assumption $e statement, so we push it to the stack:

wp, wq and wr are $f statements, so we push them to the stack:

We then process wi, which is an $a statement, more specifically, a syntactical construction statement that says: if p and q are wffs, then so is ( p => q ).

wi $a wff ( p => q ) $.

mp2.1 and mp2.3 are $e statement, so we push them to the stack:

We then process ax-mp, which is an $a statement, more specifically, a mathematical axiom that says: if p and p => q are entailed |-, then so is q.

${
  min $e |- p $.
  maj $e |- ( p => q ) $.
  ax-mp $a |- q $.
$}

Which now leaves us with:

And then, as we apply our last step, ax-mp:

Which completes executing the steps of our proof with:

Like I said before, after we verify all of the steps we take the theorem:

${
  mp2.1 $e |- p $.
  mp2.2 $e |- q $.
  mp2.3 $e |- ( p => ( q => r ) ) $.
  mp2 $p |- r $=
      wq wr mp2.2 wp wq wr wi mp2.1 mp2.3 ax-mp ax-mp $.
$}

And do two more things:

  1. We verify the stack has just a single entry (check)
  2. We pop the entry from the stack and verify that it matches the type (check) and the theorem (check)

After verifying, we add the proved theorem to our theorems list:

Hofstadter uses the term "Typographical" to refer to his MIU system, which leads to a mechanical account of number theory.