MetamathHome
Last >
| Metamath Home |
Metamath Proof Explorer Home Page | First > Last > |
| This is the starting page for the Metamath Proof Explorer subproject. See the main Metamath Home Page for an overview of Metamath and download links. |
| Contents of this page | Related pages To search this site you can use Google [external] restricted to a mirror site. For example, to find references to infinity enter "infinity site:us.metamath.org". More efficient searching is possible with direct use of the Metamath program, once you get used to its ASCII tokens. See the wildcard features in "help search" and "help show statement". |
Inspired by Whitehead and Russell's monumental Principia Mathematica, the Metamath Proof Explorer has over 10,000 completely worked out proofs, starting from the very foundation that mathematics is built on and eventually arriving at familiar mathematical facts and beyond. Each proof is pieced together with razor-sharp precision using a simple substitution rule that practically anyone (with lots of patience) can follow, not just mathematicians. Every step can be drilled down deeper and deeper into the labyrinth until axioms of logic and set theory—the starting point for all of mathematics—will ultimately be found at the bottom. You could spend literally days exploring the astonishing tangle of logic leading, say, from the seemingly mundane theorem 2+2=4 back to these axioms.
Essentially everything that is possible to know in mathematics can be derived from a handful of axioms known as Zermelo-Fraenkel set theory, which is the culmination of many years of effort to isolate the essential nature of mathematics and is one of the most profound achievements of mankind.
The Metamath Proof Explorer starts with these axioms to build up its proofs. There may be symbols that are unfamiliar to you, but we show in detail how they are manipulated in the proofs, and in principle you don't have to know what they mean. In fact, there is a philosophy called formalism which says that mathematics is a game of symbols with no intrinsic meaning. With that in mind, Metamath lets you watch the game being played and the pieces manipulated according to simple and precise rules, one step at a time.
As humans, we observe interesting patterns in these "meaningless" symbol strings as they evolve from the axioms, and we attach meaning to them. One result is the set of natural numbers, whose properties match those we observe when we count everyday objects, and their extensions to rational and real numbers. Of course, numbers were discovered centuries before set theory, and historically they were "reversed engineered" back to the axioms of set theory. The proof of 2 + 2 = 4 shows what was involved in that reverse engineering, representing the work of many mathematicians from Dedekind to von Neumann. At the other extreme of abstraction is the theory of infinite sets or transfinite cardinal numbers. Some of the world's most brilliant mathematicians have given us deep insight into this mysterious and wondrous universe, which is sometimes called "Cantor's paradise."
Metamath's formal proofs are much more detailed than the proofs you see in textbooks. They are broken down into the most explicit detail possible so that you can see exactly what is going on. Each proof step represents a microscopic increment towards the final goal. But each step is derived from previous ones with a very simple rule, and you can verify for yourself the correctness of any proof with very little skill. All you need is patience. With no prior knowledge of advanced mathematics or even any mathematics at all, you can jump into the middle of any proof, from the most elementary to the most advanced, and understand immediately how the symbols were mechanically manipulated to go from one proof step to another, even if you don't know what the symbols themselves mean. In the next section we show you how.
|
[If you are a math novice (or not) and have trouble understanding this section, let me know what you find confusing so that I can try to improve it. An important point sometimes misunderstood is that Metamath is not a theorem prover—it does not find these proofs on its own but just verifies the correctness of proofs provided to it by its users.]
What you need to know The only rule you need to know in order to follow the symbol manipulations in a Metamath proof is substitution. Substitution consists of replacing the symbols for variables with expressions representing special cases of those variables. For example, in high-school algebra you learned that a + b = b + a, where a and b are variables (placeholders for numbers). Two substitution instances of this law are 5 + 3 = 3 + 5 and (x - 7) + c = c + (x - 7). That's the only mathematical concept you need! Substitution is just writing down a specific example of a more general formula.
[Note for logicians: The substitution in Metamath proofs is, indeed, simply the direct replacement of a variable with an expression. The more complex proper substitution of traditional logic is a derived concept in Metamath, broken down into multiple primitive steps. Distinct variable provisos, which accompany certain axioms and are inherited by theorems, forbid unsound substitutions.]
How it works To show you how this works in Metamath, we will break down and analyze a proof step in the proof of 2 + 2 = 4. Once you grasp this example, you will immediately be able to verify for yourself any proof in the database—no further prerequisites are needed. You may not understand what all (or any) of the symbols mean, but you can follow the rules for how they are manipulated, like game pieces, to prove theorems.
Compare this with the years of study it might take to be able to follow and verify a proof in an advanced math textbook. Typically such proofs will omit many details, implicitly assuming you have a deep knowledge of prior material. If you want to be a mathematician, you will still need those years of study to achieve a high-level understanding. Metamath will not provide you with that. But if you just want the ability to convince yourself that a string of math symbols that mathematicians call a "theorem" is a mechanical consequence of the axioms, Metamath's proof method lets you accomplish that.
Metamath's conceptual simplicity has a tradeoff, which is the often large number of steps needed for a complete proof all the way back to the axioms. But the proofs have been computer-verified, and you can choose to study only the steps that interest you and still have complete confidence that the rest are correct.
|
| Figure 1. Step 2 of the 2p2e4
proof references step 1, which in turn "feeds" the hypothesis of earlier
theorem opreq2i. The conclusion (assertion) of opreq2i then generates
step 2 of 2p2e4. Carefully note the substitutions (lassoed in thin orange
lines) that take place. New 21-Mar-2007 See also Paul Chapman's Metamath browser screenshot, which shows the substitutions explicitly. |
In the figure above we show part of the proof of the theorem 2 + 2 = 4, called 2p2e4 in the database. We will show how we arrived at proof step 2, which is an intermediate result stating that (2 + 2) = (2 + (1 + 1)). (This figure is from an older version of this site that didn't show indentation levels, and it is less cluttered for the purpose of this tutorial. The indentation levels and the little colored numbers can make a higher-level view of the proof easier to grasp.)
Look at Step 2 of the proof. In the Ref column,
we see that it references a previously proved theorem, opreq2i. The theorem opreq2i requires a
hypothesis, and in the Hyp column of Step 2 we indicate that Step 1 will
satisfy (match) this hypothesis.
We make
substitutions into the variables of the hypothesis of opreq2i so that it
matches the string of symbols in
the Expression column for Step 1. To achieve this, we substitute
the expression "2" for variable
and the expression "(1 + 1)" for variable
.
The middle symbol in the hypothesis of opreq2i is
"=", which is a constant, and we are not allowed to substitute
anything for a constant. Constants must match exactly.
Variables are always colored, and constants are always black (except
the gray turnstile 
, which you may ignore). This makes them easy to recognize.
The variables in our database have 3 possible colors, blue, red, and purple, representing wffs, sets, and classes
respectively. Don't worry about what these terms mean right now. All
variables, regardless of color, follow the same substitution rule.
In our example, the purple letters are variables, whereas the symbols
"(", ")", "1", "2", "=", and "+" are constants.
In this example, the constants are probably familiar symbols. In other cases they may not be. You should focus only on whether the symbols are variables or constants, not on what they "mean." Your only goal is to determine what substitutions into the variables of the referenced theorem are needed to make the symbol strings match.
In the Expression column of the Assertion box of opreq2i, there are 4
variables,
,
,
,
and
.
Because we have already made substitutions into the
hypothesis, variables
and
have been
committed to the assignments "2" and "(1 + 1)" respectively, and
we can't change these assignments. However, the new variables
and
are free to be assigned with any expression we want (subject to the
legal syntax
requirement described below). By substituting "2" for
and
"+" for
, we end up with
(2 + 2) = (2 + (1 + 1)) that we show in the Expression column
for Step 2 of the proof of 2p2e4.
[It may seem peculiar to substitute a + sign for a variable, because you wouldn't do that in high-school algebra. We can do this because the variables represent arbitrary objects called "classes," not just numbers. See the description for operation value df-opr (don't worry about right-hand side of the definition, for now). A number and a + sign are both classes. You have to free your mind to forget about high-school algebra—pretend you have no idea what a number or "+" is—and just look at what happens to the symbols, independent of any meaning. In fact (and ironically), it may be better to look at a proof where all the symbols are unfamiliar, perhaps aleph1re, so that you can observe the mechanical symbol substitutions without the distraction of preconceived notions.]
When we first created the proof, why did we choose these particular
substitutions for and ?
The reason is simple—they make the proof work! But how did we know
these particular substitutions should be picked, and not others? That's
the hard part—we didn't know, nor did we know that opreq2i should be
referenced in the second proof step, nor did we know that Step 1 would
have the right expression to match the hypothesis of opreq2i. The
choices were made using intelligent guesses, that were then verified to
work. This is a skill a mathematician develops with experience. Some
of the proofs in our database were discovered by famous mathematicians.
The Metamath Proof Explorer recaptures their efforts and shows you in
complete detail the proof steps and substitutions already worked out.
This allows you to follow a proof even if you are not a mathematician,
and be convinced that its conclusion is a consequence of the axioms.
Sometimes a referenced theorem (or axiom or definition) has no
hypotheses. In that case we omit and above and immediately proceed to
. When there are
multiple hypotheses, we repeat and for each one.
|
You may want to practice the above procedure for a few other proof steps to make sure you have grasped the idea.
The rest of this section has some notes on substitutions that you may find helpful and describes the additional requirements for correctness not mentioned above. As you will observe if you study a few proofs, the Metamath proof verifier has already ensured these requirements are met, so ordinarily you don't have to worry about them.
Notes on substitutions
Legal syntax
There is a further requirement for substitutions we have not described
yet. You can't substitute just any old string of symbols for a purple
class variable. Instead, the symbol string must qualify as a class
expression. For example, it would be illegal to substitute the
nonsensical "(1 +" for variable above. However, "(1 + 1)" is legal. Here is how you
can tell. "1" is a legal class by c1. "+" is a
legal class by caddc. Then, by making these
class substitutions into the class variables of co, we see that "(1 + 1)" is a legal class. But
there is no such construction that would let us show that the
nonsensical "(1 +" is a legal class.
[On the other hand, the fact that 1 and + are both classes means we are allowed to substitute them for any class variables at all, even where they normally wouldn't go. For example, it is legal to substitute + for C and 1 for F in opreq2i above, resulting in the seemingly nonsensical ( + 1 2 ) = ( + 1 ( 1 + 1 ) ). Believe it or not, this is a perfectly valid theorem of set theory! However, it jumps out of the subtheory of arithmetic and is of little use; it certainly doesn't help us make progress towards a proof of ( 2 + 2 ) = 4. We can play around with such ideas for fun to prove silly but still perfectly valid theorems like avril1, which if nothing else provides an interesting exercise for figuring out the substitutions involved in its proof.]
Similarly, blue wff variables and red set variables can be substituted only with expressions that qualify as those types.
In other words, we must "prove" that any expression we want to substitute for a variable qualifies as a legal expression for that type of variable, before we are allowed to make the substitution.
The actual proofs stored in the database have additional steps that construct, from syntax definitions, the expressions that are substituted for variables. We suppress these construction steps on the web pages because they would make the proofs very long and tedious. However, the syntax breakdown is straightforward to check by hand if you make use of the "Syntax hints" provided with each proof. Once you get used to the syntax, you should be able to "see" its breakdown in your head; in the meantime you can trust that the Metamath proof verifier did its job.
If you want to see for yourself the hidden steps that construct the variable substitutions for each proof step, you can display them using the Metamath program. For the proof above, use the commands "save proof 2p2e4 /normal" followed by "show proof 2p2e4 /all" in the Metamath program. (Follow the instructions for downloading and running the Metamath program. Try it, it's easy!) In the "/all" proof display, you will see that step 21 corresponds to step 2 of the figure above. Steps 14-17 are the hidden steps showing that "(1 + 1)" is a legal class as we described above. To see the substitutions we talked about for step 2, you can type "show proof 2p2e4 /detailed_step 21".
In the case of axioms and definitions, we do show their detailed syntax breakdown, because there is free space on those web pages not used for anything else. These can help you become familiar with the syntax. For example, look at the definition of the number 2, df-2. You can see, at step 4, the demonstration that "(1 + 1)" is a legal expression that qualifies as a class, i.e. that can be substituted for a purple class variable.
Distinct variable restrictions Our final requirement for substitutions is described in Appendix 3: Distinct Variables below. These restrictions have no effect on how you figure out the the substitutions that were made in a proof step. All they do is prohibit certain substitutions that would otherwise be legal based what we have described so far. Eventually you should learn how they work in order to complete your understanding of the mechanics of logic, but for now, you can trust that the Metamath proof verifier has ensured that they have been met.
[The material in this section is intended to be self-contained. However, you may also find it helpful to review these suggestions. A more extensive but still informal overview is given in Chapter 3, "Abstract Mathematics Revealed," of the Metamath book (1.3 MB PDF file; click on the fourth bookmark in your PDF reader).]
The axioms for (essentially) all of mathematics can be conveniently
divided into three groups: propositional calculus, predicate
calculus, and set theory. Each axiom is a string of
mathematical symbols of two kinds: constants, also called
connectives, which we show in black; and variables, which
we show using colors. The constants that occur in the axioms are
,
,
,
,
,
, and
(left parenthesis, right parenthesis, implies, not, equals, is contained
in, for all).
Variables are placeholders that can be substituted with other expressions (strings of symbols). There are two kinds of variables in the axioms, set variables (red) and wff ("well-formed formula") variables (blue). A set variable can be substituted only with a set variable (in other words with an expression of length one, whose only symbol is a set variable), whereas a wff variable can be substituted with any expression qualifying as a wff (see below).
[In later proofs you will see a third kind of variable, called a class variable, which is shown in purple and is a kind of generalization of the set variable. Class variables help us get around the restrictive substitution rule for set variables. Introduced via definitions, they are theoretically unnecessary but make our proofs much more efficient. A theorem with class variables can always be converted to an equivalent theorem with wff variables instead (for a technical discussion see abeq2). A class variable can be substituted with either a set variable or an expression qualifying as a class.]
Following the tradition in the literature, we use Greek letters for wff variables and lower-case italic letters for set variables.
[If you use a monochrome display or printout, the red variables are always lowercase italic letters, the purple ones uppercase italic, and the blue ones Greek. The colors are not necessary to disambiguate the symbols.]
Any mathematical object whatsoever, such as the number 2, the operation of taking a square root, or the surface of a sphere, is considered to be a set in set theory. The red set variables are placeholders that represent arbitrary sets.
A set can be equal to another set, can be contained in another set, and can contain other sets. For example, the set of real numbers contains, of course, all of the real numbers. A specific real number such as 2 is also a set, but not in such a familiar way—it contains a very complex construction of sets, a kind of machine inside of it that causes it to behave according to the laws for real numbers. The square root operation is a set containing an infinite number of ordered pairs, one for each nonnegative real number; the first member of each pair is the number and the second member its square root.
A wff is an expression (string of symbols)
constructed as follows.
A starting wff either is a wff variable, or it consists of two
set variables connected with either
("equals," "is identical to") or
("is an element of," "is contained in").
Two wffs may be connected with
("implies," "only if") to form a new wff, with parentheses around the
result to prevent ambiguity. A wff may be prefixed with
("not") to form a new wff. And finally, a wff may be prefixed with
("for all," "for each," "for every")
and a set variable to form a new wff. To summarize:
If
is a wff variable and
and
are set variables, then ,
,
and
are (starting) wffs.
If
and
are wffs and
is a set variable, then
,
,
and
are also wffs.
Note that a wff variable can be viewed as a wff in its own right as well as a placeholder for which other wffs can be substituted.
The axioms below are examples of wffs. Each page describing an axiom, for example ax-11, presents the axiom's construction in a syntax breakdown chart, showing that it follows these rules and is therefore a wff. You may want to look at a few of these to make sure you understand how wffs are constructed and how to deconstruct, or parse, them into their components.
Wffs are either true or false, depending on what is assigned
to the variables they contain.
For example, the wff
is true if
and
stand for
the same set and false otherwise—there is no in-between.
An axiom (example: ax-1) is a wff that we postulate to be true no matter what (within the constraints of the syntax rules) we substitute for its variables. An inference rule (example: ax-mp) consists of one or more wffs called hypotheses, together with a wff called the conclusion (which on our web pages with proofs we also call its assertion) that we postulate to be true provided the hypotheses are true. A proof is a sequence of substitution instances of axioms and inference rules, where the hypotheses of the inference rules match previous steps in the sequence. The last step in a proof is a theorem (example: id1). For brevity, a proof may also refer to earlier theorems (example: id), but in principle it can be expanded into references to only the initial axioms and rules. We also use the word "theorem" informally to denote the result of a proof that also allows references to local hypotheses and thus has the form of an inference rule (example: a1i); however, strictly speaking, such a theorem should be called a derived inference rule or deduction.
Propositional
calculus deals with general truths about wffs regardless of
how they are constructed. The simplest propositional
truth is
"
",
which can be read "if something
is true, then it is true"—rather trivial and obvious, but nonetheless
it must be proved from the axioms (see theorem id).
In an application of this truth, we could
replace
with a more specific wff to give us, for example,
"
". (You might think that
id
would be a useless bit of trivia, but in fact it is frequently used.
For example, look at its use in the proof of the law of assertion
pm2.27.)
Our system of propositional calculus consists of three axioms and the modus-ponens inference rule. It is attributed to Jan Łukasiewicz (pronounced woo-kah-SHAY-vitch) and was popularized by Alonzo Church, who called it system P2. (Thanks to Ted Ulrich for this information.)
| Axiom Simp | ax-1 |
|
| Axiom Frege | ax-2 |
 |
