Metamath

Metamath

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

Metamath, designed by Norman Megill, is an automated proof verifier and language for mathematical theorems. It provides support for developing theorems and axioms using a syntax based on keyword tokens. The algorithm used to check the proofs, based on the substitution of variables, is relatively general and can be used to verify many logical assertions. Unlike the proofs of systems (similar to the Mizar system) which attempt to imitate the informal proofs normally used by mathematicians, proofs developed using Metamath are normally fully detailed and resemble the proofs developed using traditional symbolic logic; this is advantageous because every step of a proof can be verified even if the mathematical field the theorem belongs to is not known to the end-user (though actual development of thereoms and proofs normally requires proficiency of the related subject). One consequence of this paradigm is that the resulting proofs are much longer — a proof that would only take two or three lines in a textbook might need tens of steps in Metamath.

Metamath includes set.mm, a textual database containing over 9,000 proofs, the content of which is available on the internet using an interface called Metamath Proof Explorer. New theorems are added to the database on a daily basis; a table of the most recent proofs is maintained by Megill.

Help and information can be received either by asking Megill himself or by consulting a wiki, where some FAQs are located.

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) with a visual description of the method of substitution used by Metamath. The theorem itself states that $(2+2)=4$ (this was proved originally by Alfred North Whitehead and Bertrand Russell in Principia Mathematica), the first step of which references df-2. This axiomatic definition states that $2=(1+1)$. It is subsequently inferred (step 2) that $(2+2)=(2+(1+1))$; this is then used as a hypothesis for opreq2i, which asserts that if we have $A=B$ as a premise, then we can infer $(CFA)=(CFB)$. Thus if $A=B$, then $(CFA)=(CFB)$. This inference is applied to $(2+2)=(2+(1+1))$, and Metamath uses substitution to associate the conclusion of opreq2i ($(CFA)=(CFB)$) with $(2+2)=(2+(1+1))$. In doing so, the class $C$ has a value of $2$, $F$ has a value of $+$, $A$ has a value of $2$ and $B$ has a value of $(1+1)$. Because $A$, $B$, and $C$ are class variables, Metamath verifies that + , 2 , (1 + 1) are classes (using its substitution algorithm) in the process of verifying the proof. In doing so, Metamath associates the premise $2=(1+1)$ with df-2. In most cases, Metamath proofs are developed working backwards in a manner similar to this.

Because Metamath has a very generic concept of what a proof is, it is not limited to a particular sort of logic; proofs are treated simply as trees of formulas connected by inference rules. The sole function of Metamath is to verify that each inference may be applied to the formulas they are associated with. Because such a system corresponds to numerous systems of logic, Metamath can be used with concepts such as Hilbert spaces and lambda calculus. In contrast, it is largely incompatible with logical systems which do not make use of formulas and inference rules. The original natural deduction system (due to Gerhard Gentzen), which uses a stack of arbitrary length, is an example of a system that cannot be used with Metamath. It is possible, however, to append the stack of conditions to the formulas, provided that the requirements of Metamath are met.

The Metamath language

The Metamath language is based on a small number of tokens which formally define a particular type of logic. There are two tokens to declare the symbols of the logic: one to declare the constants ($c) and one to declare the variables ($v). Well-formed formulas and axioms are declared using the $a token, and inference rules are declared using the $a for the conclusion and the $e for the hypothesis. Finally, $p is used to declare a proof.

Further remarks

Well formed formula and axioms

In a formal description of logic, the rules to declare the well formed formulas, the axioms and the inference rules are separated. In Metamath they are combined: all three rules use the $a markup. In a Metamath proof there is no essential separation between the syntactical analysis and the properly logic treatment.

Definitions

In Metamath a definition is an axiom, and the $a token is used to declare both. The only difference lies in the fact that in definition the definiendum can be replaced (and thus eliminated) by the definiens. The symbol used by Metamath to link definiens and definiendum is the biimplication operator. Specific operators are frequently used to express definitions; a biimplication operator allows the use of the normal propositional calculus to do this.

Theorems and proof

A proof is associated with a theorem using the $p token (which is also used to declare a theorem). 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 of the used rules are stored in the Metamath proof.

Type of variables

In Metamath variables are typed with the $f statement. In set.mm, for instance, there are 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.

ASCII symbols

Metamath uses ASCII symbols to denote mathematical concepts, and consequently its notation is occasionally different from standard notation in many ways. For example, [ x / y ] ph might denote the formula that corresponds to ph when y has been properly substituted by x, and ( F ` B ) might denote the value the function F applied to B.

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

Whereas one of the seminal ideas that leads 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 Category ). 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, powersets, 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 developped 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 groups, 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 first by adding extra-axioms to the standard ZFC axioms of set.mm. This adding 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.

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 implementation 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 entering the formulas and letting mmj2 find the appropriate inference rules to connect them.

There is also a project to add a graphical user interface to Metamath called mmide.

Paul Chapman 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.

Other databases

"set.mm" is by far the biggest database written for Metamath, but there is also a formalization (by Robert Solovay) of Peano's 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.