Metamath

From Wikipedia, the free encyclopedia

Metamath

Developer(s)	Norman Megill
Written in	ANSI C
Operating system	Linux, Windows, macOS
Type	Computer-assisted proof checking
License	GNU General Public License (Creative Commons Public Domain Dedication for databases)
Website	http://metamath.org

Metamath is a language for developing strictly formalized mathematical definitions and proofs accompanied by a proof checker for this language and a growing database of thousands of proved theorems covering conventional results in logic, set theory, number theory, group theory, algebra, analysis, and topology, as well as topics in Hilbert spaces and quantum logic.

The Metamath language

While the large database of proved theorems follows conventional ZFC set theory, the Metamath language is a metalanguage, suitable for developing a wide variety of formal systems.

The set of symbols that can be used for constructing formulas is declared using $c and $v statements; for example:

$( Declare the constant symbols we will use $)
    $c 0 + = -> ( ) term wff |- $.
$( Declare the metavariables we will use $)
    $v t r s P Q $.

The grammar for formulas is specified using a combination of $f and $a statements; for example:

$( Specify properties of the metavariables $)
    tt $f term t $.
    tr $f term r $.
    ts $f term s $.
    wp $f wff P $.
    wq $f wff Q $.
$( Define "wff" (part 1) $)
    weq $a wff t = r $.
$( Define "wff" (part 2) $)
    wim $a wff ( P -> Q ) $.

Axioms and rules of inference are specified with $a statements along with ${ and $} for block scoping; for example:

$( State axiom a1 $)
    a1 $a |- ( t = r -> ( t = s -> r = s ) ) $.
$( State axiom a2 $)
    a2 $a |- ( t + 0 ) = t $.
    ${
       min $e |- P $.
       maj $e |- ( P -> Q ) $.
$( Define the modus ponens inference rule $)
       mp  $a |- Q $.
    $}

The metamath program can convert statements to more conventional TeX notation; for example, the modus ponens axiom from set.mm:

${\displaystyle \vdash \varphi \quad \&\quad \vdash (\varphi \rightarrow \psi )\quad \Rightarrow \quad \vdash \psi }$

Using one construct, $a statements, to capture syntactic rules, axiom schemas, and rules of inference provides a level of flexibility similar to higher order logical frameworks without a dependency on a complex type system.

Theorems (and derived rules of inference) are written with $p statements; for example:

$( Prove a theorem $)
    th1 $p |- t = t $=
  $( Here is its proof: $)
       tt tze tpl tt weq tt tt weq tt a2 tt tze tpl
       tt weq tt tze tpl tt weq tt tt weq wim tt a2
       tt tze tpl tt tt a1 mp mp
     $.

Note the inclusion of the proof in the $p statement. It abbreviates the following detailed proof:

tt            $f term t

tze           $a term 0

1,2 tpl       $a term ( t + 0 )

3,1 weq       $a wff ( t + 0 ) = t

1,1 weq       $a wff t = t

1 a2          $a |- ( t + 0 ) = t

1,2 tpl       $a term ( t + 0 )

7,1 weq       $a wff ( t + 0 ) = t

1,2 tpl       $a term ( t + 0 )

9,1 weq       $a wff ( t + 0 ) = t

1,1 weq       $a wff t = t

10,11 wim     $a wff ( ( t + 0 ) = t -> t = t )

1 a2          $a |- ( t + 0 ) = t

1,2 tpl       $a term ( t + 0 )

14,1,1 a1     $a |- ( ( t + 0 ) = t -> ( ( t + 0 ) = t -> t = t ) )

8,12,13,15 mp $a |- ( ( t + 0 ) = t -> t = t )

4,5,6,16 mp   $a |- t = t

The "essential" form of the proof elides syntactic details, leaving a more conventional presentation:

a2             $a |- ( t + 0 ) = t

a2             $a |- ( t + 0 ) = t

a1             $a |- ( ( t + 0 ) = t -> ( ( t + 0 ) = t -> t = t ) )

2,3 mp         $a |- ( ( t + 0 ) = t -> t = t )

1,4 mp         $a |- t = t

A generic proof checker

Metamath has no specific logic embedded and can simply be regarded as a device to apply inference rules to formulas. Simplicity is the master concept in the design of Metamath: the language of Metamath, employed to state the definitions, axioms, inference rules and theorems is only composed of a handful of keywords, and all the proofs are checked using one simple algorithm based on the substitution of variables (with optional provisos for what variables must remain distinct after a substitution is made). This "substitution" is just the simple replacement of a variable with an expression and not the proper substitution described in works on predicate calculus.

