\( \DeclareMathOperator{\num}{number} \DeclareMathOperator{\wff}{wff} \newcommand{\ove}[2]{{\genfrac{}{}{0.5pt}{0}{#1}{#2}}} \)

\(\lambda\) Logic, Types, Functionality

To and beyond



Implementing \(\mathbb{N}_{0\leq+}\) in Metamath

Feb 26, 2019

To understand all concepts used in this text, it's recommended to read the previous article.

What is Metamath?

Metamath is a language/tool to specify formal systems in the way we talked about them, and to prove statements in those systems which then get checked by the program. Its language is extremely simple which makes proof checkers more reliable, and the command-line interface makes it somewhat comfortable to use. It also comes with an extremely (>30k proofs) large database based on set theory and classical logic. But let me provide an example now.

\(\mathbb{N}_0\)

 $c number wff = |- 0 ' $. 

This statement declares the alphabet/the constants in the system, separated by spaces and indicated by the $c . Every statement is ended by $.. We can only use declared symbols in statements for obvious reasons.

$v n m o $. 

A $v statement declares the used metavariables, which are required to express axiom schemes and most inference rules. We do not declare any properties of the variables yet; this is done by the next statement.

numn $f number n $. 
numm $f number m $.
numo $f number o $.

Those are the first named statements we encounter; they need names because they'll be used in proofs. They assign a property to a variable, such that those hypotheses are implicitly "added" to the premises. For example, we'd not need the \(\num n\) in the rule \[ \begin{gather} \num n \over 0 \leq n \end{gather} \] because it is given for the whole system. This can also transform inference rules in axiom schemes.
You could read those statements as "numn expresses that n will be used as a number."

num0 $a number 0 $.
nums $a number n ' $.

Those two statements are axioms. Once again, those have to be named. num0 just defines 0 as a number, and numS declares that for every number, its successor also is a number. As you can see, metavariables somewhat define an universal property. For every ob we will substitute the metavariable with, we'll need to prove that it indeed is a number.

wffeq $a wff n = m $.
eq0 $a |- 0 = 0 $.

These two axioms are also quite simple, but it's always a good idea just to take a look at them before you continue reading.

They state that equality is a relation such that a formula is created out of two numbers, and that it is true that \(0 = 0\). We, as readers, apply a meaning to the symbol \(\vdash\): Truth.
You might argue that \(\num\) and \(\wff\) also express some kind of truth ("it is true that 0 is a number"), but it is a different kind of truth nonetheless. It's the difference between derivability and the symbol, which defines an ob in the right of it as true, when the so created ob is derivable.

${
eqS.1 $e |- n = m $.
eqS   $a |- n ' = m ' $.
$}
	  
${
eqsymm.1 $e |- n = m $.
eqsymm   $a |- m = m $.
$}

${
eqtrans.1 $e |- n = m $.
eqtrans.2 $e |- m = o $.
eqtrans   $a |- n = o $.
$}

This code introduces two new thing: blocks, as indicated by ${ / $} and the $e statement. With those two combined, you're able to express inference rules. Put your premises as $e-statements in a block, together with an axiom as the conclusion. So the first block expresses has one premise and one conclusion: \(\vdash n = m\) makes \(\vdash n'=m'\) derivable. Also note that spaces are required between literally everything, because Metamath has no idea about parentheses, operators, etc. Now let's just take a look at how proofs work:

ex1 $p |- 0 ' ' = 0 ' ' $=
  num0 nums num0 nums num0 num0 eq0 eqS eqS $.

First of all, we have a label obviously. After the first separator, the statement which is going to be proven follows. Once again, a separator. The proof itself looks more complicated than it is, a version with rectangles might help a little bit:

Since we want to prove that \(0''=0''\), we first need a proof that \(0'=0'\), and then put the used rule next to it. The proof of \(0'=0'\) relies on a proof that \(0=0\), which is obvious. Also, since we apply a rule, we need proof that 0 and 0 are numbers. They also follow in one step. Since we now apply eqS again, we need to prove that \(0'\) and \(0'\) are numbers. This can be proven by the same method, we still need to do it twice because Metamath is - as often - too simple to care.
When printed in the interactive Metamath environment, the proof looks somewhat similar:

MM> show proof ex1 /all
1     numn=num0 $a number 0
2   numn=nums $a number 0 '
3     numn=num0 $a number 0
4   numm=nums $a number 0 '
5     numn=num0 $a number 0
6     numm=num0 $a number 0
7     eqS.1=eq0 $a |- 0 = 0
8   eqS.1=eqS $a |- 0 ' = 0 '
	    9 ex1=eqS   $a |- 0 ' ' = 0 ' '

It obviously shows a lot of information that we don't necessarily need, including all the obs involved. But for now, let's move on and extend our system.

\(\mathbb{N}_{0\leq+}\)

I'll not segment the code further since there's nothing particularly new involved, and I'd rather focus on the next proof.

$c <= + ( ) $.

leqwff $a wff n <= m $.

leq0 $a |- 0 <= n $.

${
leqS.1 $e |- n <= m $.
leqS   $a |- n ' <= m ' $.
$}

${
leqeq.1 $e |- n = o $.
leqeq.2 $e |- n <= m $.
leqeq   $a |- o <= m $.
$}

${
eqleq.1 $e |- n = o $.
eqleq.2 $e |- m <= n $.
eqleq   $a |- n <= o $.
$}

${
leqtr.1 $e |- m <= n $.
leqtr.2 $e |- n <= o $.
leqtr   $a |- m <= o $.
$}

plusnum $a number ( n + m ) $.

plus0 $a |- ( 0 + m ) = m $.

${
pluss.1 $e |- m = n ' $.
pluss   $a |- ( m + o ) = ( n + o ) ' $.
$}

1plus1 $p |- ( 0 ' + 0 ' ) = 0 ' ' $=
  num0 nums num0 nums plusnum num0 num0 nums plusnum nums num0 nums nums num0
  num0 nums num0 nums num0 num0 eq0 eqS pluss num0 num0 nums plusnum num0 nums
  num0 nums plus0 eqS eqtrans $.

So let's just take a look at the metamath output of the proof, you should be familiar enough with the system itself (You could always just open the other tab :D).

MM> show proof 1plus1 /all
 1       numn=num0       $a number 0
 2     numn=nums       $a number 0 '
 3       numn=num0       $a number 0
 4     numm=nums       $a number 0 '
 5   numn=plusnum    $a number ( 0 ' + 0 ' )
 6       numn=num0       $a number 0
 7         numn=num0       $a number 0
 8       numm=nums       $a number 0 '
 9     numn=plusnum    $a number ( 0 + 0 ' )
10   numm=nums       $a number ( 0 + 0 ' ) '
11       numn=num0       $a number 0
12     numn=nums       $a number 0 '
13   numo=nums       $a number 0 ' '
14     numn=num0       $a number 0
15       numn=num0       $a number 0
16     numm=nums       $a number 0 '
17       numn=num0       $a number 0
18     numo=nums       $a number 0 '
19       numn=num0       $a number 0
20       numm=num0       $a number 0
21       eqS.1=eq0       $a |- 0 = 0
22     pluss.1=eqS     $a |- 0 ' = 0 '
23   eqtrans.1=pluss $a |- ( 0 ' + 0 ' ) = ( 0 + 0 ' ) '
24       numn=num0       $a number 0
25         numn=num0       $a number 0
26       numm=nums       $a number 0 '
27     numn=plusnum    $a number ( 0 + 0 ' )
28       numn=num0       $a number 0
29     numm=nums       $a number 0 '
30         numn=num0       $a number 0
31       numm=nums       $a number 0 '
32     eqS.1=plus0     $a |- ( 0 + 0 ' ) = 0 '
33   eqtrans.2=eqS   $a |- ( 0 + 0 ' ) ' = 0 ' '
34 1plus1=eqtrans  $a |- ( 0 ' + 0 ' ) = 0 ' '	

We see that we prove \(1+1=2\) in three main steps:
First, we prove that \((1+1)=(0+1)'\). From this point, we derive \((0+1)'=2\) and apply transitivity. To prove the first statement, we just apply the recursive definition of \(+\) and only prove that summands stay constant. For the second proof, first, we "take one ' away", and only prove the equality of the predecessors. In that case, it's enough to apply the base case of \(+\), because the juxtaposition of apostrophes does it job.

The Interactive Environment of Metamath

Writing proofs like this is tedious. What is needed is a tool listing incomplete proofs and helping you to find the correct rules to apply, maybe even finding proofs for some thing by itself? You may not be surprised that the official implementation of metamath provides this, and even more. However, I'll explain what the perhaps easiest way to use Metamath is for such formal systems.

First of all, Metamath has to read the source file. Just use read and an unescaped path. However, if any syntactic errors occur, you first have to unload (erase) the file in the exact same way. You can also use show <labels|source|proof|statement> to show 1. all the available labels, their line number and statement type 2. the source of a given label 3. the proof of a given label 4. the statement to a label. To prove a certain statement, we first have to switch modes by using prove <label>. Now, show new_proof always shows what is proven yet and marks unknown steps/obs that replace variables with a ?. To find the appliable rules/axioms, use match all/match step n. All appliable rules get listed and you get to pick between them. When you think you're done, use improve all to improve the proof and check it. The output tells you everything you'd have to do next. Obviously, there are way, way more possibilities what to do with Metamath (we might explore some more in the future), but that's just a quick summary how I work with it.

Links: