Metamath

Metamath

Developer(s)	Norman Megill
Repository	github.com/metamath/metamath-exe
Operating system	Linux, Windows, Mac OS
Type	Computer-assisted proof checking
License	Mainly GNU General Public License for the softwares and Creative Commons Public Domain Dedication for the databases
Website	http://www.metamath.org

Metamath is a computer-assisted proof checker. It 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.

Metamath has been used to develop set.mm, a human-readable database containing about 8000 (as of March 2008) fully formal proofs of mathematical theorems build over ZFC theory. Those proofs are browsable on the internet using an interface called Metamath Proof Explorer (see below Methamath Proof Explorer section). New theorems are added to set.mm daily; a table of the most recent proofs is maintained. Contributions are welcome. Help and information can be received either by asking Megill himself or by consulting a wiki, where some FAQs are located.

A formal system deduction checker

Even if Metamath is used for mathematical proof checking, its algorithm is so general we can extend (with few difficulties) the field of its usage. In fact Metamath could be used with every sort of formal systems: the checking of a computer program could be considered (even if Metamath's Jansenism would make it difficult practically speaking ); we could even use it as a syntactic checker for a natural language.

Pros and cons of Metamath's philosophy

Metamath's simplicity philosophy has good and bad consequences. Unlike systems similar to Mizar, which tend to imitate the informal proofs normally used by mathematicians by automating (and hiding) the most technical parts (at the cost of a very complex algorithm machinery), proofs developed using Metamath are fully detailed; this is advantageous because every step can be verified by the reader even if the mathematical field the theorem belongs to is not known to him (though actual development of theorems and proofs normally requires some knowledge of the related subject). On the other hand resulting proofs are much longer — a proof that would only take two or three lines in a textbook might need hundreds of steps in Metamath (most of those steps being propositional or predicate calculus inferences, which are shown in Metamath and normally not mentioned in an informal proof); in this respect Mizar is obviously more compact than Metamath.

A generic proof checker

A step-by-step proof.

Given a set of axioms and definitions, Metamath supports the verification of mathematical theorems through the exclusive use of substitution (with optional provisos for what variables must remain distinct after a substitution is made).

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 $(CFA)=(CFB)$. 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 $(CFA)=(CFB)$ 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$. So Metamath substitutes $A$ by $2$ and $B$ by $(1+1)$ and thus generates step 1. 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. So the verification is finished and the proof is 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 description in the paragraph above.

The above explanation lets suppose that formulas are stored by Metamath. In fact nothing of that sort exists. Metamath only stores the conclusion, the premises and the list of used theorems but since, with the unifying algorithm, it is possible, for the intermediate steps, to generate the conclusion from the premises nothing more is required.

Because Metamath has a very generic concept of what a proof is (namely a tree of formulas connected by inference rules) and that 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 uses other things 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 sequents) so that Metamath's requirements are met.

The Metamath language

The Metamath language is based on a very small number of tokens. There are two tokens to declare the symbols of the logic: one to declare the constants ($c) and one to declare the variables ($v). Syntactic rules and axioms are declared using the $a token, and inference rules are declared using the $a for the conclusion and the $e for the premises. Finally, $p is used to declare a theorem and its proof.

Metamath tokens carefully follow the definition of a formal system. Typically a formal system is a quadruplet $(S,F,A,I)$ where $S$ is a finite set of symbols, $F$ a set of formulas ( syntactic rules allow to decide if a string of symbols is a formula or not ), $A$ a set of axioms, $I$ a set of inference rules.

It is pretty straightforward to connect the tokens of Metamath with the abstract definition of a formal system. The finite set of symbols $S$ is declared using the $c and the $v tokens. The syntactic rules (used to define the set $F$ of formulas), the set $A$ of axioms and the set $I$ of inference rules are declared using the $a token.

We can notice that in Metamath syntactic rules, axioms and inference rules use the same token (namely the $a token). This feature is not obvious if one refers to the definition of a formal system above since this definition uses three different sets ($F$, $A$, $I$) . This at least shows that in Metamath there is no essential separation between the syntactical analysis and the properly logic treatment nor any separation between axioms and inference rules. This economical point of view is in many ways proper to Metamath where things that are often thought (perhaps too strongly) as being different are in fact confused (this tendency can be met in other places: for instance see below the remark definitions) .

