Metamath

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 $c token.
To define variables, use the $v token.
To define types of variables, use the $f token.
To define essential hypothesis, use the $e token.
To define axioms, use the $a token.
To define proofs, use the $p token.
To start proving in $p statement, 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 $a and $p tokens 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 $e or a $f statement
For every variable in $e, $a or $p, we must have a $p assertion, i.e. every variable in an essential hypothesis/axiom/proof must have a floating hypothesis (type)
A $f, $e, or $d statement is active from the place it occurs until the end of the block it occurs in. A $a or $p statement 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.

Calculus of Constructions

As an additional extension to the hierarchy of logical systems we’ve discussed, we’ll consider type theory. In type theory, every “term” has a “type” and operations are restricted to terms of a certain type.

Type theory was created to avoid paradoxes in a variety of formal logics and rewrite systems. For example, Russell’s paradox is not applicable since every sentence has its own type.

The most powerful concept in Coq is not about Coq; it’s the calculus of constructions. Coq is just a lot of awesome automation machinery on top of that.

Calculus of Constructions is a type theory based on intuitionistic logic and simply typed lambda calculus. Together with Dependent Types, Inductive Types, Recursion, they provide a neat way to do proofs.

To demonstrate why they are powerful, let’s consider one of the inference rules as an example:
${\Gamma ,x:A\vdash B:K\qquad \qquad \Gamma ,x:A\vdash N:B \over {\Gamma \vdash (\lambda x:A.N):(\forall x:A.B):K}}$

What this means is that if above the line holds, then so does everything below the line.

In this case, K is either a Prop or a Type. For simplicity, assume K is Type. To translate it, it means that:
1. If we have a judgment x of type A, from which it follows that B : K (B is a Type)
and
2. If we have a judgment x of type A, from which it follows that N : B (N has type of B)
then we can deduce that
(\x : A . N) has type (\forall (x : A) . B), and the term (\forall (x : A) . B) has type Type.

In other words, this is the rule that ties together lambda abstraction and universal quantification. It also says that a universal quantification is a type.

This rule is the reason why this flows nicely:

(* Make sure you have enabled "Display all basic low-level contents" *)
Definition test (s : Set) : bool := true.

Check test.                 (* test : forall _ : Set, bool *)

Check forall _ : Set, bool. (* forall _ : Set, bool : Type *)

Other data types are encoded similarly as with Church Numerals.

The interesting thing about this system is that it has the strong normalization property, which means that every sequence of rewrites eventually terminates.

While this is not useful for IO, it is very useful for proofs.

In any case, we can take advantage of IO by extracting code to other languages as seen in Coq to Haskell.

Coq to Haskell

Lately I spent some time learning Coq. It is a very useful programming language, but guess what? It has no IO!

So, once we prove our theorems, what do we do? We extract our code!

Let’s pick a language that has IO, for example Haskell.

For fun, let’s try to prove the following and extract the definitions to Haskell:
The sum of a list containing natural numbers is always greater than or equal to 0.

But, in order to prove this, we must define everything on a core level, that is:
1. We need to define what a list is
2. We need to define what a natural number is

We can, but we won’t do that since they are already defined in Coq itself. So we’ll just go ahead and use “list” and “nat” in our code.

Here’s the definition of our recursive function that will calculate the sum of all the elements in a list of natural numbers:

Fixpoint my_sum (l : list nat) : nat :=
  match l with
  | nil     => 0
  | x :: l' => x + my_sum l'
  end.

It’s a pretty straight-forward definition. Let’s write some examples:

Example my_sum1 : my_sum [1 ; 2 ; 3] = 6.
Proof.
  simpl. reflexivity.
Qed.

Example my_sum2 : my_sum [] = 0.
Proof.
  simpl. reflexivity.
Qed.

Example my_sum3 : my_sum [1] = 1.
Proof.
  simpl. reflexivity.
Qed.

And now, for the proof of our theorem:

(* Sum of a list of naturals will always produce a result greater than or equal to 0 *)
Theorem my_sum_nat_gt_0 : forall l : list nat, 0 <= my_sum l.
Proof.
  intros l.
  induction l.
  - (* base *) simpl. reflexivity.
  - (* i.h. *) simpl. case a.
    + (* zero *) simpl. exact IHl.
    + (* S n  *) intros n. rewrite IHl. exact (Plus.le_plus_r (S n) (my_sum l)).
Qed.

Cool! Now for the final part, which is the extraction:

Require Extraction.
Extraction Language Haskell.
Recursive Extraction my_sum.

And finally, our Haskell code generated by the commands above:

data Nat =
   O
 | S Nat

data List a =
   Nil
 | Cons a (List a)

add :: Nat -> Nat -> Nat
add n m =
  case n of {
   O -> m;
   S p -> S (add p m)}

my_sum :: (List Nat) -> Nat
my_sum l =
  case l of {
   Nil -> O;
   Cons x l' -> add x (my_sum l')}

We can now use our function my_sum for which we know our theorem to be true, and we can use it in a programming language that supports IO.

