HOME

TheInfoList



OR:

Metamath is a
formal language In logic, mathematics, computer science, and linguistics, a formal language consists of words whose letters are taken from an alphabet and are well-formed according to a specific set of rules. The alphabet of a formal language consists of sym ...
and an associated computer program (a proof checker) for archiving, verifying, and studying mathematical proofs. Several databases of proved theorems have been developed using Metamath covering standard results in
logic Logic is the study of correct reasoning. It includes both formal and informal logic. Formal logic is the science of deductively valid inferences or of logical truths. It is a formal science investigating how conclusions follow from premi ...
,
set theory Set theory is the branch of mathematical logic that studies sets, which can be informally described as collections of objects. Although objects of any kind can be collected into a set, set theory, as a branch of mathematics, is mostly concer ...
,
number theory Number theory (or arithmetic or higher arithmetic in older usage) is a branch of pure mathematics devoted primarily to the study of the integers and integer-valued functions. German mathematician Carl Friedrich Gauss (1777–1855) said, "Mathe ...
,
algebra Algebra () is one of the broad areas of mathematics. Roughly speaking, algebra is the study of mathematical symbols and the rules for manipulating these symbols in formulas; it is a unifying thread of almost all of mathematics. Elementary ...
,
topology In mathematics, topology (from the Greek words , and ) is concerned with the properties of a geometric object that are preserved under continuous deformations, such as stretching, twisting, crumpling, and bending; that is, without closing ...
and
analysis Analysis ( : analyses) is the process of breaking a complex topic or substance into smaller parts in order to gain a better understanding of it. The technique has been applied in the study of mathematics and logic since before Aristotle (384 ...
, among others. , the set of proved theorems using Metamath is one of the largest bodies of formalized mathematics, containing in particular proofs of 74 of the 100 theorems of the "Formalizing 100 Theorems" challenge, making it fourth after
HOL Light HOL Light is a member of the HOL theorem prover family. Like the other members, it is a proof assistant for classical higher order logic. Compared with other HOL systems, HOL Light is intended to have relatively simple foundations. HOL Light is a ...
, Isabelle, and Coq, but before Mizar, ProofPower, Lean, Nqthm,
ACL2 ACL2 ("A Computational Logic for Applicative Common Lisp") is a software system consisting of a programming language, created by Timothy Still it was an extensible theory in a first-order logic, and an automated theorem prover. ACL2 is designed to ...
, and Nuprl. There are at least 19 proof verifiers for databases that use the Metamath format. This project is the first one of its kind that allows for interactive browsing of its formalized theorems database in the form of an ordinary website.


Metamath language

The Metamath language is a
metalanguage In logic and linguistics, a metalanguage is a language used to describe another language, often called the ''object language''. Expressions in a metalanguage are often distinguished from those in the object language by the use of italics, quot ...
, suitable for developing a wide variety of
formal system A formal system is an abstract structure used for inferring theorems from axioms according to a set of rules. These rules, which are used for carrying out the inference of theorems from axioms, are the logical calculus of the formal system. A form ...
s. 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).


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 $ 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 $.
    $
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 Predicate or predication may refer to: * Predicate (grammar), in linguistics * Predication (philosophy) * several closely related uses in mathematics and formal logic: **Predicate (mathematical logic) **Propositional function **Finitary relation, o ...
. 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. 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 . It is the conclusion of the theorem opreq2i. The theorem opreq2i states that if , then . 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 with . There is only one way to do so: unifying with , with , with and with . So now Metamath uses the premise of opreq2i. This premise states that . As a consequence of its previous computation, Metamath knows that should be substituted by and by . The premise becomes 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 with it has to check that the syntactical rules are respected. In fact has the type class thus Metamath has to check that is also typed class.


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 a Metamath database into memory, verify the proofs of a database, modify the database (in particular by adding proofs), and write them back out to storage. It has a ''prove'' command that enables users to enter a proof, along with mechanisms to search for existing proofs. The Metamath program can convert statements to
HTML The HyperText Markup Language or HTML is the standard markup language for documents designed to be displayed in a web browser. It can be assisted by technologies such as Cascading Style Sheets (CSS) and scripting languages such as JavaScript ...
or TeX notation; for example, it can output the
modus ponens In propositional logic, ''modus ponens'' (; MP), also known as ''modus ponendo ponens'' (Latin for "method of putting by placing") or implication elimination or affirming the antecedent, is a deductive argument form and rule of inference. It ...
axiom from set.mm as: :\vdash \varphi\quad\&\quad \vdash ( \varphi \rightarrow \psi )\quad\Rightarrow\quad \vdash \psi Many other programs can process Metamath databases, in particular, there are at least 19 proof verifiers for databases that use the Metamath format.


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 :''In mathematical physics, ''Hilbert system'' is an infrequently used term for a physical system described by a C*-algebra.'' In logic, especially mathematical logic, a Hilbert system, sometimes called Hilbert calculus, Hilbert-style deductiv ...
of formal deduction though this is not a requirement.


