# Metamath

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 `wff`s 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 `wff`s, 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.