| Axiom Transp | ax-3 |
|
| Rule of Modus Ponens | ax-mp |  
|
The turnstile is a symbol (introduced by Frege in 1879) used in formal
logic to indicate that the wff that follows is provable (and is
traditionally used even for an axiom, which is "provable" in one step,
itself); it can be ignored for informal reading. (Technically, the
Metamath program needs an initial token to disambiguate the kind of
expression that follows. I figured, why not make it the turnstile that
logic books use? In the Quantum Logic Explorer, on the other hand, I
mapped it to a blank image because my physics colleague didn't like it.)
The symbols
and are
used informally in the table above to indicate the relationship between
hypotheses and conclusion; they are not part of the formal language.
Predicate
calculus introduces three new symbols, ("equals"), ("is a member of"), and ("for all"). The first two are called
"predicates." A predicate specifies a true or false relationship between its
two arguments. As an example, always evaluates to true
regardless of what is,
as the theorem equid demonstrates. The "for all"
symbol, also called the "universal quantifier," ranges over or "scans" all
possible values of its first (set variable) argument, applying them to the
second (wff) argument, and returns true if and only if the second argument is
true for every value of the first. The wff is read
"for all x, it is the case that phi is true." The axioms of predicate calculus
express the logical properties of these new symbols that are universally true,
independent from any theory (like set theory) making use of them. (What we
call "set variables" are more generally called "individual variables" in
predicate calculus without set theory.)
Our axiom system is closely related to a system of Tarski (see the note on the axioms below). Our system is exactly equivalent to the traditional axiom system in most logic textbooks but has the advantage of being easy to manipulate with a computer program. Each of our axioms corresponds to an axiom scheme of the traditional system.
|
The last axiom, ax-17, has a restriction on what substitutions we are allowed to make into its variables. This restriction is inherited by theorems that use this axiom, according to the substitutions made in their proofs, and you will often see distinct variable conditions associated with such theorems.
Eight other axioms, ax-4, ax-5o, ax-6o, ax-9o, ax-10o, ax-11o, ax-15, and ax-16, are not included in the table above because they can be derived from the ones in the table. From the set consisting of these 8 axioms plus the 11 axioms in the table above, several subsystems can be of interest for certain studies and are described below under Some Predicate Calculus Subsystems.
Some definitions will simplify our presentation of the set theory axioms, although in principle they could be eliminated. Specifically,
is an abbreviation for
is an abbreviation for
is an abbreviation for
, , and , and our wff construction rules are extended with
wb, wa, and wex. Alternately, you can rewrite the
set theory axioms
below with these three definitions eliminated.
Set theory
uses the formalism of propositional and predicate calculus to assert
properties of arbitrary mathematical objects called "sets." A set can
be contained in another set, and this relationship is indicated by the
symbol.
Starting with the simplest mathematical object, called the empty set,
set theory builds up more and more complex structures whose existence
follows from the axioms, eventually resulting in extremely complicated
sets that we identify with the real numbers and other familiar
mathematical objects. These axioms were developed in response to Russell's Paradox, a discovery that revolutionized
the foundations of mathematics and logic.
Except for Extensionality, the axioms basically say,
"given an arbitrary set (and, in the cases of Replacement and Regularity, provided
that an antecedent is satisfied), there exists another set based on or
constructed from it, with the stated properties." (The axiom of
Extensionality can also be restated this way as shown by axext2.) The individual axiom links provide more
detailed descriptions. We derive the redundant ZF axioms of
Separation,
Null Set, and
Pairing from the others as theorems.
In the ZFC axioms that follow, all set
variables are assumed to be distinct. If
you click on their links you will see the explicit distinct variable
conditions. (There is also an unusual
formalization of these axioms that does not require that their
variables be distinct.) There are no restrictions on the variables that
may occur in wff below.
| Axiom of Extensionality | ax-ext |
 |