Further remarks

Definitions

In Metamath a definition is an axiom, and the $a token is used to declare a definition as it is used to declare an axiom. The only difference lies in the fact that in definitions the definiendum may be replaced (and thus eliminated) by the definiens. For instance A =/= B is defined by ( A =/= B <-> -. A = B ) (-. meaning "not"). So if we consider the theorem |- A =/= { A } and if we replace the definiendum =/= by the definiens ( -. A = B we get -. A = { A }. Then we can continue (replacing { A } by its definition) until there are only primitives symbols (i.e. equality, belonging to relation, quantifiers and individual variables. The symbol used by Metamath to link definiens and definiendum is the equivalence operator. Specific operators are frequently used in textbooks to express definitions (such as a biimplication sign with a small "def" above the arrow) but the equivalence operator is appropriate and it also allows to use the normal propositional calculus to manage the formulas (a specific operator wouldn't be as economical).

Theorems and proof

A proof is associated with a theorem using the $p token. In theoretical logic, a proof is a list of formulas — each of which are either axioms or the consequences of the application of an inference rule to previous formulas in the list. Metamath allows the use of other theorems that have already been proved and supports the use of hypotheses (using the $e statement). Only the names (not the effective formulas) of the used theorems and axioms are stored in a Metamath proof.

Type of variables

In Metamath variables are typed with the $f statement. In set.mm, for instance, there are only three types: propositional, individual and class variables.

Schemes

Whereas a formal description of logic uses formulas with actual variables, Metamath uses schemes. The variables of Metamath's theorem schemes are generic variables, and any appropriate substitution can be made for them.

Symbols

since Metamath database are intended to be human-readable, Metamath uses ASCII to denote mathematical symbols. In set.mm the notation is occasionally different from standard. For example, [ y / x ] ph might denote the formula that corresponds to ph when x has been properly substituted by y (and which is usually written $\varphi (y)$ in a mathematics textbook), and ( F ` B ) might denote the value taken by the function F when applied to B (it would be coded $F(B)$ in a textbook).

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.

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
URL	us.metamath.org/mpegif/mmset.html
Commercial	No
Registration	No

Whereas one of the seminal ideas that leaded 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 maintaining for more than ten 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.

Norman Megill, building on Tarski, designed the background first order logic to facilitate checking proofs by computer. Megill is also the principle designer of Metamath's computer proof checking and database structure, and chose the nonlogical part of Metamath, set and set membership taken as primitive and governed by the ZFC axioms. Thanks to an improved understanding of the concept of proof, and nonlogical axioms derived from present-day canonical axiomatic set theory, Metamath's ultimate objective can be seen as "Principia Mathematica done right."

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.

We can also found some theorems of algebra concerning group (mathematics)s, rings, vector spaces and Hilbert spaces.

set.mm is available on the internet. The Metamath Proof Explorer includes a set of HTML pages that present the proofs of set.mm in a human-friendly way.

A table of contents at the top of the Proof Explorer gives a comprehensive list of all of the covered topics.

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 had been developed by adding extra-axioms to the standard ZFC axioms of set.mm. This adding (justified by historical opportunity reasons) is theoretically useless since the concept of Hilbert space can be designed with the standard ZFC axioms. However since ZFC in that case is weakened, the resulting proofs are shown in a different Explorer than the Metamath Proof Explorer.

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.

Annexe 1: 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 disambiguate confusing textbook definitions.

Megill gives a list of text books that can be used with Metamath and many theorems in the database reference them. People who want to learn mathematics for themselves can thus use Metamath in connection with these books.

Annexe 2: Other works connected to Metamath

Proof checkers

Using the design ideas implemented in Metamath, Raph Levien has realized what might be the smallest proof checker in the world, 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 realize a system where several people could collaborate together 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 realized for a broad variety of languages. Juha Arpiainen has realized 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 ( which is not the case of 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.

Databases

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 yet another database based on the formal system MIU presented in Gödel, Escher, Bach. Raph Levien has also designed several databases for his Ghilbert program.