Metamath Proof Explorer Home Page

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".

Metamath Proof Explorer Overview

My intellect never quite recovered from the strain of writing [Principia Mathematica].
—Bertrand Russell, The Autobiography of Bertrand Russell, the Early Years

Inspired by Whitehead and Russell's monumental Principia Mathematica, the Metamath Proof Explorer has over 4,000 completely worked out proofs in logic and set theory, interconnected with more than 350,000 hyperlinked cross-references. Each proof is pieced together with razor-sharp precision using a simple substitution rule. With point-and-click links, every step can be drilled down deeper and deeper into the labyrinth until axioms will ultimately be found at the bottom. You could spend literally days exploring the complex tangle of logic leading, say, from 2 + 2 = 4 back to the axioms of set theory. The proof collection includes many famous theorems of elementary set theory.

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 the rules.

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.) At the other extreme of abstraction is the theory of infinite sets (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 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. 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 any proof for yourself with very little skill. All you need is patience. You can jump into the middle of any proof, from the most elementary to the most advanced, and understand immediately the symbol manipulations with no prior knowledge of advanced mathematics or even any mathematics at all. In the next section we show you how.

How Proofs Work

...mathematical proofs, like diamonds, are hard as well as clear, and will be touched with nothing but strict reasoning.
—John Locke, Second Reply to the Bishop of Worcester

Read this section carefully to learn how to follow a Metamath proof.

The only rule you need to know in order to follow a Metamath proof is substitution. In this section we 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.

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 symbol string is a 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. (If you are already comfortable with mathematical logic, the little colored numbers can help you better see the forest through the trees.)

Breakdown of a proof step. If you have a text browser, try to obtain this image if possible; otherwise look at the actual proofs that are linked to and read the text that follows very carefully.

In the figure above we show part of the proof of the theorem 2 + 2 = 4 which is 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. Once you get used to them, though, the indentation levels 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 now have the fixed 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 qualification 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.

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 should now be able to figure out any Metamath proof. In other words, you should be able to draw a diagram like the one above for any proof step of any proof.

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.

Notes on substitutions

Substitutions are simultaneous. In other words each occurrence of a given variable in a referenced theorem must be replaced with the same expression. For example, there are two occurrences of

in the Assertion of opreq2i, and both occurrences must be replaced with the same expression, which is "+" in the above example.

Substitutions are made into the variables of the referenced theorem only, never into the variables of any proof step referenced in the Hyp column (of the theorem being proved). In other words you should pretend that any variables in the theorem being proved are constants for the purpose of figuring out the substitutions. You can see this by looking at examples such as theorem id1.

If the variables of a referenced theorem happen to have the same names as those in the theorem being proved, you may want to temporarily rename the variables in the referenced theorem before substituting expressions for them, to avoid confusion. For example, the proof of id1 will be less confusing if the occurrences of

in the referenced axioms are renamed to something else. Specifically, you can rewrite ax-1 as say

. Then, to obtain step 2 of the proof of id1, substitute "

" for

and "

" for

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. On the other hand there is no such construction that would let us show that the nonsensical "(1 +" is a legal class.

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 case of axioms and definitions, we do show their detailed syntax breakdown (because there used to be unused extra space on those web pages). 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 Theorems of predicate calculus and beyond may have restrictions on the substitutions that can be made into their variables. See the distinct variables discussion below. You usually don't have to worry about them when casually reading a proof - the Metamath proof verifier has assured these restrictions have been met - but for rigorous verification, and for creating new proofs, you must take them into account.

The Axioms

Perfection is when there is no longer anything more to take away.
—Antoine de Saint-Exupery

[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 conveniently be divided into three groups: propositional calculus, predicate calculus, and set theory.

There are two kinds of variables in the axioms, set variables (red) and wff ("well-formed formula") variables (blue). A set variable can only be substituted with another set variable, whereas a wff variable can be substituted with any expression qualifying as a wff.

[In later proofs you will see a third kind of variable, called a class variable, shown in purple. Introduced via definitions, they are theoretically unnecessary but help make our proofs much more efficient. They can always be eliminated down to the first two kinds of variables (for a technical discussion see cleqab). A class variable can be substituted with either a set variable or an expression qualifying as a class.]

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.

Wffs are either true or false, depending on what is assigned to the variables they contain. They are expressions, i.e. strings of symbols, constructed as follows. A starting wff consists of two set variables connected with either ("equals") or ("is an element of," "is contained in"). Two wffs may be connected with ("implies") to form a new wff (and parentheses surround this new wff 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") and a set variable to form a new wff. To summarize: If and are set variables, then and are (starting) wffs. If and are wffs and is a set variable, then , , and are also wffs.

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 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 is true provided the hypotheses are true. A proof is a sequence of substitution instances of axioms, along with substitution instances of inference rules whose hypotheses 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. As is traditional, we use Greek letters for variables that range over arbitrary wffs. 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 P₂. (Thanks to Ted Ulrich for this information.)

**Axioms of propositional calculus**
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; 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 informally used to indicate the relationship between hypotheses and conclusion; they are not part of the formal language.

Predicate calculus introduces the "for all" quantifier, , and postulates its properties. The wff is read "for all x, it is the case that phi is true." In an application, would typically be substituted with a wff containing , such as .

The "pure" predicate calculus deals with quantification of arbitrary wffs. Additional axioms specify properties of equality. Our axioms are formalized differently from the traditional ones in most logic textbooks; see the note on the axioms below.

**Axioms of pure predicate calculus**
Axiom of Specialization	ax-4
Axiom of Quantified Implication	ax-5
Axiom of Quantified Negation	ax-6
Axiom of Quantifier Commutation	ax-7
Rule of Generalization	ax-gen

**Axioms of equality and substitution**
Axiom of Equality (1)	ax-8
Axiom of Existence	ax-9
Axiom of Quantifier Substitution	ax-10
Axiom of Variable Substitution	ax-11
Axiom of Quantifier Introduction (1)	ax-12
Axiom of Equality (2)	ax-13
Axiom of Equality (3)	ax-14
Axiom of Quantifier Introduction (2)	ax-15
Axiom of Distinct Variables	ax-16	, where and are distinct

The last axiom has a restriction on what substitutions we are allowed to make into its set variables. This restriction propagates foward as required into theorems that use this axiom, and you will often see distinct variable conditions associated with theorems.

A final axiom, ax-17, is not shown above because it is really a metatheorem that can be proved (outside of Metamath) from the others and in this sense is redundant. Any particular theorem of logic can be proved (within Metamath) without it. However, it provides us with more general theorem schemes by introducing the notion of "a set variable not occurring in a wff" and can make proofs considerably shorter.

In principle it is possible to reformulate the axioms with as the only connective, making the connective redundant. But actually coming up with a nice set of Metamath-style axioms for this is an interesting open problem (see Problem 13 on the Workshop Miscellany page). This problem basically involves refining and simplifying a starting point that is already given, and it would be a good way for someone to become familiar with the axioms of logic while also producing something useful.

Some definitions will simplify our presentation of the set theory axioms, although in principle they could be eliminated. To understand how definitions are introduced and justified in Metamath, see the note on definitions below. For our purposes, we can pretend they are just additional axioms (which they are in some axiomatizations of logic). Click on the definitions to see how we introduce these new connectives , $/\$ , and that extend the definition of a wff.

**Some definitions**
Definition of Biconditional	df-bi
Definition of Logical AND	df-an	$/\$
Definition of Existential Quantifier	df-ex

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 bizarre 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 . Except for Extensionality, the axioms basically say, "given an arbitrary set , and (in the cases of Replacement and Regularity) provided certain conditions are met, 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 Null Set, Pairing, and Separation from the others as theorems, which are listed in the Theorem Sampler below.

**Zermelo-Fraenkel Set Theory with Choice (ZFC)**
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. Put a copy in your wallet, and you will carry in your pocket the encoding for all theorems ever proved and that ever will be proved, from the most mundane to the most profound.

Note. Books often 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 23 axioms and 2 rules in our system. Together these constitute what is called "ZFC set theory."

A Theorem Sampler

No one shall be able to drive us from the paradise that Cantor has created for us.
—David Hilbert

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. You may also find the Bibliographic Cross-Reference useful. The Theorem List shows the complete set of theorems in the database.

Propositional calculus

Law of identity

Peirce's axiom

Praeclarum theorema

Law of excluded middle

Proposition *5.18 from Principia Mathematica

The consensus theorem for logic circuits

Meredith's astonishing single axiom

Predicate calculus

Existential and universal quantifier swap

Existentially quantified implication

x = x

Definition of proper substitution

Double existential uniqueness

Set theory

Commutative law for union

A basic relationship between class and wff variables

Two ways of saying "is a set"

Derivation of Separation Axiom

Derivation of Empty Set Axiom

Derivation of Pairing Axiom

Kuratowski's ordered pair definition and theorem

Russell's paradox

Set theory (cont.)

The value of a function

Cantor's theorem

Mathematical (finite) induction

Peano's postulates for arithmetic: 1 2 3 4 5

The existence of omega (the gateway to "Cantor's paradise")

Burali-Forti paradox

Transfinite induction

Transfinite recursion part 1 2 3

The amazing recursive definition generator

Schröder-Bernstein Theorem

Pigeonhole principle

Axiom of Infinity equivalent (neat!)

Axiom of Choice equivalent (brainteaser!)

Zermelo's well-ordering theorem

Zorn's Lemma

The 28 postulates for real and complex numbers

Not quite Cantor's diagonal proof

Ordered pair theorem for non-negative integers

Archimedean property of real numbers

The square root of 2 is irrational

The nesting of natural numbers, integers, rationals, reals, and complex numbers

Complex number in terms of real and imaginary parts

Complex conjugate

Triangle inequality for absolute value

2 + 2 = 4 Trivia

First and above all he was a logician. At least thirty-five years of the half-century or so of his existence had been devoted exclusively to proving that two and two always equal four, except in unusual cases, where they equal three or five, as the case may be.
—Jacques Futrelle, Best "Thinking Machine" Detective Stories

This is a one line proof...if we start sufficiently far to the left.
—Unknown

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? Butterfly

Trivia Answer: The longest path back to an axiom from 2 + 2 = 4 is 127 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 <- enqex <- niex <- omex <- zfinf <- inf4 <- inf3 <- inf3lem7 <- inf3lem6 <- inf3lem5 <- inf3lem4 <- inf3lem3 <- inf3lem2 <- inf3lemd <- inf3lemc <- frsuc <- rdgsuct <- rdgsuc <- 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 <- zfpair <- 0inp0 <- 0nep0 <- snnz <- snid <- snidb <- snidg <- elsncg <- dfsn2 <- unidm <- uneqri <- elun <- elab2g <- elabg <- elabgf <- vtoclgf <- hbeleq <- hbel <- hbeq <- hblem <- eleq1 <- cleq2 <- cleq1 <- birbid <- bilbid <- birimd <- bilimd <- pm5.74d <- pm5.74 <- im2and <- prth <- imp4b <- imp4a <- impexp <- birim <- impbi <- bi3 <- expi <- expt <- pm3.2im <- con2d <- con2 <- nega <- pm2.18 <- pm2.43i <- pm2.43 <- pm2.27 <- com12 <- syl <- a1i <- 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 1,957 subtheorems including these. (The command "show trace_back 2p2e4 /essential" will list them.) These have a total of 20,726 steps — this is how many steps you would have to examine if you wanted to verify the proof in complete detail all the way back to the axioms.

Appendix 1: Distinct Variables In logic and set theory literature, a theorem is often accompanied by side conditions written in English, typically written after the statement of the theorem and expressed in a form such as "where ... is a variable that does not occur in the wff ..." Metamath implements these restrictions on a theorem with its "distinct variable" conditions, and often you will see a condition like this accompanying an axiom or theorem:

Distinct variable group(s):

These three groups have the following meanings, respectively: (1) and may not be substituted with the same set variable, (2) whatever set variable is substituted for may not appear in the wff expression substituted for , and (3) whatever set variable is substituted for may not appear in the class expression substituted for . For brevity we may say informally, (1) and must be distinct, (2) must not occur in , and (3) must not occur in .

Note that

Distinct variable group(s):

means the same thing as

Distinct variable group(s):

Finally, if more than two variables appear in a group, this is an abbreviated way of saying that the conditions apply to all possible pairs in the group. So,

Distinct variable group(s):

means the same thing as

Distinct variable group(s):

An example of a theorem with distinct variable conditions is eeanv.

When an axiom or theorem with a distinct variable condition is referenced in a proof, the distinct variable conditions attached the theorem being proved must satisfy those of the referenced axiom or theorem after substitutions are made into the referenced axiom or theorem. In other words a distinct variable condition in an axiom or theorem "propagates" forward into theorems that reference it. This is enforced by the Metamath proof verification engine; it will not allow a distinct variable violation.

In the Metamath language, distinct variable requirements are specified with the $d statement. Each theorem must be accompanied by $d statements specifying those distinct variable requirements that are propagated forward from the axioms and earlier theorems. To get a concrete feel for distinct variable restrictions, you may want to comment out a $d statement in a theorem in the database file set.mm then type "read set.mm" then "verify proof *" in the Metamath program to see the effect. You will see a detailed explanation of the $d violation.

Note. Sometimes new or "dummy" variables are used in a proof but do not occur in the theorem being proved. They are implicitly assumed to be distinct from all other variables, and we omit them from the "Distinct variable group(s)" list for brevity and to make the display more pleasant to read. However, you can see them mentioned explicitly (as is required by the Metamath language) 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.

Appendix 2: A Note on the Axioms The Metamath Proof Explorer's axioms of logic are based on system S3' in Remark 9.6 of the article "A Finitely Axiomatized Formalization of Predicate Calculus with Equality." These are formalized differently from the traditional ones in most logic textbooks, although they are logically equivalent. They were formalized this way in order for their manipulation rules to be much simpler than those for the traditional formalization. In particular, they incorporate no primitive notions of "free variable" and "proper substitution". (See also FAQ question 15 on the Metamath Solitaire page.)

One thing to keep in mind is that Metamath's "axioms" are not the actual axioms of logic but instead are schemes, or recipes, for generating those axioms. In particular, the "set variables" in Metamath's axioms are not the individual variables of actual axioms but rather metavariables ranging over them.

Here is an example. Consider axiom ax-9, which is more conveniently expressed as (theorem a9e), "there exists () an such that equals ." In ordinary logic, 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 . Indeed we can substitute them with the same variable, a fact that might seem at odds with usual 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 not variables but metavariables that range over an infinite set of actual (distinct) variables x₁, x₂, x₃,.... The expression " " is just a recipe for generating an infinite number of actual axioms. In an actual axiom such as "x₃ x₃ = x₂" (that we would normally never write down), symbols x₂ and x₃ always represent distinguished variables by definition. Another axiom that results from the recipe is "x₃ x₃ = x₃", which is quite different but still perfectly sound. On the other hand, when working with the actual axioms there is no rule that allows us to infer "x₃ x₃ = x₃" from "x₃ x₃ = x₂": they are completely independent axioms generated by the scheme. In the actual logic, the only rules of inference are those generated by the modus ponens and generalization schemes, and there is no substitution rule built in as a primitive notion. In fact in the actual logic, if we are given "x₃ x₃ = x₃" there is no way to infer from it (in the absence of scheme ax-9) even the obvious equivalent "x₄ x₄ = x₄" without considerable manipulation (if it is possible at all - I have been unable to find a proof - see Problem 16 on the Workshop Miscellany page).

By the way, the logician Tarski used the axiom scheme in one of his systems without requiring that and be distinct variables [reference: Kalish, D. and R. Montague, "On Tarski's formalization of predicate logic with identity," Arch. f. Math. Logik u. Grundl. 7:81-101 (1965); footnote on p. 81]. So Metamath's axiom system, while unusual, is not alone in its approach. Indeed, many of its ideas are drawn from Tarski's formalizations.

An application of Metamath's substitution rule always creates a new scheme from an old one. This is a key difference from traditional logic, in which a substitution instance of a scheme is intended to be one specific axiom or theorem of the actual logic. We work only with schemes, i.e. metalogic, and never with actual axioms or theorems. (Hence the name Metamath.) Each "theorem" on our proof pages is actually a theorem scheme (metatheorem) that is a recipe for generating an infinite number of actual theorems. The official name of the formal system used by our axioms is simple metalogic, which is defined in Remark 9.6 of the "A Finitely Axiomatized..." article mentioned above.

Sometimes we must place restrictions on the formulas generated by a scheme in order to ensure soundness. 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 "x₁ x₁ = x₁" which would mean "it is not true that all x₁ equal themselves". The metalogical rules of Metamath ensure that distinct variable restrictions "propagate" from axiom schemes having such restrictions into theorem schemes using those axioms.

So what is the difference between Metamath's axioms and traditional textbook axioms? The actual theorems generated are exactly the same. But the "recipes" for generating those theorems have a much simpler metalogical structure, at the expense of greater complexity, and possibly some nonintuitiveness, in the starting axiom schemes. The simple metalogic makes Metamath extremely easy to work with in a computer program, without the English verbiage associated with the notions of "free variable" and "proper substitution." In the Metamath axiom schemes these notions do not exist. They are artificial concepts that textbooks introduce as part of their (equivalent) metalogical recipes for generating axioms. Of course they are useful high-level concepts for humans when thinking about logic, but they add to the complexity of a computer program that works with them.

Many or most automated theorem provers, such as Otter [external], work with symbols representing the actual variables of logic, which are always assumed to be distinct, rather than with metavariables ranging over them. This necessitates the use of somewhat complex renaming rules to handle the free variable and proper substitution requirements. Metamath seems unusual in this regard, in that it works directly and only with metavariables. Whether this offers any advantages for automated theorem proving is unknown; the Metamath program is not a theorem prover but merely a proof verifier.

Finally, here is a note on the "A Finitely Axiomatized Formalization of Predicate Calculus with Equality" article for those interested. 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. In the metalogical completeness Theorem 9.7, some details that are "provable in S3' with simple metalogic" but nonetheless are tricky, are proved in theorems sbequ, sbcom2, and sbid2.

Appendix 3: Traditional Textbook Axioms of Predicate Calculus with Equality

If you want to acquire a practical working ability in logic (as opposed to just being able to follow mindlessly the symbol manipulations in our proofs), it is a good idea to become familiar with the traditional 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.

For propositional calculus, the traditional axiom and rule schemes are exactly the same as in Metamath, 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 (which we link to the roughly equivalent theorems in our formalization). 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.

stdpc4	, provided that is free for in
stdpc5	, provided that does not occur free in
ax-gen
eqid
sbequ2	, provided that is free for in

Three of these axiom schemes have English-language conditions on them. These conditions are somewhat messy to formalize, but they are not too hard to grasp. 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, PDF pp. 42-43) defines "free variable," and Section 2.11 (pp. 48-51, PDF pp. 54-57) defines "free for."

Although in some sense the traditional axiom schemes are more compact than Metamath's ax-4 through ax-16, their goal is simply to provide recipes for generating actual axioms, from which we then prove actual theorems. Theorem schemes can also be proved, but their proofs use 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 generate directly all possible theorem schemes (or more precisely, all possible schemes expressible in "simple metalogic" as defined in the "A Finitely Axiomatized Formalization of Predicate Calculus with Equality" article).

Metamath's axiom schemes of predicate calculus can be proved from the traditional ones by combining a number of special cases that follow from them. The two systems generate exactly the same set of actual theorems.

Metamath's axiom system has no built-in notion of free and bound variables. Instead, we use the hypothesis when we want to say (as we do in stdpc5) that " is effectively not free in ." We say "effectively" because any wff that is also a theorem, such as , will satisfy the hypothesis even though may technically be free in it. Our axioms also have no built-in notion of "free for." Instead we use (as in stdpc4) the notation to mean "the wff that results when is properly substituted for in the wff ." This notation is defined in 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.

Appendix 4: A Note on Definitions The Metamath language provides a very 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 is permissable. The same holds for what we call "definitions" - to Metamath definitions merely extend the formal system and are indistinguishable from axioms by the proof verifier.

For convenience we usually make an artificial distinction by prefixing their names with "df-". But all definitions are assumed to have been metalogically justified as sound outside of the Metamath formalism, meaning that they must be eliminable and must not strengthen the axiom system when they are eliminated. A carelessly introduced definition can easily lead to inconsistency.

This method of introducing definitions as new axioms keeps the Metamath language simple, flexible, and not tied to any specific formal system. If it bothers us we should consider all definitions to be additional axioms, following ultraconservative logicians such as Lesniewski [C. Lejewski, "On implicational definitions," Studia Logica 8:189-208 (1958)]. But except for five cases (df-bi, df-clab, df-cleq, df-clel, and df-sbc), we adopt the convention of introducing definitions by connecting a new symbol (or a unique new combination of symbols) with existing ones using either (if we are defining a new wff) or (if we are defining a new class). With this convention, the soundness of definitions is more or less obvious by inspection. A soundness check of such definitions could be automated although presently it is not - in part because I didn't want to complicate Metamath nor restrict it to a specific formal system.

Another issue is whether a definition matches the generally understood meaning of a concept. For example, if we swapped the symbols (df-q) and (df-r) everywhere, all definitions would remain sound but we could "prove" that the square root of 2 is rational as a special case of sqrcl. For this reason, most definitions must be carefully scrutinized by a competent mathematician anyway, and manual verification of soundness tends to be a byproduct of this inspection.

Nonetheless, the present lack of built-in soundness checking of definitions is a deficiency of Metamath compared to some other proof languages, and I may revisit it at some point. An example where it could be beneficial is in the construction of complex numbers: our only goal is to construct an object with the desired properties, and we don't really care what "throwaway" definitions we use along the way as long as they are sound. Automated soundness checking will become more important if Metamath is ever used in a large-scale collaborative project. (Thanks to Raph Levien for some comments on this issue and to Bob Solovay for proving the soundness of some of the trickier syntax constructions in the set.mm database.)

The definition list (400K) shows all of the definitions in the database.

Note added 8-Jun-03, updated 29-Nov-03: Raph Levien has devised an ingenious method for proving soundness of Metamath-style definitions that is remarkable for its simplicity and that doesn't affect the generality of Metamath's formal system. As of this writing, he is developing a new proof language called Ghilbert [external] that is based on LISP S-expressions and incorporates his new method for handling definitions. Its goal is to be a more useful system than Metamath for collaborative work, yet its proofs should be translatable to our Metamath proofs and vice-versa.

Appendix 5: How to Find Out What Axioms a Proof Depends On At the end of each proof there is a list called "This theorem was proved from these axioms." These are the axioms needed to prove the theorem from scratch, if all definitions were eliminated. You are not expected 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 tried to do, so this list is usually 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-inf. 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 - drilling down 29 layers we find it referenced in the proof of niex, which shows the the class of positive integers (from which the real numbers are constructed) is a set (i.e. exists). The Axiom of Infinity is used there in the form omex, which is a convenient version of the Axiom of Infinity using class notation. (Exercise: try to follow it all the way back to ax-inf. Answer: omex <- zfinf <- inf4 <- axinf <- ax-inf). Fortuitously, the theorem niex shows up in the 2 + 2 = 4 Trivia above so you can see its path towards proving (2 + 2) = 4.

Note for nitpicky logicians: you may find it strange that the Axiom of Regularity ax-reg is used for the proof of 2p2e4. This is because our version of the Axiom of Infinity ax-inf, which I chose because it is shorter to state than the usual one (inf4), needs Regularity to derive the usual one from it. Specifically, it is invoked at step 38 of the proof of inf3lem3.

Appendix 6: Notation for Function Values In general I tried to choose notation that is conventional or familiar, but I had to weigh it against introducing ambiguity or making the collection of notations too bloated. Sometimes I favored simplicity and consistency over convention. A notable example is the notation for "the value of a function" cfv, expressed by "

". Here "

" is a class that normally is a function, and "

" 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. Our notation is a formal one often used by set theorists and has the advantage for us that the constant symbol "" makes it unambiguous, unlike the more common textbook notation.

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 general results. For example, in the square root theorem sqrth, the square root symbol "" is a function i.e. a class (csqr), and we would show the square root of 2 as "