Metamath
| Metamath
|
|
|---|---|
|
|
| Basic data
|
|
| developer | Norman Megill |
| operating system | Microsoft Windows , Mac OS X , Linux |
| category | computerized evidence verifier |
| License | GNU General Public License |
| www.metamath.org | |
Metamath is, on the one hand, a programming language that can describe formal systems and proofs carried out in such systems ; on the other hand, it is an online archive of formal proofs that have been carried out with the Metamath programming language. Unlike the informal proofs commonly used in mathematics , Metamath can reduce every single logical step in a proof to the elementary manipulation of character strings .
motivation
Formal theories are based on a set of axioms , the basic assumptions of a theory, and inference rules in order to derive further theorems from axioms or already proven theorems . The axioms and rules of inference are written in a formal language.
The author describes the Principia Mathematica by Alfred North Whitehead and Bertrand Russell as a major influence on Metamath.
At its core, (formal) mathematics can be reduced to a simple manipulation of character strings. The standard axiomatization of mathematics is based on the ZFC ( Zermelo-Fraenkel set theory ), the majority of the proofs in the Metamath proof archive require ZFC. In fact, Metamath can be used to verify evidence in all kinds of Formal Systems. It allows the free definition of axioms and inference rules for a formal system, similar to a semi-thue system .
overview
Metamath itself is in ANSI C written. For additional verification of metamath proofs, there are proof verifiers written in different programming languages , including a Python script with just 500 lines of code . The simplicity of Metamath (the only rule applied is substitution) and the redundant verifiers completely rule out errors in a formal proof carried out with Metamath. The evidence archive for ZFC - set.mm - is hosted on github , the complete project with source code is available on the main page.
The Metamath Proof Explorer is a directory with 23,000 theorems proven on the basis of ZFC from various branches of mathematics. Every proof of a corresponding theorem can be traced back to the axioms of ZFC and the axioms and inference rules of predicate logic . Only axioms, inference rules or theorems formally derived from axioms and inference rules may be used for proof steps. Proof Explorer is also available offline via a CLI implementation of Metamath. In addition to set.mm, other databases of formal systems are available, including databases with formal evidence for quantum logic and intuitionistic logic .
example
The following formal proof is carried out in a Hilbert calculus and then converted into Metamath. Let two axioms be given in a well-defined form:
A1: (t=r -> (t=s -> r=s)) A2: (t + 0) = t
as well as the final rule modus ponens .
We want to derive t = t.
1. (t + 0) = t 2. (t + 0) = t 3. (t + 0) = t -> ((t+0)=t -> t=t) 4. ((t+0)=t -> t=t) 5. t=t
In Metamath this proof can also be given. First we define the constant symbols that we will use.
$c 0 + = -> ( ) term wff |- $.
“$ C” symbolizes the beginning of a constant declaration, “$.” Its end. As is common in many programming languages, the lexical separator symbol is a space.
Now the metavariables are defined,
$v t r s P Q $.
as well as their properties,
tt $f term t $. tr $f term r $. ts $f term s $. wp $f wff P $. wq $f wff Q $.
and also a formal grammar to define what a well-formed sentence is
tze $a term 0 $. tpl $a term ( t + r ) $. weq $a wff t = r $. wim $a wff ( P -> Q ) $.
The two axioms
A1: $a |- ( t = r -> ( t = s -> r = s ) ) $. A2: $a |- ( t + 0 ) = t $.
and the final rule (also called inference rule) modus ponens
${
min $e |- P $.
maj $e |- ( P -> Q ) $.
mp $a |- Q $.
$}
complete the specification of this formal theory. As in the above example, the statement t = t should now be proven in theory.
th1 $p |- t = t $=
Metamath can now assist in proving the theorem via the Command Line Interface. Metamath allows exactly those operations that have been declared as valid in the axioms and inference rules part. This makes mistakes in the proof impossible. There are various “levels of detail” for every proof, ranging from detailed information on each individual substitution to the usual Hilbert calculus-compliant presentation;
1 a2 $a |- ( t + 0 ) = t 2 a2 $a |- ( t + 0 ) = t 3 a1 $a |- ( ( t + 0 ) = t -> ( ( t + 0 ) = t -> t = t ) ) 4 2,3 mp $a |- ( ( t + 0 ) = t -> t = t ) 5 1,4 mp $a |- t = t
See also
Individual evidence
- ↑ Metamath Homepage Website of the Metamath project.
- ^ The Metamath Home Page Website of the University of Waterloo. Retrieved May 4, 2017.
- ↑ Norman Megill: Introduction. In: Metamath - A Computer Language for Pure Mathematics. 2017, p. 4.
- ↑ Norman Megill: Introduction. In: Metamath - A Computer Language for Pure Mathematics. 2017, p. 30.
- ↑ Norman Megill: Introduction. In: Metamath - A Computer Language for Pure Mathematics. 2017, pp. 3–4.
- ^ Metamath ZFC database