| Axiom of Replacement | ax-rep |
 |
| Axiom of Power Sets | ax-pow |
|
| Axiom of Union | ax-un |
|
| Axiom of Regularity | ax-reg |
|
| Axiom of Infinity | ax-inf |
|
| Axiom of Choice | ax-ac |
   |
There you have it, the axioms for (essentially) all of mathematics! Wonder at them and stare at them in awe. If you keep a copy in your wallet, you will carry with you the encoding for all theorems ever proved and that ever will be proved, from the most mundane to the most profound.
Note. Books sometimes make statements like "(essentially) all of mathematics can be derived from the ZFC axioms." This should not be taken literally—there's not much you can do with those 7 axioms by themselves! Implicitly, the authors mean the ZFC axioms in addition to the axioms and rules of propositional and predicate calculus, which total 21 axioms and 2 rules in our system. Together these constitute what is called "ZFC set theory."
The Tarski-Grothendieck Axiom Above we qualified the phrase "all of mathematics" with "essentially." The main important missing piece is the ability to do category theory, which requires huge sets (inaccessible cardinals) larger than those postulated by the ZFC axioms. The Tarski-Grothendieck Axiom postulates the existence of such sets. We have included it in a separate table below for two reasons: first, it is not normally considered to be part of ZFC set theory, and second, unlike the ZFC axioms, it is not "elementary," in that the known forms of it are very long when expanded to set theory primitives. Below we show it compacted with definitions. Theorem grothprim shows you what it looks like when the definitions are expanded into the primitives used by the other axioms. The Tarski-Grothendieck axiom can be viewed as a very strong replacement of the Axiom of Infinity and implies both that axiom (shown by theorem grothomex) and the Axiom of Choice (whose proof by Tarski, "On well-ordered subsets of any set [external]", Fundamenta Mathematicae 32:176-183 (1939), still needs to be formalized—any volunteers? See also Bob Solovay's 29-Mar-2008 note on AC and strongly inaccessible cardinals [external] - he points out that the mere existence of strongly inaccessible cardinals doesn't imply AC, but rather the particular form of the Tarski-Grothendieck axiom stating their existence). It also implies the Axiom of Power Sets, as mentioned in Solovay's note (see theorem grothpw).
| The Tarski-Grothendieck Axiom | ax-groth |
  |