Metamath Proof Explorer

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 First-order logic—also known as predicate logic, quantificational logic, and first-order predicate calculus—is a collection of formal systems used in mathematics, philosophy, linguistics, and computer science. First-order logic uses quantifi ...
and ZFC set theory (with the addition of Tarski-Grothendieck set theory when needed, for example in
category theory Category theory is a general theory of mathematical structures and their relations that was introduced by Samuel Eilenberg and Saunders Mac Lane in the middle of the 20th century in their foundational work on algebraic topology. Nowadays, cat ...
). The database has been maintained for over twenty years (the first proofs in ''set.mm'' are dated August 1993). 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, and elementary geometry. This database was first created by Norman Megill, but as of 2019-10-04 there have been 48 contributors (including Norman Megill). The Metamath Proof Explorer references many text books that can be used in conjunction with Metamath. Thus, people interested in studying mathematics can use Metamath in connection with these books and verify that the proved assertions match the literature.


Intuitionistic Logic Explorer

This database develops mathematics from a constructive point of view, starting with the axioms of
intuitionistic logic Intuitionistic logic, sometimes more generally called constructive logic, refers to systems of symbolic logic that differ from the systems used for classical logic by more closely mirroring the notion of constructive proof. In particular, systems o ...
and continuing with axiom systems of
constructive set theory Constructive set theory is an approach to mathematical constructivism following the program of axiomatic set theory. The same first-order language with "=" and "\in" of classical set theory is usually used, so this is not to be confused with a c ...
.


New Foundations Explorer

This database develops mathematics from Quine's
New Foundations In mathematical logic, New Foundations (NF) is an axiomatic set theory, conceived by Willard Van Orman Quine as a simplification of the theory of types of ''Principia Mathematica''. Quine first proposed NF in a 1937 article titled "New Foundation ...
set theory.


Higher-Order Logic Explorer

