Metamath

From Wikipedia, the free encyclopedia

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

Metamath Proof Explorer

URL	http://au.metamath.org/mpegif/mmset.html
Commercial?	No
Type of site	Internet encyclopedia project
Registration	No
Owner	Norman Megill
Created by	Norman Megill

The Metamath program, devised by Norman Megill, is an automated proof verifier for mathematical theorems.^[1] Given a set of axioms and definitions, Metamath can verify proofs of mathematical theorems using only one rule, substitution, with optional provisos (specified in the axioms) 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.^[2]

Metamath, however, cannot simply prove a theorem automatically. It can only verify proofs for correctness, and such proofs must be entered by a user.^[3] Also, unlike proof verifiers like Mizar that present shorter, more traditional proofs, Metamath presents proofs in a simple, step-by-step format.^[4][5], It has also the particularity of being a very short program in terms of number of lines of code. The language used to code proof is also remarkably short and therefore easy to learn.

Contents 1 Behind the scene, the soul of Turing 2 A 6,000 theorems database 3 Can Metamath be used as a pedagogical tool? 4 Mathematics as one has never seen them before 5 The Metamath language 6 A lively project 7 Other works connected to Metamath 8 References

[edit] Behind the scene, the soul of Turing

The reason why Metamath is such a concise program is due to the philosophy that underlies it. The Church-Turing thesis says that "Every function which would naturally be regarded as computable can be computed by a Turing machine." Considering that checking a proof can be viewed as a "function which would naturally be regarded as computable" one can therefore infers that it can be done by the simple "read and write" algorithm described by a Turing machine. Following this principle Metamath does no more than reading a set of formulas, comparing them with the hypotheses of a rule of inference and writing the conclusion. The universality of the Church-Turing's thesis simply ensures us that any logic can be implemented using Metamath including non-standard logics like lambda calculus, or natural deduction.

This design also explains why substitutions of set variables and bound variables checking are not managed by the software. Any time one needs a theorem which substitutes set variables by others or which checks if variables are bound, one needs to prove it. Axioms have been designed to allow that sort of proofs.

Quantum Logic Explorer

URL	http://us2.metamath.org:8888/qlegif/mmql.html
Commercial?	No
Type of site	Internet encyclopedia project
Registration	No
Owner	Norman Megill
Created by	Norman Megill and Mladen Pavičić

The only exception to this Church-Turing philosophy is the presence of a device to deal with distinct variables (the so called $d statement). According to the Church-Turing thesis this device is perfectly unnecessary and a system has been realized where this device is not used^[6]. However such a system is highly inhuman to handle and for comfort's sake the $d statements have been added.

[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.^[8] 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.^[9]

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

[edit] Can Metamath be used as a pedagogical tool?

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.^[11][12] 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, Metamath can be used as a huge example of what a symbolic system means and set.mm can also be useful because its detailed, unambiguous definitions can bring relief when one is in doubt about what a text book, with its informal and sometimes highly ambiguous definitions, means.

Megill gives a list of text books^[13] 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] Mathematics as one has never seen them before

One has been told that all mathematics could be derived from a handful of axioms. But one has never seen that concretely. In fact it is even difficult to represent oneself how all mathematics could be derived so. In school matters are presented independently, and it's difficult to imagine how for instance logic can cooperate with set theory and topology to make you able to calculate an integral. Methamath is the device that will make one able to have a very precise picture of how all that sort of things work together.

In the rest of the section I'll try to make a small guided tour of set.mm. Let's begin with propositional calculus. In metamath there is no special symbol for definition. The biimplication is used instead. But it means that there is a problem: how to define the biimplication itself. Here is the solution: df-bi I will leave predicate calculus rather untouched however I don't resist to show on an example that an implication is not an inference ( as it can be so often belived ). Here is a counterexample: 19.20.html, 19.20i.html. In one case the antecedent has to be quantified whereas in the other the premisse doesn't need it.

[edit] The Metamath language

This language is only based on markups. These markups are not very numerous. The existing markups follow very straightforwardly 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). The well formed formula are built using the the $a markup. The axioms are declared using the $a markup. The 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 then comes the description of what is considered as a proof. The metamath language uses the $p markup to declare proof.

There are some remarks to do 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 fused: the three sorts of rules use the $a markup. It is remarkably concise and this really brings an interesting view on the similar nature of syntactical rules and of axioms. When we look a proof with the Metamath command sh n / all command we can see 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 consists in the fact that the definiendum can be replaced (and thus eliminated) by the definiens. Here as well the integrative nature of the system appears clearly. The symbol used by Metamath to link definiens and definiendum is the biimplication operator. In text books it is frequent to meet a special operator in this case. But using a simple biimplication operator allows the use of the normal propositional calculus to deal with definition. Once more the integration of the system has been seeked.
3. [On theorems and proof] In Metamath a proof is connected to a theorem. And theorems are declared using the $p markup. Since the notion of proof and of theorems are tightly connected we will use both these terms as synonyms. 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 differs on several point as for what is regarded as a proof. First whereas theoretical logic in the most jansenism manner only accepts the axioms and the inferences declared in the language, Metamath (following the mathematical habit) accepts the use of other theorems previously proved. A second difference i sthat in theoretical logic, theorems have no hypotheses whereas in Metamath they do (using the $e statement). A third difference is that the very essence of proofs is captured by Metamath since only the names of the used rules are stored, the exact appearance of the formulas being obviously considered superfluous.
4. [Type of variables] In metamath variables are typed with the $f statement. In set.mm for instance there are three sorts of variables: propositional variables, individual variables and class variables.
5. [Schemes] Whereas 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.^[14]. Since schemes is the normal, intuitive way to do mathematics, the user shouldn't bother about it.
6. [Ascii symbols] set.mm uses a huge list of ascii symbols to write down the usual mathematical concepts. This list is remarkably well designed and can be used outside from Metamath to communicate mathematical ideas in media where ascii is mlandatory (mails and so on). For instance [ x / y ] ph is the way to write down the formula that corresponds to ph when y has been properly substituted by x. ( F ` B ) is used to write down the value of B by the function F ^[15]. This notation is an invention of Quine and is used to avoid the ambiguity of parentheses normally found in litterature. 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.^[16]

[edit] A lively project

Thanks to Megill, the activity is very intense, and new theorems are added to the database everyday. Most recently (as of August 2006), some topology, metric space, and Hilbert space theorems have been developed. A table of the most recent proofs is maintained.^[8] Help and information can be received either by asking Megill himself who is always willing to help people, or by consulting a wiki where some FAQs are gathered.

[edit] 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^[17], 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 as well Metamath design principles, Juha Arpiainen has realized his own proof checker called Bourbaki (in Common Lisp)^[18] and Marnix Klooster has coded a proof checker in Haskell (called Hmm^[19]). 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^[20] which provides a graphic user interface for proof entry. May be precious if you are somebody who, like me and contrary to Norman, is unable to write tons of long symbolic formulas on a sheet of paper with the only help of your pencil. There is also a project to add a graphical user interface to Metamath called mmide^[21].

"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^[22]. 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