What else is missing from our axioms? Gödel showed that no finite set of axioms or axiom schemes can completely describe any consistent theory strong enough to include arithmetic. But practically speaking, the ones above are the accepted foundation that almost all mathematicians explicitly or implicitly base their work on.
Set theorists often study the consequences of additional axioms that assert, for example, the existence of larger and larger infinities beyond those postulated by ZFC or even the Tarski-Grothendieck Axiom, to the point of flirting with inconsistency (although Gödel also showed that we can never know whether even the ZFC axioms are consistent). While this work is certainly profound and important, these axioms are not ordinarily used outside of set theory.
Listed here are some examples of starting points for your journey through the maze. You should study some simple proofs from propositional calculus until you get the hang of it. Then try some predicate calculus and finally set theory. The Theorem List shows the complete set of theorems in the database. You may also find the Bibliographic Cross-Reference useful.
| Propositional calculus Predicate calculus Set theory | Set theory (cont.) Real and complex numbers (27 postulates) |
The complete proof of a theorem all the way back to axioms can be
thought of as a tree of subtheorems, with the steps in each proof
branching back to earlier subtheorems, until axioms are ultimately
reached at the tips of the branches. An interesting exercise is,
starting from a theorem, to try to find the longest path back to an
axiom. Trivia Question: What is the longest path for the theorem
2 + 2 = 4?
Trivia Answer: A longest path back to an axiom from 2 + 2 = 4 is 150 layers deep! By following it you will encounter a broad range of interesting and important set theory results along the way. You can follow them by drilling down this path. Or you can start at the bottom and work your way up, watching mathematics unfold from its axioms.
2p2e4 (2+2=4) <- 2cn <- 2re <- 1re <- ine0 <- mul01i <- subidi <- negsubi <- negidi <- negid <- pncan3 <- subadd <- subaddi <- negeui <- addcan <- addcani <- cnegexi <- cnegex <- axrnegex <- negexsr <- pn0sr <- distrsr <- dmaddsr <- addclsr <- addsrpr <- enrer <- addcanpr <- ltapr <- ltaprlem <- ltexpri <- ltexprlem7 <- ltaddpr <- addclpr <- addclprlem2 <- addclprlem1 <- ltrpq <- recclpq <- recidpq <- recmulpq <- mulcompq <- dmmulpq <- mulclpq <- mulpipq <- enqer <- mulasspi <- nnmass <- omass <- odi <- om00el <- om00 <- omword1 <- omwordi <- omword <- omord2 <- omordi <- oaword1 <- oaword <- oacan <- oaord <- oaordi <- oalim <- rdglim2a <- rdglim2 <- rdglim <- rdglimi <- rdgfnon <- tfr1 <- tfrlem13 <- tfrlem12 <- tfrlem11 <- tfrlem9 <- tfrlem7 <- tfrlem5 <- tfrlem2 <- tfrlem1 <- tfis2 <- tfis2f <- tfis <- tfi <- onss <- ordsson <- ordeleqon <- onprc <- ordon <- ordtri3or <- ordsseleq <- ordelssne <- tz7.7 <- tz7.5 <- wefrc <- epfrc <- epel <- epelc <- brab <- brabg <- opelopabg <- copsex2g <- copsexg <- eqvinop <- opth <- opth1 <- opi1 <- snex <- snprc <- neq0 <- n0 <- n0f <- noel <- dfnul2 <- eldif <- elab2g <- elabg <- elabgf <- vtoclgf <- hbeleq <- hbel <- hbeq <- hblem <- eleq1 <- eqeq2 <- eqeq1 <- bibi1d <- bibi2d <- imbi1d <- imbi2d <- pm5.74d <- pm5.74 <- anim12d <- prth <- imp4b <- imp4a <- impexp <- imbi1i <- impbii <- bi3 <- expi <- expt <- pm3.2im <- con2d <- con2 <- notnot2 <- pm2.18 <- pm2.43i <- pm2.43 <- pm2.27 <- id <- mpd <- a2i <- ax-2
The list above was produced by typing the commands "read set.mm" then "show trace_back 2p2e4 /essential /count_steps" in the Metamath program. By the way, the complete proof of 2 + 2 = 4 involves 2,452 subtheorems including the 150 above. (The command "show trace_back 2p2e4 /essential" will list them.) These have a total of 25,933 steps — this is how many steps you would have to examine if you wanted to verify the proof by hand in complete detail all the way back to the axioms.
We selected the theorem 2 + 2 = 4 for this example rather than 1 + 1 = 2 because the latter is essentially the definition we chose for 2 and thus has a trivial proof, 1p1e2 (shown primarily to support a lame attempt at humor, with apologies to frequent contributor Mel O'Cat). In Principia Mathematica, 1 and 2 are cardinal numbers, so its proof of 1 + 1 = 2 is different: see theorems pm54.43 and pm110.643 for a translation of its theorems into modern notation.
One of the reasons that the proof of 2 + 2 = 4 is so long is that 2 and 4 are complex numbers—i.e. we are really proving (2+0i) + (2+0i) = (4+0i)—and these have a complicated construction (see the Axioms for Complex Numbers) but provide the most flexibility for the arithmetic in our set.mm database. In terms of textbook pages, the construction formalizes perhaps 70 pages from Takeuti and Zaring's detailed set theory book (and its first-order logic prerequisite) to obtain ordinal arithmetic, plus essentially all of Landau's 136-page Foundations of Analysis.
In advocating his system, Tarski wrote, "The relatively complicated character of [free variables and proper substitution] is a source of certain inconveniences of both practical and theoretical nature; this is clearly experienced both in teaching an elementary course of mathematical logic and in formalizing the syntax of predicate logic for some theoretical purposes" [Tarski, p. 61].
Tarski's system was designed for proving specific theorems rather than more general theorem schemes (which we will define below). However, theorem schemes are much more efficient than specific theorems for building a body of mathematical knowledge, since they can be reused with different instances as needed. While Tarski does derive theorem schemes from his axioms, their proofs require concepts that are "outside" of the system, such as induction on formula length. The verification of such proofs is difficult to automate in a proof verifier. (Specifically, Tarski treats the formulas of his system as set-theoretical objects. In order to verify the proofs of his theorem schemes, a proof verifier would need a significant amount of set theory built into it.)
The Metamath axiom system (system S3' in Remark 9.6 of [Megill], shown as axioms ax-1 through ax-17 above, which we will call axiom schemes in this section) reformulates Tarski's system to eliminate this difficulty. The modified axiom schemes endow it with a nice property called metalogical completeness (defined in Remark 9.6 of [Megill]). As a result, we can prove any theorem scheme expressable in the "simple metalogic" of Tarski's system by using only Metamath's direct substitution rule applied to the axiom system (and no other metalogical or set-theoretical notions "outside" of the system). Simple metalogic consists of schemes containing wff metavariables (with no arguments) and/or set (also called "individual") metavariables, accompanied by optional provisos each stating that two specified set metavariables must be distinct or that a specified set metavariable may not occur in a specified wff metavariable. Metamath's logic and set theory axiom schemes are examples of simple metalogic.
[See also Question 15 on the Metamath Solitaire page. Note that when we say "Metamath's axioms" on this web page, we usually mean the axiom schemes in the set.mm database file, which was used to create the Metamath Proof Explorer web pages. Other axiom systems are also possible with the Metamath language and program.]
Axioms vs. axiom schemes An important thing to keep in mind is that Metamath's "axioms" and "theorems" are not the actual axioms and theorems of first-order logic (i.e. the traditional predicate calculus of textbooks) but instead should be interpreted as schemes, or recipes, for generating those axioms and theorems. In particular, the (red) "set variables" in Metamath's axioms are not the individual variables of the actual axioms; instead, they are metavariables ranging over these individual variables (which in turn range over the individuals in the logic's universe of discourse—in our case of set theory, the universe of discourse is the collection of all sets). This can cause and has caused confusion, particularly because of the superficial resemblance between the two. For clarity, we will refer to Metamath's axioms as axiom schemes in this section and whenever we discuss Metamath in the context of first-order logic.
The actual language of first-order logic consists of starting
(or primitive or atomic) wffs (well-formed formulas)
constructed from actual individual
variables v1, v2, v3,.... connected by = and (such as "v2 = v4"
and "v3 v2"), which are then used to build up larger
wffs with the connectives , , and (such as "
v2 = v4 v6
v3 v2"). That is the complete language
needed to express all of set theory and thus essentially all of
mathematics. That's it; there is nothing else! There are no other
variable types in the actual language; in particular there are no
variables representing wffs. Each of our axiom schemes corresponds to
(generates) an infinite set of such actual formulas that match its
pattern. For example, "(v1 v3 v2 v3 v2)" is an
actual axiom since it matches axiom scheme ax-4,
" ," when we substitute "v1" for "" and " v3 v2" for "."
Even in propositional calculus, the "axioms" are really axiom
schemes. Although logic textbooks may have "propositional variables"
that are manipulated directly and even treated as primitive for
convenience (or certain theoretical purposes), they are really wff
metavariables when used as part of the
foundations for mathematics. An actual axiom of propositional calculus
has no propositional or wff variables but only the kinds of actual wffs we just
described. Each axiom scheme is a template corresponding to an infinite
number of actual axioms.
For example, neither the general form of
ax-1
"
"
nor the more restrictive substitution instance
"
"
is an actual axiom—both are schemes ranging over an infinite
number of actual axioms (fewer of them in the second case,
of course). An example of an actual propositional calculus
axiom is the instance
"v3 = v5
v6 v1 v4
v3 = v5".
Substitution
instances of schemes
In Metamath, by default there are no restrictions on substitutions
that may be made into a scheme, provided we honor the
metavariable types (wff variable
or set variable). This is called direct substitution,
in constrast to a more complicated "proper substitution" used
in textbook predicate calculus.
Consider, for example,
axiom scheme ax-9,
which can be abbreviated as " " (theorem scheme a9e), "there exists () an such that equals ." In traditional predicate calculus, a variable
in the quantifier's "scope"
is considered "bound," otherwise it is "free," and
substitutions must follow careful
rules taking into account of whether the variable is bound or
free at a given position.
In the Metamath language, is merely a 2-place prefix
connective or "operation" that evaluates to a wff,
taking a set variable as its first argument and a wff
as its second, with no built-in concept of "bound" or "free". In a9e, we place no restriction on what actual
variables may be substituted for "bound" metavariable and "free" metavariable . We can even
substitute them with the same variable, seemingly
at odds with the traditional rule that free and bound variables must
always be distinguished.
(When we
do need to prohibit certain substitutions, they are done with
"distinct variable" provisos we describe below, that apply to a
theorem as a whole without consideration of whether a variable's occurrence
is free or bound. This makes all substitutions very simple.)
The expression " " is just a recipe for generating an
infinite number of actual axioms. In an actual axiom such as "v3 v3 =
v2," symbols v2 and v3 always represent distinct variables by
definition, because they have different names.
Another
axiom that results from the recipe
is "v3 v3 = v3," which has a different meaning but is still
perfectly sound.
On the other hand,
when working with the actual axioms there is no rule that allows
us to infer "v3 v3 = v3"
from "v3 v3 = v2": they are independent axioms generated by
the scheme. In the actual logic, the only rules of inference are the
(infinite) specific instances of the modus
ponens and generalization
schemes—for example, from "v3
v3 = v2" we can infer "v6v3
v3 = v2" by generalization—and there is no
substitution rule built in as a primitive notion.
The proper substitution rule of traditional predicate calculus is a by-product of the axiom schemes that were chosen, and the rule is necessary to ensure that these schemes generate only correct actual axioms. Metamath uses different axiom schemes that do not require proper substitution but generate exactly the same actual axioms as traditional predicate calculus. (A price we pay with Metamath is a larger number of axiom schemes.) In the actual axioms, there are no primitive concepts of "free", "bound", "distinct", or even "substitution"—these are all metamathematical notions at the scheme level.
See also technical notes 2 and 3 below.
Metamath is a metalanguage that describes first-order logic ...and is not itself the language of first-order logic. But the "meta" aspect runs deeper than just the fact that its axioms represent schemes.
Traditional presentations of first-order logic also use schemes to describe the axioms. However, a substitution instance of one of their axiom schemes is intended to be one specific axiom of the actual logic. Formal proofs are defined so that they involve only actual axioms, to result in actual theorems. Often textbooks will derive theorem schemes to obtain more generally useful results, but such derivations are understood to be outside of the logic itself and may use metalogical techniques such as induction on formula length that are not part of the axiom system.
Metamath's key and very important difference is that an application
of its substitution rule always creates a new scheme from an old
one. Metamath works only with schemes and never with
actual axioms or theorems.
For example, the schemes
"
" and
"
" are two
substitution instances that we can infer from the scheme
"
." These substitution instances
are new schemes in their own right, into which we can make further
substitutions to specialize them further if we wish.
The set and wff variables of the Metamath language are one level
up, or "meta," from the point of view of the logic that it describes.
(Hence the name Metamath, meaning "metavariable math.") Each
"theorem" on our proof pages is a theorem scheme (metatheorem) that is a
recipe for generating an infinite number of actual theorems.
In fact,
the Metamath language cannot even express specific, actual theorems such
as "v1 v2 v1 v2." We would have to do that outside
of the Metamath system. Ordinarily this is unnecessary; even logic
textbooks work informally with theorem schemes after they explain how
the formal system is constructed. Metamath formalizes the process for
working directly with schemes and makes the necessary metalogic (its
substitution rule) part of the axiom system itself, so that no
techniques outside of the axiom system are needed to derive its theorem
schemes.
Distinct
variables Sometimes we must place
restrictions on the formulas generated by a scheme in order to ensure
their soundness, and we use distinct variable
restrictions for this purpose. For example, the theorem scheme dtru, , has the restriction that metavariables
and cannot be substituted
with the same actual variable, otherwise we could end up with the
nonsense substitution instance "v1 v1 = v1"
which would mean "it is not true that every object v1 equals itself." The substitution rule of
Metamath ensures that distinct variable restrictions "propagate" from
axiom schemes having such restrictions into theorem schemes using those
axioms.
Note that distinct variable restrictions are
metalogical conditions imposed on certain axiom and theorem
schemes. They have no role in the actual logic, where two actual
variables with different names are distinct by definition—simply
because they have different names, which is what "distinct" means. Thus
in an actual theorem generated by dtru, such as
"v1 v1 =
v2," it would be redundant (and
meaningless) to require that v1
and v2 be distinct. There is no
danger of inferring from this the falsehood "v1
v1 = v1", because there is no substitution rule in
the actual language that lets us do so.
As we
mentioned (three paragraphs earlier), the Metamath language itself cannot
express actual theorems such as "v1 v1 = v2." Instead, the distinct variable
restriction on dtru is enforced at the level of
theorem schemes. In this example, we are not allowed to substitute the
same metavariable, say , for both and
whenever we reference dtru in a proof
step.
Technical notes 1. For anyone interested, here are some technical notes on the [Megill] paper. The claim in Remark 9.6, "C14' is omitted from S3' because it can be proved from the others using only simple metalogic," is proved in theorem ax15. Axiom C16' is also redundant—see theorem ax16, whose proof was discovered in 2006 and not known at the time of the paper. The somewhat bizarre axiom C10' was shown to be equivalent to the simpler ax-9 after the paper was submitted; see theorem ax9. In the proof of the metalogical completeness theorem, Theorem 9.7, some details that are stated without proof as "provable in S3' with simple metalogic," but which are nonetheless are tricky, are proved by theorems sbequ, sbcom2, and sbid2v.
2. Some people dislike the fact that ax-9 actually represents two conceptually different
axiom schemes, one where and
are always distinct variables (one bound, one free) and another which
really means " ." Raph Levien calls this "bundling" (see
"Principal
instances of metatheorems" [external]). To a certain extent, the
current choice of axiom schemes is a matter of preference, partly to
reduce the number of schemes, partly to postpone the introduction of distinct variables, and partly to study systems with no distinct variable restrictions.
An interesting open problem is to devise an alternate axiomatization
that presents non-bundled axiom schemes except possibly ones
specifically designed for that purpose. If we want the system to be
metalogically complete, we must be able to derive the bundled versions
of the axiom schemes. For example, if we don't use ax-9 as an axiom scheme, then at least we should be
able to prove it as a theorem scheme from whatever other axiom schemes
are chosen to replace it.
3. Tarski used the axiom scheme " " in
one of his systems without requiring that and be distinct variables (see [KalishMontague], footnote on p. 81).
In other words, he bundled it like we do. On the
other hand, he required that and be distinct in this scheme of his system S2 mentioned above,
since the scheme " " could be derived as a metatheorem and was
therefore redundant. Tarski considered it better to include the
distinct variable condition since it "simplified" the system by
generating fewer actual axioms—i.e. it "weakened" the
scheme—even though it made the statement of the
scheme more complex. However, Tarski was not concerned with
metalogical completeness, so his goals were different from ours.
4. An interesting feature of Metamath's axiom system is that it is finitely axiomatized in the following strong sense: at any point in a proof, there are only finitely many axiom schemes in the system from which the next step can be chosen, and whenever the choice is valid i.e. unifies, there is a unique most general theorem that that results. This fact is exploited and illustrated in the Metamath Solitaire applet: you are presented with exactly all possible allowed (unifiable) choices, and when you choose one you are shown the most general theorem that results. This is in sharp contrast to traditional predicate calculus (and even Tarski's system), where we must choose from an infinite number of substitution possibilities in order to apply an axiom. In particular, ZFC set theory also becomes finitely axiomatized in this strong sense, because the Replacement Scheme of ZFC becomes a single "axiom" (or more precisely, a single scheme expressable in simple metalogic) under Metamath's formalization. (Note that the terminology "finitely axiomatized" is also used in the literature in a different way, to mean a theory with finitely many actual axioms on top of predicate calculus, without counting the infinite number of axioms of predicate calculus itself. For example, under that meaning, ZFC set theory is not finitely axiomatized because its Axiom of Replacement is a scheme describing an infinite number of axioms.)
5. Interestingly, Raph Levien has shown (see Item 16 on the Workshop Miscellany page) that in the
actual logic, if we are given "v3
v3 = v3" it is impossible to infer from it, in the
absence of scheme ax-9, even the obvious
equivalent "v4 v4 = v4." This illustrates
that bound variable renaming (related to substitution)
is not part of the axioms themselves
but only of the metamathematics that describes them.
If you want to acquire a practical working ability in logic, it is a good idea to become familiar with the traditional textbook axioms. Their built-in concepts of free and bound variables and proper substitution are a little more complex than Metamath's simple substitution rule, but they allow you to work at a somewhat higher level and are better suited than Metamath's for humans to understand intuitively. In fact, many of the proofs here were sketched out informally using traditional methods before being formalized with Metamath's axioms.
For classical propositional calculus, the traditional axiom and rule schemes are exactly the same as Metamath's axioms and rule (interpreted as schemes), namely ax-1, ax-2, ax-3, and rule ax-mp. The additional axiom and rule schemes for traditional predicate calculus with equality are the following. The first three are the axiom and rule schemes for traditional predicate calculus, and the last two are the axiom schemes for the traditional theory of equality. We link to the approximately equivalent theorem schemes in the Metamath formalization.
| stdpc4 | , provided that is free for in |
| stdpc5 | , provided that is not free in |
| ax-gen | |
| stdpc6 |
|
| stdpc7 | 
, provided that is free for in
|
Three of these axiom schemes have informal English-language conditions on them. These conditions are somewhat awkward to formalize, but they are not hard to grasp intuitively. You can look them up in any elementary logic book. They are also explained in Hirst and Hirst's A Primer for Logic and Proof [external] (PDF, 0.5MB); Section 2.4 (pp. 36-37; add 6 for the PDF page number) defines "free variable," and Section 2.11 (pp. 48-51) defines "free for." See pp. 15, 51, & 64 for the propositional calculus, predicate calculus, and equality axioms respectively.
Stefan Bilaniuk's A Problem Course in Mathematical Logic [external], another free on-line book, provides a more extensive study of logic.
Even though the traditional axiom system looks different from Metamath's, the two axiom systems generate exactly the same set of actual theorems. (Read about schemes in the previous section to understand what "actual" means.) Specifically, all of Metamath's axiom schemes ax-4 through ax-17 can be proved as theorem schemes of the traditional system. Conversely, every instance of the traditional axiom schemes is an instance of a theorem scheme provable from Metamath's axiom schemes.
Although in some sense the traditional axiom schemes are more compact than Metamath's ax-4 through ax-17, their goal is simply to provide recipes for generating actual axioms, from which we then prove actual theorems. Theorem schemes can also be proved from the traditional axiom schemes, but their proofs use informal metalogical techniques that are not part of the axiom system. In Metamath, on the other hand, we deal only with schemes and never with actual axioms, and its formalization is designed to let us prove directly all possible theorem schemes of a certain kind (specifically, all possible schemes expressible in simple metalogic).
Metamath's system does not have the traditional system's
(metalogical) notions of
"not free in" and "free for" built in, so the traditional system's
schemes cannot be translated exactly to schemes in the
Metamath language. However,
we can emulate these notions (in either system, actually, since every
scheme in Metamath's system is a scheme of the traditional system) with
conventions that are based on a formula's logical properties
(rather than its structure, as is the case with the traditional
axioms). To say that " is effectively not free in ," we can use the hypothesis . This hypothesis holds in all
cases where is
not free in in the traditional system (and in a few other cases as well,
which is why we say "effectively"—for example, the wff will satisfy the hypothesis, as shown by
theorem hbequid, even though is technically free
in it).
We can emulate "free for" through the use of our definition of proper
substitution df-sb.
Both our system and the traditional system are called Hilbert-style systems. Another very powerful approach, called a Gentzen-style system, embeds the deduction (meta)theorem into its axiom system, but we do not discuss it here. Frédéric Liné has been developing a Gentzen-style system called natural deduction [external] in the Metamath language.
,
,
,
These three groups (in this example 3 pairs) have the following meanings, respectively, as side conditions of the theorem scheme or axiom scheme shown above them:
and
may not be substituted with the same set variable,
may not appear in the wff expression substituted for
,
and
may not appear in the class expression substituted for
.
and
are distinct,
does not occur in
,
and
does not occur in
.[Actually, there is only one rule in the
Metamath language: the two expressions that are substituted for the two
variables in a distinct variable pair must not have any variables in
common. This is why a distinct variable pair is officially called a
"disjoint variable pair" in the Metamath specification. We present the
rule as three separate cases above for clarity. In the set theory
database file, set.mm, we adopt the convention that at least one set
variable always appears in a distinct variable pair, so these are the
only cases you will see. Under this convention, a distinct variable
pair such as "," will never occur, even though technically it is not
illegal.]
Note that
,
,
Finally, if more than two variables appear in a group, this is an abbreviated way of saying that the restrictions apply to all possible pairs in the group. So,
,,
,
,
,
When an axiom or theorem with distinct variable restrictions is
referenced in a proof step, the variables in the resulting proof step
will "inherit" them. For example, look at step 1 of the proof of cleljust, which has a substitution instance of
ax-17. As you can see, ax-17 requires the distinct variable pair ,, and the proof
step substitutes
for and for . So, this means that cannot be among those variables
that are contained in the wff
The distinct
variable requirement of ax-17 thus imposes the
requirement that theorem cleljust must have
as provisos the two distinct variable pairs , and ,,
otherwise the proof verifier will tell us that this substitution
instance is invalid. And indeed, you can see this exact requirement in
the "Distinct variable groups" list on the cleljust page.
You can see a dynamic example in the Metamath Solitaire applet by
entering the first proof of
and watching the transformation of the
distinct variable requirement that appears at the tenth step (ax-16).
Constants are considered distinct from all variables and never appear (nor are allowed to appear) in a distinct variable group. See the comment for isset.
In the Metamath language, distinct variable requirements are specified with the $d statement. Each theorem must be accompanied by those $d statements that it needs to satisfy the distinct variable requirements propagated forward (inherited) from the axioms and earlier theorems referenced in its proof. To get a concrete feel for distinct variable restrictions, we can temporarily comment out the "$d x z" condition for theorem cleljust in the database file set.mm. When we try to verify the proof with the Metamath program, the resulting error message will read as follows. (Note that step 25 is the same as step 1 on the web page; steps 1-24 are syntax building steps that can be seen with "show proof cleljust /all".)
Read this section
carefully to learn how to follow a Metamath proof.
MM> verify proof cleljust
cleljust
?Error at statement 5305, label "cleljust", type "$p":
wel vz ax-17 vz vx vy elequ1 equsex bicomi $.
^^^^^
There is a disjoint variable ($d) violation at proof step 25. Assertion
"ax-17" requires that variables "ph" and "x" be disjoint. But "ph" was
substituted with "x e. y" and "x" was substituted with "z".
Variables "x" and "z" do not have a disjoint variable requirement in the
assertion being proved, "cleljust".
This error message can be used to determine any missing $d
statements during proof development. Alternately, the
mmj2 program will compute the necessary
$d's automatically.
Note
1 Sometimes new or "dummy" variables are
used in a proof but do not occur in the theorem being proved. Usually
they must be distinct from other variables, but on the web pages we
always omit them from the "Distinct variable group(s)" list for
brevity and to make the display more pleasant to read. You can
see them mentioned explicitly (as is required by the Metamath language
spec) in $d statements in the database file set.mm. An example is the
variable that
must be distinct from the others in the proof of ax15. By the way, the "Distinct variable group(s)"
that are shown are exactly those that need to be satisfied by any
proof that references the theorem.
(An issue that is brought up occasionally is whether the Metamath language itself should be changed so that $d statements on dummy variables are implicit. This is partly a matter of taste, but so far I have felt it better to require explicit $d statements for them. There are good arguments both ways, but to me, philosophically it makes the language more transparent, if more tedious. Also, if they are made implicit, we could not force an error message to explain why they are needed. And importantly, existing databases are compatible with either method, whereas if we made $d statements optional for dummy variables, it would be hard to go back.)
Note
2 Textbooks often use the
notation () to
denote that variable may appear in the wff substituted for . Metamath doesn't have a
notation like this, but we can achieve the logical equivalent simply by
omitting the distinct variable group ,, as the example axsep
shows. Since this isn't obvious from the theorem itself, it is
important to pay attention to the distinct variable groups to detect
this intent. Often, as we do for axsep, we
will note the intent in the theorem's description.
In a sense, Metamath is opposite from the usual textbook convention: in Metamath, any variable may appear in a substitution instance of a wff by default; it is the exceptions that must be made explicit with distinct variable requirements. Keeping this in mind may make the comparison to logic textbooks a little easier.
Note
3 Distinct variable requirements are
sometimes confusing to Metamath newcomers. Unlike traditional predicate
calculus, Metamath does not confer a special status to a bound
variable (e.g. the quantifier variable in ); there is no built-in concept of its "scope." All
variables, whether free or bound, are subject to the same direct
substitution rule. Metamath's substitution rule does not treat a
variable after the quantifier symbol "" any differently from a variable after
any other constant connective such as "". The only thing that matters is that
the syntax is legal for the variable type, and that any distinct
variable requirements are satisfied. This may
take some getting used to by someone schooled in traditional "proper
substitution" (which involves analyzing the scopes of bound variables
and renaming them if necessary), even though it is
simpler than the traditional approach. Unless otherwise
specified by a distinct variable group, a quantified (or any other)
variable is by default not necessarily distinct from other
variables in the same expression, even those in the same scope. This is
opposite the usual implicit assumption in traditional mathematics. For
example, in many textbooks, it would be implicit that the two variables
in theorem scheme dtru must be distinct (since
one is bound and the other is free), but in Metamath this requirement
must be made explicit. (On the other hand, in an instance of dtru in
the actual logic, which Metamath cannot express directly, the two
variables are implicitly distinct by definition, as explained the "Distinct variables" subsection of Appendix 1 above.)
Another reason for confusion may be distinct variable requirements appear separately from the formula part of a theorem and are implicitly rather than directly referenced in proofs, possibly making the relationship between the two unclear to some people. However, there is no fundamental difference between a logical hypothesis ($e statement in the database) and a distinct variable requirement, in that a proof may be invalid unless it is present. It can be helpful to think of each axiom or theorem (and each step in a proof) as being an assertion of the form "L & D => C," where L is the (possibly empty) set of relevant $e statements, D is the (possibly empty) set of relevant $d statements, and C is the conclusion ($a statement for an axiom or $p statement for a theorem). Perhaps a better name for a distinct variable "requirement" (or "proviso," or "restriction," or "constraint," or "side condition") would be distinct variable "hypothesis."
A curiosity Two otherwise identical theorems with different distinct variable requirements can express very different mathematical facts. Compare, for example, dvdemo1 and dvdemo2.
The bottom line The Metamath language itself doesn't have a separate mechanism for introducing definitions and in particular ensuring their soundness. The only way to add a definition to a database is to introduce it as a new axiom. In the same way that an axiom system can be inconsistent, an unsound definition may lead to an inconsistency.
If you don't know what we mean by an unsound definition, here is a simple example. Suppose we modify df-2 to become the self-referential expression "2 = ( 1 + 2 )" instead of its present "2 = ( 1 + 1 )". From this, we can easily prove the contradiction 0 = 1. Therefore, this "definition" leads to inconsistency and is unsound. But since it is an axiomatic ($a) assertion in the database, the Metamath proof verifier is perfectly content to use it as a new fact and does not issue an error message.
Thus, the soundness of definitions must be verified independently of the Metamath proof verifier, either by hand or with through the use of a separate automated tool.
Raph Levien has written a program to translate Metamath's set.mm database into his Ghilbert [external] language. The Ghilbert proof verifier is designed to have a safe definition mechanism. For example, it will not allow us to introduce "2 = ( 1 + 2 )" as a definition. Although having to convert to Ghilbert is somewhat inconvenient, new definitions are typically added relatively infrequently compared to new theorems and proofs. Perhaps eventually a tool will be written to verify definitional soundness directly for the set.mm database. In the meantime, careful manual verification of new set theory definitions, introduced as explained below, is quite simple, and automated soundness verification should be needed only occasionally, for example when complete assurance is desired for a result that will be published.
Discussion The Metamath language provides a very simple and general framework for describing arbitrary formal systems. Intrinsically it "knows" nothing about logic or math; all it does is blindly assure us that we cannot prove anything not permitted by whatever formal system we have described to it. What we call an "axiom" is to Metamath merely a new pattern for combining symbols that we have told it is permissable. The same holds for what we call "definitions"—to Metamath, definitions merely extend the formal system with new patterns and are indistinguishable from axioms by the proof verifier.
For convenience, we usually make an artificial distinction by prefixing definition names with "df-". But every definition is assumed to have been metalogically justified outside of the Metamath formalism as being sound. A definition is sound provided (1) it is eliminable and (2) it does not strengthen the axiom system when it is eliminated from a theorem.
This method of introducing definitions as new axioms keeps the Metamath language simple and not tied to any specific formal system. A definition that is sound in one formal system may be unsound in another. For example, a recursive definition may not be eliminable in a system too weak to prove the necessary recursion theorem, and even when it is, its elimination can be quite complex (see e.g. the discussion of df-rdg).
One extreme viewpoint is to consider all definitions to be additional axioms, following logicians such as Leśniewski [C. Lejewski, "On implicational definitions," Studia Logica 8:189-208 (1958)].
Leśniewski regards definitions as theses of the system. In this respect they do not differ either from the axioms or from theorems, i. e. from the theses added to the system on the basis of the rule of substitution or the rule of detachment. Once definitions have been accepted as theses of the system, it becomes necessary to consider them as true propositions in the same sense in which axioms are true. [p. 190]This was roughly the original idea when Metamath was first designed. The concept of definitional soundness was considered outside of the scope of the proof verification engine, because it is intrinsically dependent on the strength of the axiom system. Instead, definitional soundness was expected to be verified independently, either by hand or by an automated tool customized for the particular logic system used by the database. (Such a tool might recognize the "df-" prefix as a keyword meaning "definition" and would impose constraints to guarantee that the definition is sound under the axiom system of that database.)
In the set theory database set.mm, we have adopted the conservative convention that most definitions, beyond the basics needed for a practical development of set theory, consist of a single new class constant symbol followed by an equal sign followed by a class expression built from earlier symbols, for example the definition of rational numbers df-q. Thus the definition is more or less a drop-in replacement that abbreviates a fixed, more complicated expression (with possible renaming of bound variables). The soundness of such definitions is simple to check by inspection: if (1) the left-hand constant symbol is new and doesn't appear in the right-hand side, (2) all variables are distinct (all of them appear in a single $d statement), and (3) we can prove (with a Metamath theorem, e.g. qjust for df-q) that the right-hand expression equals itself with all variables renamed, then the definition is sound. These steps could be automated for this restricted kind of definition, although currently they are not. But I strongly recommend this convention to anyone extending set.mm, so that any future tool will be able to verify such definitions automatically.
A non-mathematical (human) issue with a definition is whether it matches the generally understood meaning of a concept. For example, if we swapped the symbols 4 (df-4) and 5 (df-5) everywhere, all definitions would remain sound, but we could "prove" that ( 2 + 2 ) = 5. For this reason, all definitions still must be carefully scrutinized by a competent mathematician, and obviously there is no way to automate this inspection.
Automated definitional soundness checking will become more important if Metamath is ever used in a large-scale collaborative project. However, it is more likely that Ghilbert will be used for that purpose and that Metamath will continue to be used for smaller, self-contained projects such as set.mm. As they have in the past, these two projects can continue to "feed" each other with new theorems developed on their respective platforms.
The definition list (1.8MB) shows all of the definitions in the database. The web page for every proof lists all definitions that were used somewhere along its path back to the axioms, so that nothing is hidden from the user in this sense.
(Thanks to Raph Levien and Freek Wiedijk for discussions on this topic, and to Bob Solovay for manually proving the soundness of all of the basic set theory definitions in the set.mm database.)
You shouldn't expect to see immediately the relationship between them and the proof you are looking at—it is usually not obvious at all. This list of axioms was determined by scanning back through the proof tree until axioms were reached, and in fact required a considerable amount of CPU power. Mathematicians generally like to prove theorems using as few axioms as possible, which I also usually tried to do, so this list is often the minimum set needed for the proof you are seeing.
For example, we see that the Axiom of Choice ax-ac was not needed to prove 2 + 2 = 4 2p2e4, but we did need the Axiom of Infinity ax-inf2. Why did we need Infinity? Well, our number 2 is a real number, and the Axiom of Infinity is needed to prove that any real number exists. (And why is this? Very informally, we can think of an arbitrary real number as having an infinite list of digits after the decimal point, and we need an axiom that tells us that such infinite lists exist before we can manipulate them with set variables.) But the place where Infinity is used is buried deep inside the proof tree—you have to drill down through 49 layers of proofs to find it. If you want to see its path all the way to 2 + 2 = 4, locate mulpipq in the 2 + 2 = 4 Trivia path list above. Then branch off from that path and follow this one back to the Axiom of Infinity: mulpipq <- enqex <- niex <- omex <- zfinf <- ax-inf2.
To find out the path above, in the Metamath program I saved the outputs of "show usage ax-inf2 /recursive" and "show trace_back 2p2e4" into two lists then determined their common members with some text processing.
".
Here
""
is a
class that normally is a function,
""
a class that normally is the
argument of the function, and
""
is the class that results when the function is evaluated at the
argument. (The result, however, is well-defined for any classes
whatsoever substituted for the class variables and ends up evaluating
to the empty set when it is not meaningful—see for example theorem ndmfv.)
Textbooks often use the familiar notation ""
for the value of a function. Outside of context, this notation is
ambiguous: it could also mean the expression that results when is substituted into
the expression that represents. Our left-apostrophe notation, invented by Peano,
is often used by set theorists and has the advantage for us that it is
unambiguous and independent of context.
For special functions such as square root, textbooks indicate
function values with an assortment of two-dimensional graphical
structures and syntactical idioms that may be ambiguous outside of
context. Our versions may seem unfamiliar because we are constrained to
a linear language and we need context-independent, unambiguous notation.
We also prefer a single notation for function value to be able to reuse
our rich collection of theorems about function values. For example, in
the square root theorem sqrthi, the square root
symbol "
" is a function i.e. a class (csqr), and we display the square root of 2 as
"
".
Two other examples
are the real part of an complex number
A,
where we use
"
"
instead of
"",
and the conjugate of a complex number,
where we use
"
"
instead of
"
" (or sometimes with an overbar),
both of which you can see in theorem
cjval.
Another example is the factorial function, which we express as
"
"
instead of
"" in
facnn2.
In the conventional textbook notation,
these four examples use four different positional relationships to
indicate one concept (the value of a function), but I decided to use a
single syntax for all four to make the development of proofs simpler.
There is an exception to the above convention: the
unary minus function
df-neg is so common I decided to
create a special syntax for it. So, the negative of a complex number is
represented as the visually more familiar "
" rather than the more tedious
"". A drawback is that we have to prove separately
certain
theorems such as the equality theorem negeq
instead of being able to reuse the general-purpose fveq2.
Another very important exception is the notation for an operation
value, which is the function value of an ordered pair as defined by
df-opr. It is so commonly used that we
adopted the convenient and familiar notation of three juxtaposed class
expressions surrounded by parentheses, such as "( 3 + 2 )". While this
may appear to be syntactically ambiguous with such expressions as the
union of two classes (cun), " 
", the
difference is that operation value notation requires that the center
symbol be a class expression: "+" is a class expression (caddc) but a stand-alone "" is not. (We do not define the
union of two classes as an operation because it must work with proper
classes as arguments—not to mention that the operation value
definition ultimately depends on it anyway.)
In the set.mm database, there are 8 other axiom schemes of predicate calculus (ax-4, ax-5o, ax-6o, ax-9o, ax-10o, ax-11o, ax-15, and ax-16) that are not included in our "official" list of 11 predicate calculus axiom schemes (and 1 rule) above, because they can be derived as theorems from the official ones. As their names suggest, we used to include them, but they were removed from the official list over time when they were discovered to be redundant or were replaced by new versions. However, we have kept them in the database, because from the set consisting of these 8 axiom schemes plus the "official" ones, several subsystems can be of interest for certain studies. For brevity, "axiom" always means "axiom scheme" in the table below. In the table, we assume that all 19 axiom schemes and 1 rule (22 axioms and 2 rules if we include propositional calculus) are present, except for the ones listed in the "Omit axioms" column.
| Omit axioms | Discussion of resulting subsystem |
|---|---|
| ax-4, ax-5o, ax-6o, ax-9o, ax-10o, ax-11o, ax-15, and ax-16 | As mentioned above, the 8 omitted
axioms can be derived from the others (see theorems ax4, ax5o, ax6o, ax9o, ax10o, ax11o, ax15, ax16). This system
is metalogically complete and is the one we
ordinarily use. It is equivalent to system S3' in Remark 9.6 of [Megill].
Even though we reference these 8 redundant axioms in proofs for better granularity, each of them is proved from the others in the corresponding theorem immediately before each redundant axiom is introduced, so if desired all references to them can be eliminated easily. |
| ax-17 | This system is logically complete (see comments in ax-17), but we lose the powerful metalogic afforded by the concept of "a variable not occurring in a wff". It is conjectured that ax-4, ax-11o, and ax-15 (and possibly other otherwise redundant ones as well) cannot be derived from the others in this system. Proofs in any system omitting ax-17 tend to be long. |
| ax-11, ax-11o | This system is logically complete. Any specific substitution instance of the omitted axioms that contains no wff metavariables can be derived from from the axioms of this subsystem (see theorems ax11eq, ax11el, ax11indn, ax11indi, and ax11inda), but, as Juha Arpiainen proved, the omitted axioms themselves cannot be derived (see comments in ax-11). In other words, this system is logically complete but is not metalogically complete. |
| ax-10, ax-11, ax-11o, ax-16, ax-17 |
System with no distinct variables. This system has no distinct
variable contraints, making the concept of substitution as simple as it
can possibly be and also significantly simplifying the algorithm for
verifying proofs. It is
equivalent to system S2 in Section 4 of [Megill]. The primary drawback of this system is
that for it to be considered complete, we must ignore antecedents called
"distinctors" that stand in for
what would be distinct variable constraints (see the linked discussion).
We can optionally include ax-11o or ax-11 for a somewhat more powerful metalogic, since these also involve no distinct variable restrictions (although without them we can still derive any instance of them not containing wff metavariables). Proofs in this system tend to be long. |
| ax-11o, ax-16, ax-17 | It is conjectured that ax-11o cannot be derived from the axioms of this subsystem. See Item 9b on the Workshop Miscellany page. |
| ax-11, ax-16, ax-17 | It is known that ax-11 can be derived from the axioms of this subsystem (see theorem ax11). |
| ax-10o and ax-11 | It is conjectured that ax-10o cannot be derived from the axioms of this subsystem. |
| Omit all predicate calculus axioms except ax-4, ax-5, ax-6, ax-7, and ax-gen |
The subsystem ax-1 through ax-7, ax-mp, and ax-gen, i.e. the axioms not involving equality,
is weaker than traditional predicate calculus without equality (i.e.
that omits the equality axioms labeled stdpc6 and stdpc7 in the table in
the traditional predicate calculus section).
The reason is that traditional predicate calculus incorporates proper
substitution as part of its metalogic, whereas in our system proper
substitution is accomplished directly by the logic itself through our
more complex axioms ax-8 through ax-17. In our system, substitution and equality
are intimately tied in with each other. This "pure" subsystem in effect
represents the fragment of logic that remains when equality, proper
substitution, and the concept of distinct variables are completely
stripped out. Interestingly, if we map "for all" to "necessity" and
omit ax-7 from the "pure" subsystem, the result
is exactly the modal logic system known as S5 (thanks to Bob Meyer for
pointing this out). See also Item 12 on the Workshop Miscellany page.
Optionally, we can replace ax-5 and ax-6 with ax-5o and ax-6o (provided we replace them both) to obtain an equivalent subsystem. Theorems ax5, ax6, ax5o, and ax6o prove the equivalence. In this subsystem, ax467 can replace ax-4, ax-6o, and ax-7. |
For propositional and predicate calculus, Margaris is now available in an inexpensive Dover edition and is reasonably readable for beginners, once you get used to the archaic dot notation used in place of parentheses. Our 19.x series of theorems, such as 19.35, corresponds to Margaris' handy predicate calculus table on pp. 89-90. Hirst and Hirst's on-line A Primer for Logic and Proof, mentioned above, uses modern notation and is also highly recommended.
For set theory, Quine is wonderfully written and a pleasure to read. The first part on virtual classes (pp. 15-21) is a must-read if you want to understand our purple class variables (which in Quine are Greek letters). Quine also uses the archaic dot notation, but this is really a very minor hurdle, especially since you can compare the Metamath versions of many of the theorems. Takeuti and Zaring is the set theory reference we follow most closely, including most of our notation, and its rigor makes it straightforward to formalize proofs; but some people find it a dry and technical read, and it is also out of print. Suppes, which is available in a Dover edition, goes to extremes to avoid virtual classes, leading to bizarre theorems like "the set of all sets is empty" (Theorem 50, p. 35); nonetheless, it provides a gentle introduction that we reference surprisingly frequently.
Some closely followed texts in the Metamath Proof Explorer are listed below. I am not specifically endorsing them but just indicating which books and papers I consulted frequently while building the database.
Browsing with the Unicode font By default, the Metamath Proof Explorer uses GIF images for all math symbols. Depending on your computer, browser, and Internet connection, this may result in slow rendering of large proofs, such as projlem7 (870K), which is the largest in the database. On each page with a proof, at the top there is a link to switch to the Unicode font version. You will stay in the Unicode font directory (you will see "mpeuni" instead of "mpegif" in the URL) until you switch back to the GIF version on a page with a proof.
Unfortunately, Internet Explorer versions 6 and 7 do not implement some of the standard Unicode math symbols, which is why I chose GIF images as the default. The missing symbols are displayed as blank rectangular boxes, making the page unreadable. The free Firefox and Mozilla [external] browsers implement them correctly. Safari on MacOS X (10.3.9) has also been reported to work (and quite nicely, based on a screenshot sent to me).
If you know of any other browsers that work correctly with Metamath's Unicode symbols, let me know so that I can put the information here. To check for correctness, compare the symbols in Unicode and GIF versions of the ASCII token chart.
Display font Since some people spend a great deal of time studying this site, I purposely left the main font unspecified so that you can choose the one you find the most comfortable. In Firefox, select Tools -> Options -> Content -> Default font. In Internet Explorer, select Tools -> Internet Options -> Fonts. On Windows, Times New Roman is the standard font. If you prefer a sans-serif font, Arial will align correctly with our math symbol GIF images. By the way, the minty green background color (#EEFFFA=r238,g255,b250) used for the proofs was chosen because it has been claimed to be less fatiguing for long periods of work, but most browsers will let you override it if you wish.
If you are viewing the GIF version of these pages, the appearance may be more consistent if font antialiasing is turned off. If you are viewing the Unicode version, the Unicode symbols may be more legible if it is turned on.
Viewing with a text browser The Metamath Proof Explorer can be viewed with a text-only browser. All symbols will be shown as ASCII tokens. The most common text browser, Lynx, does not format tables, making proofs somewhat confusing to read. But good results are achieved with the table-formatting text browsers w3m [external] and links [external]. Of these, I personally find w3m the most readable.
One advantage of a text browser is that you can select and copy the formulas in a convenient ASCII form that can be pasted into text documents, emails, etc. (The Mozilla browser will also do this if the copy buffer is pasted into a text editor.) Text browsers are also extremely fast if you have a slow connection. If you are blind, a text browser can make this site accessible, although for theorem and proof displays, direct use of the Metamath program CLI (command-line interface) might be more efficient—I would be interested in any feedback on this.
| This
page was last updated on 16-Feb-2013. Your comments are welcome: Norman Megill  Copyright terms: Public domain |
W3C HTML validation [external] |
