Metamath

From Wikipedia, the free encyclopedia

Metamath
Developer:	Norman Megill
OS:	Linux, UNIX, Cygwin, Windows, Mac OS
Use:	Computer-assisted proof checking
License:	GNU General Public License and Creative Commons Public Domain Dedication
Website:	http://www.metamath.org

Metamath Proof Explorer

A proof of the Metamath Proof Explorer
URL	http://us.metamath.org/mpegif/mmset.html
Commercial?	No
Type of site	Internet encyclopedia project
Registration	No
Owner	Norman Megill
Created by	Norman Megill

Metamath, devised by Norman Megill, is an automated proof verifier for mathematical theorems^[1]. The language used to code theorems and axioms is based on markups. And the algorithm used to check the proofs, based on substitutions of variables, is remarkably general and able to check a large set of logics. Unlike the proofs of Mizar and similar systems which try to imitate the unformal proofs normally used by mathematicians, Metamath's proofs are fully detailed and resemble the proofs developped by the symbolic logic tradition. Ironically it has even been said that Metamath's proofs resemble mathematics as it would be if passed through a dissassembler. The advantage of this approach is that every step of a proof can be checked even if you don't know the field the theorem belongs to (obviously to code the proof however this knowledge is mandatory). The disadvantage is that the resulting proofs are much longer: a proof that would only take two or three lines in a textbook can need tens of steps in Metamath.

Metamath comes along with a database of 6,000 proofs called set.mm. The content of this database is available on the internet using an interface called the Metamath Proof Explorer. New theorems are daily added to the database. A table of the most recent proofs is maintained.^[2] Help and information can be received either by asking Megill himself or by consulting a wiki where some FAQs are gathered.

Contents 1 A generic proof checker 2 The Metamath language 3 A 6,000 theorems database 4 Annexe 1: Pedagogy 5 Annexe 2: Other works connected to Metamath 6 References

[edit] A generic proof checker

Given a set of axioms and definitions, Metamath can verify proofs of mathematical theorems using only one rule, substitution (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.^[3]

Because it has a very generic concept of what a proof is, Metamath is not dedicated to a specific logic. In Metamath's view, a proof is a tree of formulas connected by inference rules. Checking that the inference rules may be applied to the formulas to which they are connected is the only work of Metamath. So any proof that can be thought as a tree of formulas linked by inference rules can be checked. Since that sort of pattern corresponds to systems as different as Gentzen-style systems of logic, Hilbert-style systems of logic or lambda calculus we can claim that Metamath is adapted to most species of logic. Some systems can't be checked by Metamath. Natural deduction systems that use arbitrary-length stacks, for example, can't. However in the case of natural deduction for instance it is possible to slightly modify the system originally devised by Gentzen in order that it fits what is required by Metamath.

[edit] The Metamath language

The Metamath language is based on a small number of markups, which follow the formal description of a logic. There are two markups to declare the symbols of the language; one to declare the constants ($c) and one to declare the variables ($v). Well-formed formulas and axioms are declared using the $a markup. Inference rules are declared using the $a markup for the conclusion and the $e markup for the hypothesis. The definition of the language stops here. In a formal description of a logic there then comes the description of what is considered as a proof. The metamath language uses the $p markup to declare a proof.

Some further remarks about the Metamath language:

1. 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.
2. Definitions: In Metamath a definition is an axiom. The same feature (the $a markup) is used for the two concepts of axiom and of definition. The only difference lies in the fact that 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. Using a simple biimplication operator allows the use of the normal propositional calculus to deal with definition.
3. On theorems and proof: In Metamath a proof is connected to a theorem and theorems are declared using the $p markup. In theoretical logic, a proof is a list of formulas, each of them being an axiom or the consequence 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 allows theorems to have hypotheses (using the $e statement). Only the names of the used rules are stored in Metamath, the exact appearance of the formulas being considered superfluous.
4. Type of variables: In metamath variables are typed with the $f statement. In a typical Metemath proof there are three types of variables: propositional variables, individual variables and class variables.
5. 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.^[4]
6. ASCII symbols: Metamath uses ASCII symbols to denote mathematical concepts. Metamath's notation is different from standard notation in many ways. For example, [ x / y ] ph denotes the formula that corresponds to ph when y has been properly substituted by x; ( F ` B ) denotes the value the function F applied to B.^[5] This notation, an invention of Quine, was chosen to avoids the ambiguity of parentheses in standard notations. The inverse of a relation, or "converse" as Megill calls it (following Quine), is denoted by a u-ish symbol above and to the left of the relation, as opposed to the -1 superscript used traditionally.^[6] As it is shown by these three examples the differences between Metamath's denotation and standard ones are always motivated by syntactical analysis problem (like ambiguities). However they can seem surprizing at first, it's not very difficult to become accustomed to them.

[edit] A 6,000 theorems database

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."^[7]), 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 can have sometimes the impression that the ambition of its author is essentially to add all the mathematics one theorem after the other.

"set.mm" contains more than 6,000 theorems, including theorems of propositional calculus, predicate calculus and ZFC set theory. A wide range of concepts are developed:

• Simple set theory: union and intersection, either in their indexed and in their simple forms, power set, and a class builder.
• Arithmetic: cardinals, ordinals and natural numbers are constructed, along with recursion, equinumerosity, induction, operations and other concepts of arithmetic.
• Real and complex numbers: the real and complex numbers are constructed from Dedekind cuts, and the concepts of sequences, limits and so on are developed for them. The exponential and trigonometric functions are implemented.
• Topology: Topology and metric spaces are currently developped.
• Algebra: we can also found some theorems of algebra concerning groups, rings and vector spaces.

"set.mm" is available on the internet.^[2] The "Metamath Proof Explorer" includes a set of HTML pages that present the proofs of "set.mm" in a human-friendly way. It is linked with a "Hilbert Space Explorer" that contains more than 1,000 theorems pertaining to the Hilbert space. Yet another "Explorer" shows separate proofs related to quantum logic.^[8]

A table of contents at the top of the Proof Explorer gives a comprehensive list of all of its covered topics.^[9]

[edit] 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.^[10][11] 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 too much detailed for being used with ease in school. However, set.mm can be used in a school context, as an example of a symbolic system, big enough to be interesting. set.mm can also be useful because its detailed, symbolic, unambiguous definitions can bring disambiguate confusing textbook definitions.

Megill gives a list of text books^[12] 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.

[edit] Annexe 2: Other works connected to Metamath

Using the design ideas implemented in Metamath, Raph Levien has realized what might be the smallest proof checker in the world in terms of code. Called Ghilbert^[13], the program is only 500 lines of Python code long. 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 Metamath design principles, Juha Arpiainen has realized his own proof checker called Bourbaki (in Common Lisp)^[14] and Marnix Klooster has coded a proof checker in Haskell (called Hmm^[15]). Although they all use the overall Metamath approach to formal system checker coding, they also implement new concepts of their own.

Mel O'Cat designed a system called mmj2^[16] which provides a graphic user interface for proof entry. It may be useful for those unable or unwilling to write long symbolic formulas without aid. There is also a project to add a graphical user interface to Metamath called mmide^[17].

"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 and and a formalization of natural deduction called nat.mm^[18]. 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.

[edit] References