This database starts with
higher-order logic mathematics and logic, a higher-order logic is a form of predicate logic that is distinguished from first-order logic by additional quantifiers and, sometimes, stronger semantics. Higher-order logics with their standard semantics are more express ...
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 Robert Martin Solovay (born December 15, 1938) is an American mathematician specializing in set theory. Biography Solovay earned his Ph.D. from the University of Chicago in 1964 under the direction of Saunders Mac Lane, with a dissertation on ' ...
formalizes
Peano arithmetic In mathematical logic, the Peano axioms, also known as the Dedekind–Peano axioms or the Peano postulates, are axioms for the natural numbers presented by the 19th century Italian mathematician Giuseppe Peano. These axioms have been used nearly ...
. The database ''nat.mm'' formalizes
natural deduction In logic and proof theory, natural deduction is a kind of proof calculus in which logical reasoning is expressed by inference rules closely related to the "natural" way of reasoning. This contrasts with Hilbert-style systems, which instead use a ...
. The database ''miu.mm'' formalizes the
MU puzzle The MU puzzle is a puzzle stated by Douglas Hofstadter and found in '' Gödel, Escher, Bach'' involving a simple formal system called "MIU". Hofstadter's motivation is to contrast reasoning within a formal system (ie., deriving theorems) against rea ...
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 In mathematics, Hilbert spaces (named after David Hilbert) allow generalizing the methods of linear algebra and calculus from (finite-dimensional) Euclidean vector spaces to spaces that may be infinite-dimensional. Hilbert spaces arise natural ...
theory which have now been merged into the Metamath Proof Explorer, and the "Quantum Logic Explorer", which develops
quantum logic In the mathematical study of logic and the physical analysis of quantum foundations, quantum logic is a set of rules for manipulation of propositions inspired by the structure of quantum theory. The field takes as its starting point an observa ...
starting with the theory of orthomodular lattices.


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 Lambda calculus (also written as ''λ''-calculus) is a formal system in mathematical logic for expressing computation based on function abstraction and application using variable binding and substitution. It is a universal model of computation t ...
. However, Metamath provides no direct support for
natural deduction In logic and proof theory, natural deduction is a kind of proof calculus in which logical reasoning is expressed by inference rules closely related to the "natural" way of reasoning. This contrasts with Hilbert-style systems, which instead use a ...
systems. As noted earlier, the database ''nat.mm'' formalizes natural deduction. The Metamath Proof Explorer (with its database ''set.mm'') instead uses a set of conventions that allow the use of natural deduction approaches within a Hilbert-style logic.


Other works connected to Metamath


Proof checkers

Using the design ideas implemented in Metamath,
Raph Levien Raphael Linus Levien (also known as Raph Levien; born April 6, 1970) is a software developer, a member of the free software developer community, through his creation of the Advogato virtual community and his work with the free software branch of G ...
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. 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 Common Lisp (CL) is a dialect of the Lisp programming language, published in ANSI standard document ''ANSI INCITS 226-1994 (S20018)'' (formerly ''X3.226-1994 (R1999)''). The Common Lisp HyperSpec, a hyperlinked HTML version, has been derived f ...
called Bourbaki and Marnix Klooster has coded a proof checker in
Haskell Haskell () is a general-purpose, statically-typed, purely functional programming language with type inference and lazy evaluation. Designed for teaching, research and industrial applications, Haskell has pioneered a number of programming lang ...
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 The GUI ( "UI" by itself is still usually pronounced . or ), graphical user interface, is a form of user interface that allows users to interact with electronic devices through graphical icons and audio indicator such as primary notation, inste ...
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 (unlike Metamath). This technical difference brings more comfort to the user. In particular Metamath sometimes hesitates between several formulas it 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. Milpgame is a proof assistant and a checker (it shows a message only something gone wrong) with a
graphic user interface The GUI ( "UI" by itself is still usually pronounced . or ), graphical user interface, is a form of user interface that allows users to interact with electronic devices through graphical icons and audio indicator such as primary notation, inste ...
for the Metamath language(set.mm),written by Filip Cernatescu, it is an open source(MIT License) Java application (cross-platform application: Window,Linux,Mac OS). User can enter the demonstration(proof) in two modes : forward and backward relative to the statement to prove. Milpgame checks if a statement is well formed (has a syntactic verifier). It can save unfinished proofs without the use of dummylink theorem. The demonstration is shown as tree, the statements are shown using html definitions (defined in typesetting chapter). Milpgame is distributed as Java .jar(JRE version 6 update 24 written in NetBeans IDE).


See also

*
Automated proof checking In computer science and mathematical logic, a proof assistant or interactive theorem prover is a software tool to assist with the development of formal proofs by human-machine collaboration. This involves some sort of interactive proof edit ...
*
Proof assistant In computer science and mathematical logic, a proof assistant or interactive theorem prover is a software tool to assist with the development of formal proofs by human-machine collaboration. This involves some sort of interactive proof editor ...


References

{{Reflist


External links


Metamath
official website.
What do mathematicians think of Metamath
opinions on Metamath. Free mathematics software Free theorem provers Large-scale mathematical formalization projects Proof assistants