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 symb ...
and an associated computer program (a
proof checker
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 ...
) 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 premises ...
,
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 conce ...
,
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 arithmetic function, integer-valued functions. German mathematician Carl Friedrich Gauss (1777â ...
,
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 a ...
,
topology
In mathematics, topology (from the Greek language, Greek words , and ) is concerned with the properties of a mathematical object, geometric object that are preserved under Continuous function, continuous Deformation theory, deformations, such ...
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 (38 ...
, 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 aut ...
,
Isabelle
Isabel is a female name of Spanish origin. Isabelle is a name that is similar, but it is of French origin. It originates as the medieval Spanish form of '' Elisabeth'' (ultimately Hebrew ''Elisheva''), Arising in the 12th century, it became popul ...
, and
Coq
Coq is an interactive theorem prover first released in 1989. It allows for expressing mathematical assertions, mechanically checks proofs of these assertions, helps find formal proofs, and extracts a certified program from the constructive proof ...
, but before
Mizar
Mizar is a second-magnitude star in the handle of the Big Dipper asterism in the constellation of Ursa Major. It has the Bayer designation ζ Ursae Majoris ( Latinised as Zeta Ursae Majoris). It forms a well-known naked eye d ...
,
ProofPower,
Lean
Lean, leaning or LEAN may refer to:
Business practices
* Lean thinking, a business methodology adopted in various fields
** Lean construction, an adaption of lean manufacturing principles to the design and construction process
** Lean governm ...
,
Nqthm
Nqthm is a theorem prover sometimes referred to as the Boyer–Moore theorem prover. It was a precursor to ACL2.
History
The system was developed by Robert S. Boyer and J Strother Moore, professors of computer science at the University of Texas ...
,
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 JavaScri ...
or
TeX
Tex may refer to:
People and fictional characters
* Tex (nickname), a list of people and fictional characters with the nickname
* Joe Tex (1933–1982), stage name of American soul singer Joseph Arrington Jr.
Entertainment
* ''Tex'', the Italian ...
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. ...
axiom from set.mm as:
:
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 deductive ...
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 quantifie ...
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, cate ...
). 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 ...
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 co ...
.
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 Foundations ...
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 u ...
. 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 axiom ...
. 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 re ...
based on the formal system MIU presented in ''
Gödel, Escher, Bach
''Gödel, Escher, Bach: an Eternal Golden Braid'', also known as ''GEB'', is a 1979 book by Douglas Hofstadter.
By exploring common themes in the lives and works of logician Kurt Gödel, artist M. C. Escher, and composer Johann Sebastian Bach, t ...
''.
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 observat ...
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 ...
.
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 axiom ...
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 ...
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 fro ...
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 editor ...
*
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