MetamathHome
Last >
| Metamath Home |
Metamath Proof Explorer Home Page | First > Last > |
| Contents of this page | Related pages To search this site you can 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 8,000 completely worked out proofs in logic and set theory, interconnected with over a million hyperlinked cross-references. Each proof is pieced together with razor-sharp precision using a simple substitution rule that practically anyone 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 2+2=4 back to the 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 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 or counting numbers, whose properties match those we observe when we count everyday objects. 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, sometimes called "Cantor's paradise." Some of the world's most brilliant mathematicians have given us deep insight into this mysterious and wondrous universe that, so far as we know, exists only in the mind.
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 result in its proof steps, 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.]
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). Two substitution instances of this law are 5 + 3 = 3 + 5 and (b - 7) + c = c + (b - 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 that took
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 Expression shown 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
can be assigned to 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 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 and take a quick look at this summary of symbols. 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 Roman italic letters for set variables.
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.
Wffs are either true or false, depending on what is
assigned to the variables they contain.
They are expressions constructed as follows, and expressions constructed
this way can be substituted for wff variables in the axioms (or in
theorems derived from the axioms).
A starting wff is either 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. Exercise: Convince yourself that the
axioms below are wffs. Answer:
The web page for each axiom,
for example ax-10,
presents its construction in a
syntax breakdown chart.
Wffs constructed this way are, in principle, able to express all of mathematics. In practice it is inefficient, and as we develop mathematics from the axioms we often introduce new symbols to abbreviate (define) more complex expressions. But these can always be broken down into the form we just described.
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 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 two symbols, ("equals") and ("is a member of"), 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. Predicate calculus also introduces a symbol called the
"universal quantifier." It ranges over or "scans" its second (wff)
argument with all possible values of its first (set variable) argument,
returning true if and only if it is the case that the second argument is
true regardless of the value of the first argument. 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" might be more generally
called "individual variables" in predicate calculus without set theory.)
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. Our axioms—which correspond to axiom schemes of the traditional system—are closely related to a system of Tarski (see the note on the axioms below).
The subsystem we call "pure" predicate calculus deals with quantification of arbitrary wffs. Additional axioms specify properties of equality. If we wish, we can replace ax-4, ax-6, and ax-7 with a single axiom; see theorem ax467.
| |||||||||||||||||||||
| |||||||||||||||||||||
|
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.
Three other axioms, ax-11o, ax-15, and ax-16, are not included above because they can be derived from the others. From the set consisting of these three axioms plus the others 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.
In the ZFC axioms that follow, all set
variables are assumed to be distinct. If
you click on the 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. 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 axext.) 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.
| Axiom of Extensionality | ax-ext |
 |
| Axiom of Replacement | ax-rep |
 |
| Axiom of Union | ax-un |
|
| Axiom of Power Sets | ax-pow |
|
| 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 plus the axioms and rules of propositional and predicate calculus, which total 22 axioms and 2 rules in our system. Together these constitute what is called "ZFC set theory."
Grothendieck's 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. Grothendieck's 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. Grothendieck's axiom can be viewed as a very strong replacement of the Axiom of Infinity and implies both that axiom (shown by theorem grothinf) and the Axiom of Choice (whose proof by Tarski, "On well-ordered subsets of any set", Fundamenta Mathematicae 32:176-183 (1939), still needs to be formalized—any volunteers?).
| Grothendieck's 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 Grothendieck's 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: The longest path back to an axiom from 2 + 2 = 4 is 134 levels 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 <- readdcl <- axaddrcl <- addresr <- 0idsr <- 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 <- rdglimt <- rdglim <- rdgfnon <- tfr1 <- tfrlem13 <- tfrlem12 <- tfrlem11 <- tfrlem9 <- tfrlem7 <- tfrlem5 <- tfrlem2 <- tfrlem1 <- tfis2 <- tfis2f <- tfis <- tfi <- onsst <- ordsson <- ordeleqon <- onprc <- ordon <- ordtri3or <- ordsseleq <- ordelssne <- tz7.7 <- tz7.5 <- wefrc <- epfrc <- epel <- epelc <- brab <- brabg <- opelopabg <- opabid <- opex <- prex <- snex <- 0ex <- eueq <- eu4 <- mo4 <- mo4f <- mo3 <- mo2 <- eu3 <- eu2 <- euex <- eu1 <- sb8eu <- sb8 <- sbid2 <- sbco <- sbbi <- sban <- sbim <- sbi2 <- sbn <- sbn1 <- sb4 <- equs5 <- hbnae <- hbae <- alequcoms <- alequcom <- equcomi <- equid <- ax9 <- 19.22 <- 3imtr4g <- 3imtr3g <- anbi2i <- anim2i <- anim12i <- pm3.26 <- sylbi <- biimp <- bi1 <- pm3.26im <- con1i <- negb <- nega <- pm2.18 <- pm2.43i <- pm2.43 <- pm2.27 <- id <- mpd <- a2i <- ax-1
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,204 subtheorems including these. (The command "show trace_back 2p2e4 /essential" will list them.) These have a total of 23,085 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.
The description of the Axioms for Complex Numbers provides an overview of the number constructions involved in the last stages of the 2 + 2 = 4 proof.
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 still requires nontrivial and somewhat ad hoc metalogic, such as induction on formula length, to derive theorem schemes (as opposed to specific theorems). Theorem schemes are more efficient for building a body of mathematical knowledge, since they can be reused with different instances as needed. However, the metalogic needed to derive them in Tarski's system is difficult to automate in a proof verifier.
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 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 (also defined there) of Tarski's system by using only Metamath's direct substitution rule applied to the axiom system (and no other metalogical notions "outside" of the system).
[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 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
formulas with the connectives , , and (such as "v2 = v4 v3 v2"). That is the complete actual language of logic
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 "."
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 scope
of a quantifier such as is considered "bound," otherwise it is "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, a fact that might seem at odds
with the traditional rule that free and bound variables must always be
distinguished. Well, in the actual axioms generated by this scheme, the
variables are considered to be distinct. The symbols and are metavariables that range over
the infinite set of actual (distinct) variables v1, v2,
v3,....
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 distinguished variables by
definition. 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 "v3v3 v3 =
v2" by generalization—and there
is no substitution rule built in as a primitive notion.
In fact, 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." That also shows that a single axiom
representative of ax-9 is not sufficient for the
logic to be complete; we need the infinite number of axioms
corresponding to this Metamath scheme.
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. Proofs 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
Read this section
carefully to learn how to follow a Metamath proof.