Pretty cool stuff, right? 🙂

Bonus: You can’t do these kind of proofs in Haskell itself, since it has no support for dependent types (we’ll cover that in a future post).

MU puzzle

The MU puzzle is an example of a Formal system we will take a look at, as described by Douglas Hofstadter in his book Gödel, Escher, Bach.

We’re given a starting string MI, and some transformation rules.

Here are the transformation rules:

Nr.	Formal rule			Informal explanation	Example
1.	x`I`	→	x`IU`	Add a `U` to the end of any string ending in `I`	`MI`	to	`MIU`
2.	`M`x	→	`M`xx	Double the string after the `M`	`MIU`	to	`MIUIU`
3.	x`III`y	→	x`U`y	Replace any `III` with a `U`	`MUIIIU`	to	`MUUU`
4.	x`UU`y	→	xy	Remove any `UU`	`MUUU`	to	`MU`

Here is an example usage to derive MIIU from MII for some of the transformation rules:

MI (an axiom)
MII (by rule 2)
MIIII (by rule 2)
MIIIIIIII (by rule 2)
MUIIIII (by rule 3)
MUUII (by rule 3)
MII (by rule 4)
MIIU (by rule 1)

More formally, we can represent the MU puzzle as follows:

Language
1. The set of symbols is { M, I, U }.
2. A string is a grammatical sentence (wff) if its first word is M, and no other words are Ms. E.g.: The following strings are grammatical sentences: M, MIUIU, MUUUIII.
MI is the starting string, thus an axiom.
The inference rules are the transformation rules we’ve just defined above.

The question now is, can we convert MI to MU using the transformation rules?

In order to answer this, we will use invariant (a property that holds true whenever we apply some of the rules) with induction to prove our claim.

What would be a good invariant here?

Let’s suppose we can somehow get to MUIIIU. Now, if we apply rule 3 to it, we get MUUU. Apply rule 4, and pure win!

Note that, in order to be able to apply rule 3, we need to have the number of subsequent I’s to be divisible by 3. So let’s have our invariant say that “There are no subsequent I’s in the string that are divisible by 3”.

1. For the starting axiom, we have one I. Invariant OK.
2. Applying rule 2 will be doubling the number of I’s, so we can have: I, II, IIII, IIIIIII (in particular, 2^n I’s). Invariant OK.
3. Applying rule 3 will be reducing the number of I’s by 3. But note that 2^n – 3 is still not divisible by 3. Invariant OK.

So we’ve shown that with the starting axiom MI it is not possible to get to MU. But, what if we have a different starting axiom? Or even, different rules? 🙂

But if we look carefully, we’ve used a different formal system to reason about MU (i.e. divisibility by 3). This is because the puzzle cannot be solved in its own system. Otherwise, an algorithm would keep trying different inference rules of MU indifinitely (not knowing that MU is impossible).

In general, for any formal system there’s this limitation. Gödel’s theorem shows that there’s no formal system that can contain all possible truths, because it cannot prove some truths about its own structure.

So, having experience with different formal systems and combining them as needed can be useful 🙂

Formal systems

This post is a generalization to one of my previous posts, Hierarchy of logical systems.

Wikipedia states the following definition of a formal system:

A formal system is any well-defined system of abstract thought based on the model of mathematics

More formally, a formal system is consisted of:

A formal language, i.e.
1. A finite set of symbols, that can be used for constructing formulas (i.e. finite strings of symbols).
2. A grammar, which tells how well-formed formulas (abbreviated wff) are constructed out of the symbols.
A set of axioms.
A set of inference rules.

Once we defined a formal system, other systems can extend it.

For example, the ZFC set theory is based on first-order logic, which itself is based on propositional logic which is a formal system.

In general, we often put our focus on which parts of mathematics can be formalized in particular formal systems, rather than trying to find a theory in which all of mathematics can be developed, for the reason below.

Gödel’s incompleteness theorem states that there doesn’t exist* a formal system that is both complete and consistent.

Note that the statement above is about systems that allow expressing arithmetic of natural numbers (e.g. Peano, ZFC, but first-order logic also has some paradoxes if we allow self-referential statements).

In other words, for every such formal system, we will have either:

There will be statements that are true in that system, but which cannot be proved to be true inside the system (incomplete).

A quick example is the statement “This statement is not provable”.
The statement can either be true or false:
True: It is not provable.
False: It is provable, but we’re trying to prove something false.
Thus the system is incomplete, because some truths are unprovable.
There will be a theorem in the system that is contradictory (inconsistent).

We can start with the following statement: “This statement is false”.

This statement is true if and only if it is false, and therefore it is neither true nor false (inconsistent).

The proof above tells us that we should keep thinking about our formal systems outside of their own definition, i.e. as the famous saying goes to think outside of the box, in order to improve our systems. Similarly to how we sometimes do meta-thinking to improve ourselves.

In conclusion, formal systems are our attempt to abstract models, whenever we reverse engineer nature in attempt to understand more. They may be imperfect, but can be very useful for our understanding.

We will look at an example of a formal system in my next post.