Metamath: Difference between revisions
Line 129: | Line 129: | ||
== The Metamath proof checker == |
== The Metamath proof checker == |
||
The Metamath program is the original program created to manipulate databases written using the Metamath language. It has a text (command line) interface and is written in C. It can read Metamath databases, modify them (such as by adding proofs), and write them back out to storage. |
|||
The Metamath program can convert statements to [[HTML]] or [[TeX]] notation; |
The Metamath program can convert statements to [[HTML]] or [[TeX]] notation; |
||
for example, the [[modus ponens]] axiom from set.mm: |
for example, it can output the [[modus ponens]] axiom from set.mm as: |
||
:<math>\vdash \varphi\quad\&\quad \vdash ( \varphi \rightarrow \psi )\quad\Rightarrow\quad \vdash \psi</math> |
:<math>\vdash \varphi\quad\&\quad \vdash ( \varphi \rightarrow \psi )\quad\Rightarrow\quad \vdash \psi</math> |
Revision as of 21:32, 14 July 2019
![]() | |
Developer(s) | Norman Megill |
---|---|
Repository | |
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 formal language and an associated computer program (a proof checker) for archiving, verifying, and studying mathematical proofs.[1]. Several databases of proved theorems have been developed using Metamath covering standard results in logic, set theory, number theory, algebra, topology and analysis, among others.[2].
As of July 2019, the set of proved theorems using Metamath is one of the largest bodies of formalized mathematics, containing in particular proofs of 71[3] of the 100 theorems of the "Formalizing 100 Theorems" challenge, making it third after HOL Light and Isabelle, but before Coq, Mizar, ProofPower, Lean, Nqthm, ACL2, and Nuprl.
The Metamath language
The Metamath language is a metalanguage, suitable for developing a wide variety of formal systems. The Metamath language has no specific logic embedded in it. Instead, it can simply be regarded as a way to prove that inference rules (asserted as axioms or proven later) can be applied. The largest database of proved theorems follows conventional ZFC set theory and classic logic, but other databases exist and others can be created.
The Metamath language design is focused on simplicity; the language, 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).[4]
Language Basics
The set of symbols that can be used for constructing formulas is declared using $c
(constant symbols)
and $v
(variable symbols) 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
(floating (variable-type)
hypotheses) and $a
(axiomatic assertion) 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 and
optional $e
(essential hypotheses) statements; 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 $. $}
Using one construct, $a
statements, to capture syntactic rules, axiom schemas, and rules of inference is intended to provide a level of flexibility similar to higher order logical frameworks without a dependency on a complex type system.
Proofs
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
Substitution
All Metamath proof steps use a single substitution rule, which is just the simple replacement of a variable with an expression and not the proper substitution described in works on predicate calculus. Proper substitution, in Metamath databases that support it, is a derived construct instead of one built into the Metamath language itself.
The substitution rule makes no assumption about the logic system in use and only requires that the substitutions of variables are correctly done.
![](http://upload.wikimedia.org/wikipedia/commons/7/7b/Proofstep.gif)
Here is a detailed example of how this algorithm works. Steps 1 and 2 of the theorem 2p2e4
in the Metamath Proof Explorer (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.
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
.
The Metamath proof checker
The Metamath program is the original program created to manipulate databases written using the Metamath language. It has a text (command line) interface and is written in C. It can read Metamath databases, modify them (such as by adding proofs), and write them back out to storage.
The Metamath program can convert statements to HTML or TeX notation; for example, it can output the modus ponens axiom from set.mm as:
Metamath databases
The Metamath website hosts several databases that store theorems derived from various axiomatic systems. Most databases (.mm files) have an associated interface, called an "Explorer", which allows one to navigate the statements and proofs interactively on the website, in a user-friendly way. Most databases use a Hilbert system of formal deduction though this is not a requirement.
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/mpeuni/mmset.html |
Commercial | No |
Registration | No |
The Metamath Proof Explorer (recorded in set.mm) is the main and by far the largest database, with over 23,000 proofs in its main part as of July 2019. It is based on classical first-order logic and ZFC set theory (with the addition of Tarski-Grothendieck set theory when needed, for example in category theory). The database has been maintained for over twenty years (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 contributors. The database contains developments, among other fields, of set theory (ordinals and cardinals, recursion, equivalents of the axiom of choice, the continuum hypothesis...), the construction of the real and complex number systems, order theory, graph theory, abstract algebra, linear algebra, general topology, real and complex analysis, Hilbert spaces, number theory, elementary geometry...
Intuitionistic Logic Explorer
This database develops mathematics from a constructive point of view, starting with the axioms of intuitionistic logic and continuing with axioms of constructive set theory.
New Foundations Explorer
This database develops mathematics from Quine's New Foundations set theory.
Higher-Order Logic Explorer
This database starts with higher-order logic and derives equivalents to axioms of first-order logic and of ZFC set theory.
Databases without explorers
The Metamath website hosts a few other databases which are not associated with explorers but are nonetheless noteworthy. The database peano.mm written by Robert Solovay formalizes Peano arithmetic. The database nat.mm[6] formalizes natural deduction. The database miu.mm formalizes the MU puzzle based on the formal system MIU presented in Gödel, Escher, Bach.
Older explorers
The Metamath website also hosts a few older databases which are not maintained anymore, such as the "Hilbert Space Explorer", which presents theorems pertaining to Hilbert space theory which have now been merged into the Metamath Proof Explorer, and the "Quantum Logic Explorer", which develops quantum logic starting with the theory of orthomodular lattices.
Deduction and Natural Deduction
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.
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.[7][8] 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.[9] 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.[10] 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[11] and Marnix Klooster has coded a proof checker in Haskell called Hmm.[12]
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.[13] 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.[14] 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.
See also
References
- ^ Megill, Norman; Wheeler, David A. (2019-06-02). Metamath: A Computer Language for Mathematical Proofs (Second Edition ed.). Morrisville, North Carolina, US: Lulul Press. p. 248. ISBN 978-0-359-70223-7.
{{cite book}}
:|edition=
has extra text (help) - ^ Megill, Norman. "What is Metamath?". Metamath Home Page.
- ^ Metamath 100.
- ^ Megill,Norman. "How Proofs Work". Metamath Proof Explorer Home Page.
- ^ "Metamath.org Site Info". Alexa Internet. Retrieved 2019-02-02.
- ^ Liné, Frédéric. "Natural deduction based Metamath system". Archived from the original on 2012-12-28.
{{cite web}}
: Unknown parameter|deadurl=
ignored (|url-status=
suggested) (help) - ^ Megill, Norman. "Mathematical vernacular". Archived from the original on 2012-12-28.
{{cite web}}
: Unknown parameter|deadurl=
ignored (|url-status=
suggested) (help) - ^ Wiedijk, Freek. "The mathematical vernacular" (PDF).
- ^ Megill, Norman. "Reading suggestions". Metamath.
- ^ Levien,Raph. "Ghilbert".
- ^ Arpiainen, Juha. "Presentation of Bourbaki". Archived from the original on 2012-12-28.
{{cite web}}
: Unknown parameter|deadurl=
ignored (|url-status=
suggested) (help) - ^ Klooster,Marnix. "Presentation of Hmm". Archived from the original on 2012-04-02.
{{cite web}}
: Unknown parameter|deadurl=
ignored (|url-status=
suggested) (help) - ^ O'Cat,Mel. "Presentation of mmj2". Archived from the original on December 19, 2013.
{{cite web}}
: Unknown parameter|deadurl=
ignored (|url-status=
suggested) (help) - ^ Hale, William. "Presentation of mmide". Archived from the original on 2012-12-28.
{{cite web}}
: Unknown parameter|deadurl=
ignored (|url-status=
suggested) (help)
External links
- Metamath: official website.
- What do mathematicians think of Metamath: opinions on Metamath.