Even if Metamath is used for mathematical proof checking, its algorithm is so general we can extend the field of its usage. In fact Metamath could be used with every sort of formal system: the checking of a computer program could be considered (even if Metamath's low level would make it difficult); it could possibly even be a syntactic checker for a natural language (same remark). Because Metamath has a very generic concept of what a proof is (namely a tree of formulas connected by inference rules) and no specific logic is embedded in the software, Metamath can be used with species of logic as different as Hilbert-style logics or sequents-based logics or even with lambda calculus. In contrast, it is largely incompatible with logical systems which use other things rather than formulas and inference rules. The original natural deduction system (due to Gerhard Gentzen), which uses an extra stack, is an example of a system that cannot be implemented with Metamath. In the case of natural deduction however it is possible to append the stack to the formulas (transforming the natural deduction formulas into a sort of sequent) so that Metamath's requirements are met.

What makes Metamath so generic is its substitution algorithm. This algorithm makes no assumption about the used logic and only checks the substitutions of variables are correctly done.

A step-by-step proof

So here is a detailed example of how this algorithm works. Steps 1 and 2 of the theorem 2p2e4 in set.mm are depicted left. Let's explain how Metamath uses its substitution algorithm to check that step 2 is the logical consequence of step 1 when you use the theorem opreq2i. Step 2 states that ( 2 + 2 ) = ( 2 + ( 1 + 1 ) ). It is the conclusion of the theorem opreq2i. The theorem opreq2i states that if A = B, then (C F A) = (C F B). This theorem would never appear under this cryptic form in a textbook but its literate formulation is banal: when two quantities are equal, one can replace one by the other in an operation. To check the proof Metamath attempts to unify (C F A) = (C F B) with ( 2 + 2 ) = ( 2 + ( 1 + 1 ) ). There is only one way to do so: unifying C with 2, F with +, A with 2 and B with ( 1 + 1 ). So now Metamath uses the premise of opreq2i. This premise states that A = B. As a consequence of its previous computation, Metamath knows that A should be substituted by 2 and B by ( 1 + 1 ). The premise A = B becomes 2=( 1 + 1 ) and thus step 1 is therefore generated. In its turn step 1 is unified with df-2. df-2 is the definition of the number 2 and states that 2 = ( 1 + 1 ). Here the unification is simply a matter of constants and is straightforward (no problem of variables to substitute). So the verification is finished and these two steps of the proof of 2p2e4 are correct.

There is however some complications that are not shown on the picture. When Metamath unifies ( 2 + 2 ) with B it has to check that the syntactical rules are respected. In fact B has the type class thus Metamath has to check that ( 2 + 2 ) is also typed class This is done using the same sort of unification described in the paragraph above.

The above explanation may let suppose that formulas are stored by Metamath. In fact nothing of that sort exists. Metamath only stores the conclusion and the premises of the proven theorem and the list of the names of the theorems used by the proof and nothing more. But since it is possible, with the substitution algorithm, to generate the conclusion from the premises nothing more is required.

Databases

Metamath comes along with two main databases set.mm and ql.mm. set.mm stores theorems concerning ZFC theory and ql.mm develops a set of quantum logic theorems. Three internet interfaces (the Metamath Proof Explorer, the Hilbert Space Explorer and the Quantum Logic Explorer) are provided to explore these two databases in a human friendly way.

set.mm is by far the biggest database written for Metamath, but there is also a formalization (by Robert Solovay) of Peano arithmetic called peano.mm (included in metamath.zip) and a formalization of natural deduction called nat.mm. There is a database based on the formal system MIU presented in Gödel, Escher, Bach. Raph Levien has also designed several databases for his Ghilbert program.

Metamath Proof Explorer

Metamath Proof Explorer

A proof of the Metamath Proof Explorer
Type of site	Internet encyclopedia project
Headquarters	USA
Owner	Norman Megill
Created by	Norman Megill
Website	us.metamath.org/mpegif/mmset.html
Alexa rank	2,281,276 (April 2014)
Commercial	No
Registration	No

Metamath has been used to develop set.mm, a human-readable database containing over 30,000 (As of March 2017) fully formal proofs of mathematical theorems built upon ZFC set theory. Those proofs may be browsed on the internet using an interface called Metamath Proof Explorer. New theorems are added to set.mm daily; a table of the most recent proofs is maintained.

One of the seminal ideas that lead Megill to design Metamath was the desire to precisely determine the correctness of some proofs ("I enjoy abstract mathematics, but I sometimes get lost in a barrage of definitions and start to lose confidence that my proofs are correct."), we can also think that the spirit of the Encyclopedia animates the growing up of Metamath and its most important database (called set.mm). Reading set.mm we may have sometimes the impression that the ambition of its author is essentially to add all the mathematics one theorem after the other.

set.mm has been maintained for twenty years now (the first proofs in set.mm are dated August 1993). It is mainly a work by Norman Megill but there are also proofs made by other participants. Technically speaking set.mm develops—in the Hilbert style—ZFC set theory with the addition of the Grothendieck-Tarski axiom (to manage categories). The underlying logic is classical propositional calculus and classical predicate calculus with equality.

set.mm is a valuable tool to understand how well-known set theory concepts such as classes, power sets, union, relations, functions, equivalence classes and so on are derived from the axioms.

However set.mm doesn't stop at these basic notions but explores more elaborated theories.

Cantor concepts such as ordinal and cardinal numbers, equinumerosity or aleph function are defined.
Integers and natural numbers are constructed along with traditional arithmetic tools such as operations, recursion or induction.

The real and complex numbers are constructed from Dedekind cuts, and the concepts of sequence, limit of a sequence, sum of a series and so on are developed for them. The concept of integral is still missing.

Square root, exponentiation, exponential and trigonometric functions are implemented.
General topology is currently developed: topological spaces, closed and open sets, neighborhood, limit point, continuous function, Hausdorff spaces, metric spaces, Cauchy sequences have been defined.

One can also find some theorems of algebra concerning groups, rings, vector spaces, and Hilbert spaces.

Hilbert Space Explorer

The Hilbert Space Explorer presents more than 1,000 theorems pertaining to the Hilbert space theory. Those theorems are included in set.mm. They are not shown in the Metamath Proof Explorer because they have been developed by adding extra axioms to the standard axioms of set.mm. ZFC is weakened by this adding which explains why the resulting proofs are shown in a separate Explorer. This adding (justified by historical opportunity reasons) is theoretically useless since the concept of Hilbert space can be designed with the standard ZFC axioms.

Quantum Logic Explorer

Quantum logic theorems can be found in the database ql.mm. The Quantum Logic Explorer is an internet interface to this database.

Pedagogy

The method of proof used by Metamath is far different from what is used in a school context. In schools what is required is the literate, synthetic method of proof developed by mathematicians since Euclid's time. In Metamath, the method of proof is the symbolic, analytical method of proof invented by Aristotle, Leibniz, Peano, and Frege. Thus, Metamath is unsuitable for school exercises. To speak simply, the proofs in Metamath are much too detailed to be used with ease in school. However, set.mm can be used in a school context as an example of a symbolic system that is big enough to be interesting. set.mm can also be useful because its detailed, symbolic, unambiguous definitions can resolve confusion with textbook definitions. Students may also appreciate the rigor of the Metamath Proof Explorer; no steps are skipped, no assumption left unstated, and no proofs are left "to the reader".

The Proof Explorer references many text books that can be used in conjunction with Metamath. Thus, people interested in studying mathematics can use Metamath in connection with these books.

Other works connected to Metamath

Proof checkers

Using the design ideas implemented in Metamath, Raph Levien has implemented very small proof checker, mmverify.py, at only 500 lines of Python code.

Ghilbert is a similar though more elaborate language based on mmverify.py. Levien would like to implement a system where several people could collaborate and his work is emphasizing modularity and connection between small theories.

Using Levien seminal works, many other implementations of the Metamath design principles have been implemented for a broad variety of languages. Juha Arpiainen has implemented his own proof checker in Common Lisp called Bourbaki and Marnix Klooster has coded a proof checker in Haskell called Hmm.

Although they all use the overall Metamath approach to formal system checker coding, they also implement new concepts of their own.

Editors

Mel O'Cat designed a system called Mmj2, which provides a graphic user interface for proof entry. The initial aim of Mel O'Cat was to allow the user to enter the proofs by simply typing the formulas and letting Mmj2 find the appropriate inference rules to connect them. In Metamath on the contrary you may only enter the theorems names. You may not enter the formulas directly. Mmj2 has also the possibility to enter the proof forward or backward (Metamath only allows to enter proof backward). Moreover Mmj2 has a real grammar parser (unlike Metamath). This technical difference brings more comfort to the user. In particular Metamath sometimes hesitates between several formulas analyzes (most of them being meaningless) and asks the user to choose. In Mmj2 this limitation no longer exists.

There is also a project by William Hale to add a graphical user interface to Metamath called Mmide. Paul Chapman in its turn is working on a new proof browser, which has highlighting that allows you to see the referenced theorem before and after the substitution was made.