mmset.raw.html

<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN"
   "https://www.w3.org/TR/html4/loose.dtd">
<!-- The file mmset.html is generated from mmset.raw.html -
  see the regen-from-raw script for details -->
<HTML LANG="EN-US">

<!-- To convert mmset.raw.html to mmset.html, use the metamath.exe command:
  markup mmset.raw.html mmset.html /alt_html /symbols /css /labels
-->

<!-- Warning (4-Aug-2021):  The link https://validator.w3.org/check?uri=referer
on the bottom right of this page no longer works correctly (it checks the wrong
page, so you may be tricked into thinking there are no errors).  Instead, paste
the URL of this page directly into https://validator.w3.org/ or use their
upload feature.  -->

<HEAD>

<!-- improve mobile display -->
<META NAME="viewport" CONTENT="width=device-width, initial-scale=1.0">

<META HTTP-EQUIV="Content-Type" CONTENT="text/html; charset=iso-8859-1">
<TITLE>Proof Explorer - Home Page - Metamath</TITLE>
<LINK REL="shortcut icon" HREF="favicon.ico" TYPE="image/x-icon">

<!--
<style type="text/css">
@media screen { /* hide from IE3 */ a[href]:hover { background: #ffa } }
</style>
<style type="text/css"> a:hover { background: #A6CAF0 } </style>
<style type="text/css"> a:hover { background: #B2FFE8 } </style>
<style type="text/css"> a:hover { background: #E2F2DE } </style>
<style type="text/css"> a:hover { background: #C9FFBC } </style>
<style type="text/css"> a:hover { background: #D6D6FF }
<style type="text/css"> TABLE,TD { border-style: ridge } </style>
-->

<STYLE TYPE="text/css">
<!--
/* Math symbol image will be shifted down 4 pixels to align with normal
  text for compatibility with various browsers.  The old ALIGN=TOP for
  math symbol images did not align in all browsers and should be deleted.
  All other images must override this shift with STYLE="margin-bottom:0px".
  (2-Oct-2015 nm) */
img { margin-bottom: -4px }
-->
</STYLE>

</HEAD>

<BODY BGCOLOR="#FFFFFF" STYLE="padding: 0px 8px">

<TABLE BORDER=0 CELLSPACING=0 CELLPADDING=0 WIDTH="100%">

  <TR>
    <TD ALIGN=LEFT VALIGN=TOP><A HREF="../index.html"><IMG SRC="mm.gif"
      BORDER=0
      ALT="Metamath Home"
      TITLE="Metamath Home"
      HEIGHT=32 WIDTH=32 ALIGN=TOP STYLE="margin-bottom:0px"></A>
    </TD>
    <TD ALIGN=CENTER VALIGN=TOP><FONT SIZE="+3"
      COLOR="#006633"><B>Metamath Proof Explorer Home Page</B></FONT>
    </TD>

    <TD NOWRAP ALIGN=RIGHT VALIGN=TOP><FONT SIZE=-2
      FACE=sans-serif> <A HREF="wn.html">First &gt;</A><BR><A
      HREF="grothprim.html">Last &gt;</A></FONT>
    </TD>
  </TR>

  <TR>
    <TD COLSPAN=3 ALIGN=LEFT VALIGN=TOP><FONT SIZE=-2
      FACE=sans-serif>
      <A HREF="../mm.html">Mirrors</A>&nbsp; &gt;
        &nbsp;<A HREF="../index.html">Home</A>&nbsp; &gt;
      &nbsp;MPE Home&nbsp; &gt;
      &nbsp;<A HREF="mmtheorems.html">Th. List</A>&nbsp; &gt;
      &nbsp;<A HREF="mmrecent.html">Recent</A>
      </FONT>
    </TD>
  </TR>
</TABLE>

<!--
<TABLE BORDER=0 WIDTH="100%"><TR>
<TD NOWRAP ALIGN=LEFT VALIGN=TOP><FONT SIZE=-2 FACE=sans-serif><A
HREF="../index.html"><IMG SRC="mm.gif" BORDER=0 ALT="Metamath Home"
HEIGHT=32 WIDTH=32 ALIGN=LEFT STYLE="margin-bottom:0px"><IMG
SRC="spacer.gif" BORDER=0 ALT="" HEIGHT=32 WIDTH=2 ALIGN=LEFT
STYLE="margin-bottom:0px">Metamath<BR>Home</A></FONT></TD>

<TD ALIGN=CENTER VALIGN=TOP>
<FONT COLOR="#006633">
<FONT SIZE="+3">
<B>Metamath Proof Explorer Home Page</B>
</FONT>
</FONT>
</TD>

<TD NOWRAP ALIGN=RIGHT VALIGN=TOP>
<FONT SIZE=-2 FACE=sans-serif>
<A HREF="wn.html">First &gt;</A>
<BR>
<A HREF="grothprim.html">Last &gt;</A>
</FONT>
</TD>
</TR>
</TABLE>
-->

<HR SIZE=1 NOSHADE>

<FONT SIZE=-1>
<FONT COLOR="#006633">
The aleph null above is the symbol for the first infinite cardinal number,
discovered by Georg Cantor in 1873 (see Theorem ~ aleph0 ).
</FONT>
</FONT>

<HR NOSHADE SIZE=1>

<FONT SIZE=-1>
<FONT COLOR="#006633">
This is the starting page for the Metamath Proof Explorer subproject (set.mm
database).  See the main
</FONT>
<A HREF="../index.html">Metamath Home Page</A><FONT COLOR="#006633"> for an
overview of Metamath and download links.  If you wish to contribute your own
proofs to the Metamath project, see <A HREF="../index.html#contribute">How can
I contribute to Metamath?</A>
</FONT>
</FONT>

<HR NOSHADE SIZE=1>
<TABLE BORDER=0 WIDTH="100%">
<TR>
<TD VALIGN=TOP WIDTH="50%">
<B><FONT COLOR="#006633">Contents of this page</FONT></B>
<MENU>
<LI>
<A HREF="#overview">Metamath Proof Explorer Overview</A></LI>
<LI>
<A HREF="#proofs">How Metamath Proofs Work</A>
<!--
<FONT SIZE=-2 FACE="Comic Sans MS" COLOR=ORANGE>Revised</FONT>
<FONT SIZE=-1><I>23-Apr-2006</I></FONT>
-->
<!--
<FONT SIZE=-2 FACE="Comic Sans MS" COLOR=ORANGE>Added</FONT>
<FONT SIZE=-1><I>20-May-2003</I></FONT>
-->
</LI>
<LI>
<A HREF="#axioms">The Axioms</A>
<FONT SIZE=-1>(<A HREF="#scaxioms">Propositional Calculus</A>,
<A HREF="#pcaxioms">Predicate Calculus</A>,
<A HREF="#staxioms">Set Theory</A>,
<A HREF="#groth">The Tarski&ndash;Grothendieck Axiom</A>)</FONT>
<!--
<FONT SIZE=-2 FACE="Comic Sans MS" COLOR=ORANGE>Revised </FONT>
<FONT SIZE=-1><I>22-June-2009 (the Tarski&ndash;Grothendieck Axiom)</I></FONT>
-->
</LI>
<LI>
<A HREF="#class">The Theory of Classes</A>
<FONT SIZE=-2 FACE="Comic Sans MS" COLOR=ORANGE>Added</FONT>
<FONT SIZE=-1><I>13-Dec-2015</I></FONT>
</LI>
<LI>
<A HREF="#theorems">A Theorem Sampler</A>
<!--
<FONT SIZE=-2 FACE="Comic Sans MS" COLOR=ORANGE>Revised</FONT> <FONT
SIZE=-1><I>19-May-2003</I></FONT>
-->
</LI>
<LI>
<A HREF="#trivia">2 + 2 = 4 Trivia</A>
<FONT SIZE=-1>(<A HREF="#2p2e4length">more</A>)
<!--
<FONT SIZE=-2 FACE="Comic Sans MS" COLOR=ORANGE>Added</FONT> <FONT
  SIZE=-1><I>22-Dec-2018</I></FONT>
-->
</FONT>
</LI>
<LI>
<A HREF="#axiomnote">Appendix 1: A Note on the Axioms</A>
<!--
<FONT SIZE=-2 FACE="Comic Sans MS" COLOR=ORANGE>Revised</FONT> <FONT
SIZE=-1><I>10-Jul-2015</I></FONT>
-->
</LI>
<LI>
<A HREF="#traditional">Appendix 2: Traditional
Textbook Axioms of Predicate Calculus</A>
<!--
<FONT SIZE=-2 FACE="Comic Sans MS" COLOR=ORANGE>Revised</FONT> <FONT
SIZE=-1><I>6-Oct-2005</I></FONT>
-->
</LI>
<LI> <A HREF="#distinct">Appendix 3: Distinct Variables</A>
<FONT SIZE=-1>(<A HREF="#dv-history">History</A>,
  <A HREF="#dv-notes">Notes</A>)</FONT>

<FONT SIZE=-2 FACE="Comic Sans MS" COLOR=ORANGE>Revised</FONT> <FONT
SIZE=-1><I>21-Dec-2016</I></FONT>

<!--
<FONT SIZE=-2 FACE="Comic Sans MS" COLOR=ORANGE>Revised</FONT> <FONT
  SIZE=-1><I>16-Jun-2008 (added Note 4)</I></FONT>
-->

</LI>
<LI> <A HREF="#definitions">Appendix 4: A Note on Definitions</A></LI>

<LI> <A HREF="#assume">Appendix 5: How to Find Out What Axioms a Proof
Depends On</A></LI>
<LI> <A HREF="#function">Appendix 6: Notation for Function and Operation
 Values</A></LI>

<LI> <A HREF="#subsys">Appendix 7: Some Predicate Calculus
Subsystems</A>

</LI>

<LI> <A HREF="#oldaxioms">Appendix 8: Axiom Numbering
Before December 2018</A>

<!--
<FONT SIZE=-2 FACE="Comic Sans MS" COLOR=ORANGE>Added</FONT> <FONT
SIZE=-1><I>26-Dec-2018</I></FONT>
-->

</LI>

<LI> <A HREF="#read">Reading Suggestions</A>

<!--
<FONT SIZE=-2 FACE="Comic Sans MS" COLOR=ORANGE>Revised</FONT> <FONT
SIZE=-1><I>23-Aug-2006</I></FONT>
-->

</LI>

<LI> <A HREF="#bib">Bibliography</A></LI>

<LI> <A HREF="#textonly">Browsers and Fonts</A></LI>
<!--
<LI> <A HREF="#textonly">Viewing with a Text Browser</A></LI>
<LI> <A HREF="#unicode">Browsing with the Unicode Font</A>
<LI> <A HREF="#copyright">Copyright Terms</A>

<FONT SIZE=-2 FACE="Comic Sans MS" COLOR=ORANGE>Added</FONT> <FONT
SIZE=-1><I>8-Aug-2003</I></FONT>

</LI>
-->

</MENU>
</TD>

<TD VALIGN=TOP>
<B><FONT COLOR="#006633">Related pages</FONT></B>
<MENU>

<!--
<LI> <A HREF="mmtheorems.html#mmtc">Table of Contents and Theorem List</A></LI>
-->
<LI> <A HREF="mmtheorems.html">Theorem List (Table of Contents)</A> </LI>

<LI>
<A HREF="mmrecent.html">Most Recent Proofs (this mirror)</A>
(<A HREF="https://us.metamath.org/mpeuni/mmrecent.html">latest</A>)
</LI>

<LI>
<A HREF="conventions.html">Conventions and Style</A>

<!--
<FONT SIZE=-2 FACE="Comic Sans MS" COLOR=ORANGE>Added</FONT>
<FONT SIZE=-1><I>15-Jan-2017</I></FONT>
-->

</LI>

<LI> <A HREF="mmbiblio.html">Bibliographic Cross-Reference</A> </LI>

<LI> <A HREF="mmdefinitions.html">Definition List (3MB)</A> </LI>

<LI>
<A HREF="mmnatded.html">Deduction Form and Natural Deduction</A>

<!--
<FONT SIZE=-2 FACE="Comic Sans MS" COLOR=ORANGE>Added</FONT>
<FONT SIZE=-1><I>7-Feb-2017</I></FONT>

<FONT SIZE=-1>(<A HREF="natded.html">Natural Deduction Rules</A>
-->

<!--
<FONT SIZE=-2 FACE="Comic Sans MS" COLOR=ORANGE>Added</FONT>
<FONT SIZE=-1><I>9-Feb-2017</I></FONT>)</FONT>
-->
</LI>

<LI>
<A HREF="mmdeduction.html">Weak Deduction Theorem</A> (an older method)
</LI>

<LI>
<A HREF="mmcomplex.html">Real and Complex Numbers</A>
</LI>

<LI>
<A HREF="mmtopstr.html">Algebraic and Topological Structures</A>
<FONT SIZE=-2 FACE="Comic Sans MS" COLOR=ORANGE>Added</FONT>
<FONT SIZE=-1><I>24-Nov-2018</I></FONT>
</LI>

<LI>
<A HREF="mmfrege.html">Frege Notation</A>
<FONT SIZE=-2 FACE="Comic Sans MS" COLOR=ORANGE>Added</FONT>
<FONT SIZE=-1><I>7-Nov-2020</I></FONT>
</LI>

<LI>
<A HREF="mmzfcnd.html">ZFC Axioms With No Distinct Variables</A>
<!--
<FONT SIZE=-2 FACE="Comic Sans MS" COLOR=ORANGE>Revised</FONT>
<FONT SIZE=-1><I>12-Apr-2008</I></FONT>
-->
</LI>

<LI>
<A HREF="mmascii.html">ASCII Symbol Equivalents for Text-Only Browsers</A>
</LI>

<LI>
Miscellaneous <A HREF="mmnotes.txt">notes</A>
</LI>

<LI>
<A HREF="../index.html#contribute">How can I contribute to Metamath?</A>
</LI>

<!-- <LI> <A HREF="mmhil.html">Hilbert Space Explorer Home Page</A></LI> -->
</MENU>

<B><FONT COLOR="#006633">External links</FONT></B>
<MENU>
<LI>
<A HREF="https://github.com/metamath/set.mm">GitHub repository</A>
(contains the database as well as help on contributing)
</LI>

<!--
<LI>
<A HREF="http://math.vanderbilt.edu/~~schectex/ccc/choice.html">
A home page for THE AXIOM OF CHOICE</A>
[retrieved 21-Dec-2016] has some interesting set theory information.
</LI>
-->
</MENU>

<FONT SIZE=-1>
<B><FONT COLOR="#006633">To search this site</FONT></B>
you can use <A HREF="http://www.google.com/">Google</A> [retrieved 21-Dec-2016]
restricted to a mirror site.  For example, to find references to infinity enter
"infinity site:us.metamath.org".

<B><FONT COLOR="#006633">More efficient searching</FONT></B>
<!-- for particular symbols and patterns -->
is possible with direct use of the
<A HREF="../index.html#mmprog">Metamath program</A>, once you get used to its
<A HREF="mmascii.html">ASCII tokens</A>.  See the wildcard features in "help
search" and "help show statement".
</FONT>
</TD>
</TR>
</TABLE>

<P>
<HR NOSHADE SIZE=1><A NAME="overview"></A>
<B><FONT COLOR="#006633">Metamath Proof Explorer Overview</FONT></B>
&nbsp;&nbsp;&nbsp;


<!--
<P>
<CENTER>
<FONT COLOR="#006633">
<I>My intellect never quite recovered from the strain of writing.</I>
[Principia Mathematica]
<BR>
&mdash;Bertrand Russell,
<I>The Autobiography of Bertrand Russell, the Early Years</I>
</FONT>
</CENTER>
-->

<!--
<P>
<CENTER>
<FONT COLOR="#006633">
<I>I have been ever since definitely less capable of dealing with difficult
abstractions than I was before.</I>
&mdash; Bertrand Russell
</FONT>
</CENTER>
-->

<!--
<P>
<CENTER>
<FONT COLOR="#006633">
<I>...today we know that it is possible, logically speaking, to derive almost
all of present-day mathematics from a single source, the Theory of Sets.</I>
<BR>
&mdash;Nicolas Bourbaki
</FONT>
</CENTER>
-->

<P>
<CENTER>
<FONT COLOR="#006633"><I>From <A HREF="pm54.43.html">this
proposition</A> it will follow, when arithmetical addition has been
defined, that 1+1=2.</I><BR> &mdash;<I>Principia Mathematica</I>, Volume
I, page 360.</FONT>
</CENTER>

<!--
<P>
<CENTER>
<FONT COLOR="#006633">
<I>Mathematics is a game played according to certain simple rules with
meaningless marks on paper.</I>
<BR>
&mdash;David Hilbert
</FONT>
</CENTER>
-->

<P>
<CENTER>
<TABLE WIDTH="90%">
<TR><TD ALIGN=CENTER>
<TABLE BORDER=0 CELLSPACING=0 CELLPADDING=5 BGCOLOR="#EEFFFA">
<TR><TD ALIGN=CENTER>
David A. Wheeler has prepared an excellent 14-minute YouTube video,
<A HREF="https://www.youtube.com/watch?v=8WH4Rd4UKGE">Metamath Proof Explorer:
A Modern Principia Mathematica</A>, on the history of formalization and the
motivation for Metamath, the proof of 2+2=4, and more.</TD>
</TR>
</TABLE>
</TD>
</TR>
</TABLE>
</CENTER>

<P>
Inspired by Whitehead and Russell's monumental <I>Principia Mathematica</I>,
<!--(where 1+1=2 is finally proved on page 86 of Volume II), -->
the Metamath Proof Explorer has over 26,000 completely worked out proofs in its
main sections (and over 41,000 counting "mathboxes", which are annexes where
contributors can develop additional topics), starting from the very foundation
that mathematics is built on and eventually arriving at familiar mathematical
facts and beyond.
<!-- 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 (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&mdash;the starting point for
all of mathematics&mdash;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 <A HREF="#trivia">2+2=4</A> back to these
axioms.
</P>

<P>
Essentially everything that is possible to know in mathematics can be derived
from a handful of axioms known as <I>Zermelo-Fraenkel set theory,</I> 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.
</P>

<P>
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 <I>formalism</I> 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.
<!-- Amazingly, the rules - with which essentially all of mathematics can be
derived - are simpler than those involved in a game of chess! -->
</P>

<P>
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 <A HREF="#trivia">2 + 2 = 4</A> 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."
</P>

<!--
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.
-->
<!--
that transcends the physical universe, giving us a glimpse into a higher
reality, perhaps even the mind of God.
-->

<P>
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.
</P>

<P>
<HR NOSHADE SIZE=1><A NAME="proofs"></A>
<B><FONT COLOR="#006633">How Metamath Proofs Work</FONT></B>

<P>
<CENTER>
<FONT COLOR="#006633">
<I>A mathematical theory is not to be considered complete until you have made
it so clear that you can explain it to the first man whom you meet on the
street.</I>
<BR>
&mdash;David Hilbert
</FONT>
</CENTER>

<!--
<P>
<CENTER>
<FONT COLOR="#006633">
<I>Thus mathematics may be defined as the subject in which we never know what
we are talking about, nor whether what we are saying is true.</I>
<BR>
&mdash;Bertrand Russell
</FONT>
</CENTER>

<P>
<CENTER>
<FONT COLOR="#006633">
<I>The lyf so short, the craft so long to lerne </I>
<BR>
&mdash;Geoffrey Chaucer
</FONT>
</CENTER>

<P>
<CENTER>
<FONT COLOR="#006633">
<I>The ultimate goal of mathematics is to eliminate any need for intelligent
thought.</I>
<BR>
&mdash;Alfred North Whitehead
</FONT>
</CENTER>

<P>
<CENTER>
<FONT COLOR="#006633">
<I>...mathematical proofs, like diamonds, are hard as well as clear, and will
be touched with nothing but strict reasoning.</I>
<BR>
&mdash;John Locke, <I>Second Reply to the Bishop of Worcester</I>
</FONT>
</CENTER>

<P>
<BLOCKQUOTE>
<FONT COLOR="#006633" SIZE=-1>
He was 40 yeares old before he looked on Geometry; which happened accidentally.
Being in a Gentleman's Library, Euclid's Elements lay open, and 'twas the 47
<I>El. libri</I> I. He read the Proposition.  <I>By G__,</I> sayd he (he would
now and then sweare an emphaticall Oath by way of emphasis) <I>this is
impossible!</I> So he reads the Demonstration of it, which referred him back to
such a Proposition; which Proposition he read.  That referred him back to
another, which he also read.  <I>Et sic deinceps</I> that at the last he was
demonstratively convinced of that trueth.  This made him in love with Geometry.
</FONT>

<CENTER>
<FONT COLOR="#006633" SIZE=-1>&mdash;John Aubrey, "A Brief Life of
Thomas Hobbes, 1588-1679" in <I>Brief Lives</I> (c. 1694)
</FONT>
</CENTER>
</BLOCKQUOTE>
-->

<P>
<CENTER>
<TABLE WIDTH="90%">
<TR><TD ALIGN=CENTER>
<TABLE BORDER=0 CELLSPACING=0 CELLPADDING=5 BGCOLOR="#EEFFFA">
<TR><TD ALIGN=CENTER><IMG SRC="_nmegill.gif" WIDTH=16 HEIGHT=19
ALT="The Floating Head of Wisdom says: "
TITLE="The Floating Head of Wisdom says: ">&nbsp;&nbsp;&nbsp;
<FONT COLOR="#F7941D">
<B>Read this section carefully to learn how to follow a Metamath proof.</B>
</FONT>
</TD></TR></TABLE>
</TD></TR></TABLE>
</CENTER>

<!--
<P>
<FONT SIZE="-1">
[If you are a math novice (or not) and have trouble understanding this section,
<A HREF="../email.html">let me know</A> what you find confusing so that I can
try to improve it.  An important point sometimes misunderstood is that Metamath
is <I>not</I> a theorem prover&mdash;it does not find these proofs on its own
but just verifies the correctness of proofs provided to it by its users.]
</FONT>
-->

<P>
<B><FONT COLOR="#006633">What you need to know</FONT></B>
&nbsp;&nbsp;&nbsp;
The only rule you need to know in order to follow the symbol manipulations in a
Metamath proof is <B>substitution</B>.  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
<I>a</I> + <I>b</I> = <I>b</I> + <I>a</I>, where <I>a</I> and <I>b</I> are
variables (placeholders for numbers).  Two substitution instances of this law
are 5 + 3 = 3 + 5 and (<I>x</I> - 7) + <I>c</I> = <I>c</I> + (<I>x</I> - 7).
That's the only mathematical concept you need!
<!-- And if you don't know it, reread this paragraph until you do! -->
Substitution is just writing down a specific example
<!-- or a specialized version --> of a more general formula.
</P>

<!--
<B>Exercise:</B> How do we avoid confusion due to the fact that the
<I>b</I> in the second substitution instance also occurs in the original
formula?  <B>Answer:</B> Rename the <I>b</I> of the original formula to
some other variable, say <I>d</I>, giving us <I>a</I> + <I>d</I> =
<I>d</I> + <I>a</I>.  Then we replace the two occurrences of <I>a</I>
with (<I>b</I> - 7) and the two occurrences of <I>d</I> with <I>c</I>,
yielding the final answer (<I>b</I> - 7) + <I>c</I> = <I>c</I> +
(<I>b</I> - 7).
-->

<P>
<FONT SIZE="-1">
[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 <A HREF="#traditional">traditional logic</A> is a
derived concept in Metamath, broken down into multiple primitive steps.
<A HREF="#distinct">Distinct variable</A> conditions, which accompany certain
axioms and are inherited by theorems, forbid unsound substitutions.]
</FONT>
</P>

<P>
<B><FONT COLOR="#006633">How it works</FONT></B>
&nbsp;&nbsp;&nbsp;
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 <I>any</I> proof in the
database&mdash;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.
</P>

<P>
<CENTER>
<TABLE WIDTH="90%">
<TR>
<TD ALIGN=CENTER>
<TABLE BORDER=0 CELLSPACING=0 CELLPADDING=5 BGCOLOR="#EEFFFA">
<TR>
<TD ALIGN=CENTER>
An animated version of the 2+2=4 proof step in this section is presented
starting at 7m32s into David A. Wheeler's
<A HREF="https://www.youtube.com/watch?v=8WH4Rd4UKGE&amp;t=7m32s">Metamath
Proof Explorer:  A Modern Principia Mathematica</A>.
</TD>
</TR>
</TABLE>
</TD>
</TR>
</TABLE>
</CENTER>

<P>
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.
</P>

<P>
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.
</P>

<P>
<A NAME="figure1"></A>
<TABLE ALIGN=CENTER WIDTH="10%"><TR><TD>
<IMG BORDER=0 SRC="_proofstep.gif"
WIDTH=592 HEIGHT=369
ALT="Breakdown of a proof step. Credit: N. Megill 2003. Public domain."
TITLE="Breakdown of a proof step. Credit: N. Megill 2003. Public domain."
ALIGN=RIGHT STYLE="margin-bottom:0px">
</TD>
</TR>

<TR><TD ALIGN=CENTER>
<FONT SIZE="-1"><B>Figure 1.</B>
Step 2 of the 2p2e4 proof references step 1, which in turn "feeds" the
hypothesis of earlier theorem oveq2i (which used to be called opreq2i).  The
conclusion (assertion) of oveq2i then generates step 2 of 2p2e4.  Carefully
note the substitutions (lassoed in thin orange lines) that take place.
<BR>
<BR>

<!-- <FONT SIZE=-2 FACE="Comic Sans MS" COLOR=ORANGE>Added</FONT> -->
<FONT SIZE=-1><I>21-Mar-2007</I></FONT>

See also Paul Chapman's <A HREF="_mmbrows2p2e4.png">Metamath browser
screenshot</A>, which shows the substitutions explicitly.
</FONT>
</TD>
</TR>
</TABLE>

<P>
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 <A HREF="../index.html#pink">little <!-- pink --> colored numbers</A> can
make a higher-level view of the proof easier to grasp.)
</P>

<!-- <P><FONT COLOR="#F7941D" FACE=sans-serif><B>(1)</B></FONT> -->

<P>
<IMG SRC='_orange1circ.gif' WIDTH=19 HEIGHT=19 ALT='(1)'>
&nbsp;&nbsp;
Look at Step 2 of the proof.
In the Ref column, we see that it references a previously proved theorem,
~ oveq2i .  The theorem oveq2i requires a
hypothesis, and in the Hyp column of Step 2 we indicate that Step 1 will
satisfy (match) this hypothesis.
</P>

<P>
<IMG SRC='_orange2circ.gif' WIDTH=19 HEIGHT=19 ALT='(2)'>
&nbsp;&nbsp;
We make substitutions into the variables of the hypothesis of ~ oveq2i 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 ` A ` and the
expression "(1 + 1)" for variable ` B ` .  The middle symbol in the hypothesis
of ~ oveq2i is "=", which is a constant, and we are not allowed to substitute
anything for a constant.  Constants must match exactly.
</P>

<P>
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, <FONT
COLOR="#0000FF">blue</FONT>, <FONT COLOR="#FF0000">red</FONT>, and <FONT
COLOR="#CC33CC">purple</FONT>, 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 uppercase italic letters are variables, whereas the
symbols "(", ")", "1", "2", "=", and "+" are constants.
</P>

<P>
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.
</P>

<P>
<IMG SRC='_orange3circ.gif' WIDTH=19 HEIGHT=19 ALT='(3)'>
&nbsp;&nbsp;
In the Expression column of the Assertion box of ~ oveq2i , there are four
variables, ` A ` , ` B ` , ` C ` , and ` F ` .  Because we have already made
substitutions into the hypothesis, variables ` A ` and ` B ` have been
committed to the assignments "2" and "(1 + 1)" respectively, and we can't
change these assignments.  However, the new variables ` C ` and ` F ` are free
to be assigned with any expression we want (subject to the legal syntax
requirement described below).  By substituting "2" for ` C ` and "+" for
` F ` , we end up with (2 + 2) = (2 + (1 + 1)) that we show in the Expression
column for Step 2 of the proof of ~ 2p2e4 .
</P>

<P>
<FONT SIZE="-1">
[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-ov (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&mdash;pretend you have no
idea what a number or "+" is&mdash;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.]
</FONT>
</P>

<P>
When we first created the proof, why did we choose these particular
substitutions for ` C ` and ` F `?
The reason is simple&mdash;they make the proof work!  But how did we know
these particular substitutions should be picked, and not others?  That's
the hard part&mdash;we didn't know, nor did we know that oveq2i 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 oveq2i.  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.
</P>

<P>
Sometimes a referenced theorem (or axiom or definition) has no
hypotheses.  In that case we omit <IMG SRC='_orange1circ.gif' WIDTH=19
HEIGHT=19 ALT='(1)'> and <IMG SRC='_orange2circ.gif' WIDTH=19 HEIGHT=19
ALT='(2)'> above and immediately proceed to <IMG SRC='_orange3circ.gif'
WIDTH=19 HEIGHT=19 ALT='(3)'>. When there are multiple hypotheses, we
repeat <IMG SRC='_orange1circ.gif' WIDTH=19 HEIGHT=19 ALT='(1)'> and
<IMG SRC='_orange2circ.gif' WIDTH=19 HEIGHT=19 ALT='(2)'> for each one.
</P>

<P>
<CENTER>
<TABLE WIDTH="90%">
<TR>
<TD ALIGN=CENTER>
<TABLE BORDER=0 CELLSPACING=0 CELLPADDING=5 BGCOLOR="#EEFFFA">
<TR>
<TD ALIGN=CENTER>
<IMG SRC="_nmegill.gif" WIDTH=16 HEIGHT=19
ALT="The Floating Head of Wisdom says: "
TITLE="The Floating Head of Wisdom says: ">&nbsp;&nbsp;&nbsp;
<FONT COLOR="#F7941D">
<B>
Done!  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.
</B>
</FONT>
</TD>
</TR>
</TABLE>
</TD>
</TR>
</TABLE>
</CENTER>

<P>
You may want to practice the above procedure for a few other proof steps to
make sure you have grasped the idea.
</P>

<P>
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.
</P>

<P>
<B><FONT COLOR="#006633">Notes on substitutions</FONT></B>
&nbsp;&nbsp;&nbsp;
<MENU>

<LI>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 ` F `
in the Assertion of oveq2i, and both occurrences must be replaced with
the same expression, which is "+" in the above example.
</LI>

<LI>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).  <I>In other words you
should pretend that all variables in the theorem being proved are
constants for the purpose of figuring out the substitutions.</I> You can
see this by looking at examples such as Theorem ~ idALT .  To follow the proof
of ~ idALT , you should treat the symbol ` ph ` as if it were a
constant symbol, when you are figuring out the substitutions to make
into the variables of the referenced theorems (or axioms).
</LI>

<LI>If the variables of a referenced theorem (or axiom) 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 (or axiom)
before substituting expressions for them, to avoid confusion.  For
example, the proof of ~ idALT will be less confusing if the occurrences of
` ph ` in the referenced axioms are renamed to something else.
Specifically, you can rewrite ~ ax-1 as, say, ` ( ch -> ( ps -> ch ) ) ` .
Then, to obtain step 2 of the proof of ~ idALT , substitute "` ph `" for ` ch `
and "` ( ph -> ph ) `" for ` ps ` .
</LI>

</MENU>

<P id="legal_syntax">
<B><FONT COLOR="#006633">Legal syntax</FONT></B>
&nbsp;&nbsp;&nbsp;
There is a further requirement for Metamath 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 ` B ` 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.
</P>

<!--
<P><FONT SIZE="-1">[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 <I><FONT COLOR="#CC33CC">C</FONT></I> and 1 for
<I><FONT COLOR="#CC33CC">F</FONT></I> in oveq2i 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.
-->
<!--
If this bothers
you, consider the following analogy:  any random collection of syntactically
legal statements in a computer language constitute a valid program,
even though the program would be of little use.
-->
<!--
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.]</FONT>
</P>
-->

<P>
Similarly, blue wff variables and red setvar variables can be substituted only
with expressions that qualify as those types.
</P>

<P>
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.  This also states precisely what is being
substituted, preventing any ambiguity.
</P>

<P>
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.
</P>

<P>
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
<A HREF="../index.html#mmprog">Metamath program</A>.  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".
</P>

<P>
This is a general property of Metamath, not just of the set.mm database.
For example, step 32 of proof <tt>th1</tt> in demo database <tt>demo0.mm</tt>
must match two expressions to use theorem <tt>mp</tt>:
<UL>
<LI> ` |- ( P -> Q ) `
<LI> ` |- ( ( t + 0 ) = t -> ( ( t + 0 ) = t -> t = t ) ) `
</UL>

This could be matched many different expressions, for example:
<UL>
<LI> `P` := ` ( t + 0 ) = t `
<LI> `Q` := ` ( ( t + 0 ) = t -> t = t ) `
</UL>

or

<UL>
<LI> ` P ` := ` ( t + 0 ) = t -> ( ( t + 0 ) = t `
<LI> ` Q ` := ` t = t )`
</UL>
<!--- 4-Aug-2021 nm </P> here causes http://validator.w3.org failure -->

<P>
However, theorem <tt>mp</tt> in database <tt>demo0.mm</tt> actually has four
arguments (which you can see if you ask metamath.exe to show them).  The first
two are the substitutions, which are usually suppressed.  That is, you first
have to prove ` wff P ` , then ` wff Q ` , then ` |- P ` , then
` |- ( P -> Q  ) ` , and then theorem mp applies to derive ` |- Q ` .  If you
use metamath.exe, "show proof th1" will list only 5 steps, but with suspicious
gaps in the numbering; "show proof th1 /all" will show all the substitution
steps (which in fact make up the majority of the actual proof on disk).
</P>

<P>
A proof of ` wff P ` is equivalent to a proof that ` P ` is a well-formed
formula, and it is this that prevents invalid substitutions like
` Q ` := ` t = t ) ` ; you will not be able to prove ` wff t = t ) ` so that
proof will not work. But in any case the Metamath verifier isn't being asked to
come up with the substitution (although most metamath proof assistants will,
using unification), so no matching algorithm is necessary, only a substitution
and an equality check.
</P>

<P>
In the case of axioms and definitions, we <I>do</I> 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 <tt>set.mm</tt> (Metamath Proof Explorer) 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.
</P>

<P>
<B><FONT COLOR="#006633">Distinct variable conditions</FONT></B>
&nbsp;&nbsp;&nbsp;
Our final requirement for substitutions is described in
<A HREF="#distinct">Appendix 3:  Distinct Variables</A> 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.
</P>

<P>
<B><FONT COLOR="#006633">Class variables</FONT></B>
&nbsp;&nbsp;&nbsp;
Our example of 2+2=4, with its purple class variables, depends on a
definitional mechanism that extends the wff and setvar variables used in the
axioms to greatly simplify our presentation.  After the axiom section below, we
describe the <A HREF="#class">theory of classes</A>, which you should read to
understand how these tie into the primitive concepts used by the axioms.
</P>

<P>
<HR NOSHADE SIZE=1>
<A NAME="axioms"></A>
<B><FONT COLOR="#006633">The Axioms</FONT></B>
&nbsp;&nbsp;&nbsp;
<!--- 4-Aug-2021 nm </P> here causes http://validator.w3.org failure -->

<!--
<P><CENTER><FONT COLOR="#006633"><I>Everything should be made as simple
as possible, but not simpler.</I><BR> &mdash;attributed to Albert
Einstein</FONT></CENTER>
-->

<P>
<CENTER>
<FONT COLOR="#006633">
<I>Perfection is when there is no longer anything more to take away.</I>
<BR>
&mdash;Antoine de Saint-Exupery
</FONT>
</CENTER>

<P>
<FONT SIZE="-1">
[The material in this section is intended to be self-contained.  However, you
may also find it helpful to review <A HREF="../index.html#start">these
suggestions</A>.
<!-- and take a quick look at this
<A HREF="../mmsolitaire/mms.html#q5">summary of symbols</A>. -->
A more extensive but still informal overview is given in Chapter 3, "Abstract
Mathematics Revealed," of the <A HREF="../downloads/metamath.pdf">
<I>Metamath</I> book</A> (1.3 MB PDF file; click on the fourth bookmark in your
PDF reader).]
</FONT>
</P>

<P>
An <B>axiom</B> is a fundamental assumption that provides a starting point for
reasoning.  The axioms for (essentially) all of mathematics can be conveniently
divided into three groups:  <B>propositional calculus,</B> <B>predicate
calculus,</B> and <B>set theory</B>.  Each axiom is a string of mathematical
symbols of two kinds:  <B>constants</B>, also called <B>connectives</B>, which
we show in black; and <B>variables</B>, which we show in color.  The constants
that occur in the axioms of predicate calculus are ` ( ` , ` ) ` , ` -> ` ,
` -. ` , ` = ` , ` e. ` , and ` A. ` (left parenthesis, right parenthesis,
implies, not, equals, is a member of, for all).  The axioms of set theory may
also use some defined constants (like ` /\ ` and ` E. ` ) when this results in
a more readable assertion.
</P>

<P>
Variables are placeholders that can be substituted with other expressions
(strings of symbols).  There are two kinds of variables in the axioms,
<B>setvar variables</B> (lowercase italic letters in
<FONT COLOR="#FF0000">red</FONT>) and <B>wff ("well-formed formula")
variables</B> (lowercase Greek letters in
<FONT COLOR="#0000FF">blue</FONT>).  A wff variable can be substituted with any
expression qualifying as a wff (see below).  A setvar variable can be
substituted only with another setvar variable (in other words with an
expression of length one, whose only symbol is a setvar variable) since there
are no rules that let us construct more complex expressions for them.  We call
these "setvar variables" rather than just "set variables" to emphasize this
restriction.  The reason for this restriction is that they often serve as bound
or dummy variables in expressions, i.e. the first argument of the ` A. `
quantifier connective introduced below.  It is the same reason that you cannot
substitute say 2 for x in "the integral of x dx" to result in "the integral of
2 d2", which would be nonsense.
</P>

<P>
<FONT SIZE="-1">
[In later proofs you will see a third kind of variable, called a <B>class
variable</B>, which is shown in <FONT COLOR="#CC33CC">purple</FONT> (usually as
uppercase italic letters) and is a kind of generalization of the setvar
variable that can be substituted with expressions such as 2 or ` ( _pi + 3 ) `.
The <A HREF="#class">theory of classes</A> will be discussed in the next
section.]
</FONT>
</P>

<P>
Following the tradition in the literature, we use italic Greek letters for wff
variables and lower-case italic letters for setvar variables.
</P>

<P>
<FONT SIZE="-1">
[If you use a monochrome display or printout, or are colorblind, the red
variables are lowercase italic letters, the purple ones uppercase italic, and
the blue ones italic Greek.   Sometimes we use mathematical symbols (such as +)
as class variables, and in that case they are distinguished by both the purple
color and a dotted underline.  In all cases, the colors are not necessary to
disambiguate the symbols.  You can see the list of all symbols including
variables on the <A HREF="mmascii.html">ASCII Symbol Equivalents</A> page.]
</FONT>
</P>

<P>
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
<B>set</B> in set theory.  The red setvar variables represent arbitrary sets
such as these. (You can't substitute the expressions for these sets directly
into the setvars, as discussed above, but must use the setvars as part of a
formula that specifies the properties of these sets indirectly.  Our theory of
classes in the next section makes direct substitutions possible, giving us an
often more convenient mechanism for practical work.)
</P>

<P>
<I>A set can be equal to another set, can be contained in another set, and can
contain other sets.</I>
<!-- ("Is contained in," "is a member of," "is an element of," and "belongs to"
mean the same thing.) -->
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&mdash;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 in the presence of the ZFC axioms.  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.  (Recall that a setvar variable can only be replaced with another
setvar variable, so we cannot replace a setvar variable with say the symbol
"2".  Manipulation of such symbols uses the definitional mechanism we will
introduce in the <A HREF="#class">Theory of Classes</A> section below.)
</P>

<P>  <A NAME="wffsyntax"></A>
A <B>wff</B> is an expression (string of symbols) constructed as follows.  A
starting wff either is a wff variable, or it consists of two setvar variables
connected with either ` = ` ("equals," "is identical to") or ` e. ` ("is an
element of," "is a member of," "belongs to," "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
` A. ` ("for all," "for each," "for every") and a setvar variable to form a new
wff.
&nbsp;
<I>To summarize:</I>
If ` ph ` is a wff variable and ` x ` and ` y ` are setvar variables, then
` ph ` , ` x = y ` , and ` x e. y ` are (starting) wffs.  If ` ph ` and ` ps `
are wffs and ` x ` is a setvar variable, then ` ( ph -> ps ) ` , ` -. ph ` ,
and ` A. x ph ` are also wffs.
</P>

<P>
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.
</P>

<P>
The axioms below are examples of wffs.  Each page describing an axiom, for
example ~ ax-12 , 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.
</P>

<!--
<P>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.
-->

<P>
<I>Wffs are either true or false,</I> depending on what is assigned to the
variables they contain.  For example, the wff ` x = y ` is true if ` x ` and
` y ` stand for the same set and false otherwise&mdash;there is no in-between.
</P>

<P>
An <B>axiom</B> (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 <B>inference rule</B> (example: ~ ax-mp ) consists of one or
more wffs called <B>hypotheses</B>, together with a wff called the
<B>conclusion</B> (which on our web pages with proofs we also call its
<B>assertion</B>) that we postulate to be true provided the hypotheses are
true.  A <B>proof</B> 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 <B>theorem</B> (example:
~ idALT ).  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.
</P>

<P>
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 <B>derived inference rule</B> or <B>deduction</B>.  In a
derived inference rule, a proof is a sequence steps each of which is a
substitution instance of an axiom, a hypothesis, or a substitution instance of
an inference rule applied to previous steps.  (Note that a proof with nothing
but references to hypotheses still qualifies as a proof, even though neither
axioms nor inference rules are involved.  For example, the unusual derived
inference rule ~ a1ii is proved before we even introduce the first axiom!)
</P>

<P>
<A NAME="scaxioms"></A><B><FONT COLOR="#006633">Propositional
calculus</FONT></B> deals with general truths about wffs regardless of how they
are constructed.  The simplest propositional truth is "` ( ph -> ` ` ph ) `",
which can be read "if something is true, then it is true"&mdash;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 ` ph ` with a more
specific wff to give us, for example, "` ( x ` ` = ` ` y ` ` -> ` ` x ` ` = `
` y ) `".  (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 .)
</P>

<!--
<P>In a formula, all occurrences of a given variable must be simultaneously
substituted with a given expression, just as in high-school algebra where we
must substitute 3 for <I>both</I> occurrences of <I>b</I> when we conclude
<I>a</I> + 3 = 3 + <I>a</I> from
<I>a</I> + <I>b</I> = <I>b</I> + <I>a</I>&mdash;it is not legal to conclude
<I>a</I> + 3 = <I>b</I> + <I>a</I>.  Similarly, we cannot conclude
"` ( ph -> x = y ) `" from "` ( ph -> ph ) `".
</P>
-->

<P>
Our system of propositional calculus consists of three axioms and the modus
ponens inference rule.  It is attributed to Jan &#321;ukasiewicz (pronounced
<I>woo-kah-SHAY-vitch</I>) and was popularized by Alonzo Church, who called it
system P<SUB>2</SUB>.
<I>(Thanks to Ted Ulrich for this information.)</I>
</P>

<P>
<CENTER>
<TABLE BORDER CELLSPACING=0 BGCOLOR="#EEFFFA" SUMMARY="Axioms of propositional
calculus">
<CAPTION><B>Axioms of propositional calculus</B></CAPTION>

<TR ALIGN=LEFT><TD> <A HREF="ax-1.html"> Axiom <I>Simp</I></A></TD> <TD
NOWRAP><FONT COLOR="#006633"><B>ax-1</B></FONT></TD> <TD> ` |- ( ph `
` -> ( ps -> ph ) ) ` </TD></TR>
<TR ALIGN=LEFT><TD><A HREF="ax-2.html">Axiom <I>Frege</I></A></TD> <TD
NOWRAP><FONT COLOR="#006633"><B>ax-2</B></FONT></TD>

<TD> ` |- ( ( ph -> ( ps -> ch ) ) -> ( ( ph -> ps ) -> ( ph -> ch ) ) ) `
</TD>
</TR>
<TR ALIGN=LEFT><TD>
<A HREF="ax-3.html">Axiom <I>Transp</I></A></TD>
<TD NOWRAP>
<FONT COLOR="#006633"><B>ax-3</B></FONT>
</TD>

<TD>
` |- ( ( -. ph -> -. ps ) -> ( ps -> ph ) ) `
</TD>
</TR>
<TR ALIGN=LEFT>
<TD><A HREF="ax-mp.html">Rule of Modus Ponens</A></TD>
<TD NOWRAP><FONT COLOR="#006633"><B>ax-mp</B></FONT></TD>

<TD>
` |- ph `&nbsp;&nbsp;&nbsp;` & `&nbsp;&nbsp;&nbsp;` |- ( ph -> ps ) `&nbsp;&nbsp;&nbsp;` => `&nbsp;&nbsp;&nbsp; ` |- ps `
</TD>
</TR>
</TABLE>
</CENTER>

<P>
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.
</P>

<P>
<A NAME="pcaxioms"></A>
<B><FONT COLOR="#006633">Predicate calculus</FONT></B>
introduces three new symbols, ` = ` ("equals"), ` e. ` ("is
a member of"), and ` A. ` ("for all").  The first two are called "predicates."
A predicate specifies a true or false relationship between its two arguments.
As an example, ` x = x ` always evaluates to true regardless of what ` x ` is,
as Theorem ~ equid demonstrates.  The "for all" symbol, also called the
"universal quantifier," ranges over or "scans" all possible values of its first
(setvar variable) argument, applying them to the second (wff expression)
argument, and returns true if and only if the second argument is true for every
value of the first.  The wff ` A. x ph ` 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 "setvar variables"
are more generally called "individual variables" in predicate calculus without
set theory.)
</P>

<P>
Our axiom system is closely related to a system of Tarski (see the
<A HREF="#axiomnote">note on the axioms</A> below).  Our system is exactly
equivalent to the <A HREF="#traditional">traditional</A> 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
<A HREF="#schemes">axiom scheme</A> of the traditional system.
</P>

<CENTER>
<TABLE>
<TR>
<TD>
<TABLE BORDER CELLSPACING=0 BGCOLOR="#EEFFFA" WIDTH="100%"
SUMMARY="Axioms of predicate calculus with equality">
<CAPTION>
<B>Axioms of predicate calculus with equality - Tarski's S2</B>
</CAPTION>

<TR ALIGN=LEFT>
<TD><A HREF="ax-gen.html">Rule of Generalization</A></TD>
<TD NOWRAP><FONT COLOR="#006633"><B>ax-gen</B></FONT></TD>
<TD>
` |- ph `&nbsp;&nbsp;&nbsp;` => `&nbsp;&nbsp;&nbsp;` |- A. x ph `
</TD>
</TR>

<TR ALIGN=LEFT>
<TD><A HREF="ax-4.html">Quantified Implication</A></TD>
<TD NOWRAP><FONT COLOR="#006633"><B>ax-4</B></FONT></TD>
<TD>
` |- ( A. x ( ph -> ps ) -> ( A. x ph -> A. x ps ) ) `
</TD>
</TR>

<TR ALIGN=LEFT>
<TD><A HREF="ax-5.html">Distinctness</A></TD> <TD NOWRAP>
<FONT COLOR="#006633"><B>ax-5</B></FONT></TD>
<TD> ` |- ( ph -> A. x ph ) ` , where ` x ` does not occur in ` ph `
</TD>
</TR>

<TR ALIGN=LEFT>
<TD><A HREF="ax-6.html">Existence</A></TD>
<TD NOWRAP><FONT COLOR="#006633"><B>ax-6</B></FONT></TD>
<TD>
` |- -. A. x -. x = y `
</TD>
</TR>

<TR ALIGN=LEFT>
<TD><A HREF="ax-7.html">Equality</A></TD>
<TD NOWRAP><FONT COLOR="#006633"><B>ax-7</B></FONT></TD>
<TD>
` |- ( x = y -> ( x = z -> y = z ) ) `
</TD>
</TR>

<TR ALIGN=LEFT><TD><A HREF="ax-8.html">Left Equality for Binary Predicate</A>
</TD>
<TD NOWRAP><FONT COLOR="#006633"><B>ax-8</B></FONT></TD>
<TD>
` |- ( x = y -> ( x e. z -> y e. z ) ) `
</TD>
</TR>

<TR ALIGN=LEFT><TD><A HREF="ax-9.html">Right Equality for Binary Predicate</A>
</TD>
<TD NOWRAP><FONT COLOR="#006633"><B>ax-9</B></FONT></TD>
<TD>
` |- ( x = y -> ( z e. x -> z e. y ) ) `
</TD>
</TR>
</TABLE>

<P>
<TABLE BORDER CELLSPACING=0 BGCOLOR="#EEFFFA" WIDTH="100%"
SUMMARY="Axioms of predicate calculus with equality">
<CAPTION>
<B>Axioms of predicate calculus with equality - auxiliary schemes</B>
</CAPTION>

<TR ALIGN=LEFT>
<TD><A HREF="ax-10.html">Quantified Negation</A></TD>
<TD NOWRAP><FONT COLOR="#006633"><B>ax-10</B></FONT></TD>
<TD>
` |- ( -. A. x ph -> A. x -. A. x ph ) `
</TD>
</TR>

<TR ALIGN=LEFT>
<TD><A HREF="ax-11.html">Quantifier Commutation</A></TD>
<TD NOWRAP><FONT COLOR="#006633"><B>ax-11</B></FONT></TD>
<TD>
` |- ( A. x A. y ph -> A. y A. x ph ) `
</TD>
</TR>

<TR ALIGN=LEFT>
<TD><A HREF="ax-12.html">Substitution</A></TD>
<TD NOWRAP><FONT COLOR="#006633"><B>ax-12</B></FONT></TD>
<TD>
` |- ( x = y -> ( A. y ph -> A. x ( x = y -> ph ) ) ) `
</TD>
</TR>

<TR ALIGN=LEFT>
<TD><A HREF="ax-13.html">Quantified Equality</A></TD>
<TD NOWRAP><FONT COLOR="#006633"><B>ax-13</B></FONT></TD>
<TD>
` |- ( -. x = y -> ( y = z -> A. x ` ` y = z ) ) `
</TD>
</TR>
</TABLE>
</TD>
</TR>
</TABLE>
</CENTER>

<P>
Axiom ~ ax-5 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 <A HREF="#distinct">distinct variable</A> conditions associated with such
theorems.
</P>

<P>
The above table is divided into two groups, those from a system devised by
logician Alfred Tarski and some additional auxilliary axiom schemes.  The
latter, while logically redundant at the object language level, endow the the
system with a property called "scheme completeness", which means that any theorem (scheme) expressible in the <A
HREF="#wffsyntax">wff syntax</A> described above can be proved <I>directly</I>,
without having to resort to techniques like combining cases or induction on
formula length.  This is explained <A HREF="#compare">below</A>.
</P>

<P>
In December 2018, the axioms were renumbered and may not correspond to the
numbers in older papers, slide presentations, and websites.  See
<A HREF="#oldaxioms">Appendix 8</A> for details.
</P>

<!--
<P>(This ends the section on predicate calculus.)</P>
-->

<!--
<P>
If we are willing to live without the concept of "a setvar variable not
occurring in a wff" (or wish to do so to simplify the metalogic), we can
omit Axiom ~ ax-5 and still have a complete
system of logic.  However, ~ ax-5 provides us
with more general theorem <I>schemes</I> and can make proofs
considerably shorter.  Interestingly, if we include ~ ax-5 , then ~ ax-c14 and
~ ax-c16 become redundant (see ~ axc14 and ~ axc16 ).
</P>

<P>
To simplify the metalogic even further&mdash;with no restrictions on
substitutions at all&mdash;we can omit both ~ ax-c16
and ~ ax-5 , provided we are willing to live with
redundant "<A HREF="mmzfcnd.html#distinctors">distinctors</A>" that will
accumulate as antecedents of theorems.  Aside from this nuisance, we
would still have a complete system of logic, although it wouldn't be
a very practical one since its proofs tend be very long.
</P>
-->

<!--
<P>
In principle it is possible to reformulate the axioms with ` e. ` 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 <B>open
problem</B> (see Problem 13 on the <A HREF="../award2003.html">Workshop
Miscellany</A> page).  This problem basically involves refining and
simplifying a starting point that is already given (see me for details).
If you're interested, it would be a good way to become acquainted with
the axioms of logic while also producing something new that will live on
after you!
</P>
-->

<!--
<P>
The quantifier prefix ` A. x ` means "for all sets ` x ` ."  For example, a
very obvious truth (whose proof is ~ ax-gen applied to ~ equid ) is
` A. x x = x ` which simply means "any set ` x ` is equal to itself."  On the
other hand it states something quite profound:  it literally means <I>any</I>
set ` x ` whatsover.  This includes all mathematical objects that have
ever been discovered and that ever will be discovered, from the empty
set containing nothing, to numbers so large that they can encode all of
human knowledge, to infinite sets of integers and real numbers up
through the largest uncountable infinities.  Think about it.
</P>
-->

<P>
<B><FONT COLOR="#006633">Some definitions</FONT></B>
will simplify our presentation of the set theory axioms, although in principle
they could be eliminated.  Specifically,
<UL>
<LI>` ( ph /\ ps ) ` is an abbreviation for ` -. ( ph -> -. ps ) `</LI>
<LI>
` ( ph <-> ps ) ` is an abbreviation for ` ( ( ph -> ps ) /\ ( ps -> ph ) ) `
</LI>
<LI>` E. x ph ` is an abbreviation for ` -. A. x ` ` -. ph `</LI>
</UL>
In our database, these are introduced (in a different order) by the statements
~ df-bi (biconditional), ~ df-an (logical AND), and ~ df-ex (existential
quantifier).  To understand how definitions are introduced and justified in
Metamath, see the <A HREF="#definitions">note on definitions</A> below.  But
for our purposes, you can just <I>assume that</I> ~ df-bi , ~ df-an ,
<I>and</I> ~df-ex <I>are additional axioms</I> (which they are in some
axiomatizations of logic) so that you don't have to be concerned with their
metalogical justification.  Under this assumption, our primitive or basic
connectives are extended with ` <-> ` , ` /\ ` , and ` E. ` , 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.
<!--- 4-Aug-2021 nm </P> here causes http://validator.w3.org failure -->

<P>
<A NAME="staxioms"></A><B><FONT COLOR="#006633">Set theory</FONT></B> uses the
formalism of propositional and predicate calculus to assert properties of
arbitrary mathematical objects called "sets."  A set can be an element of
another set, and this relationship is indicated by the ` e. ` 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 <A HREF="ru.html">Russell's Paradox</A>, a discovery
that revolutionized the foundations of mathematics and logic.
</P>

<P>
Except for Extensionality, the axioms basically say, "given an arbitrary set
` x ` (and, in the cases of Replacement and Regularity, provided that an
antecedent is satisfied), there exists another set ` y ` based on or
constructed from it, with the stated properties."  (The axiom of extensionality
can also be restated this way as shown by ~ axexte .)  The individual axiom
links provide more detailed descriptions.  We derive the redundant ZF axioms of
<A HREF="axsep.html">Separation</A>, <A HREF="axnul.html">Null Set</A>, and
<A HREF="axpr.html">Pairing</A> from the others as theorems.
</P>

<P>
<A NAME="zfcaxioms"></A> In the ZFC axioms that follow, <I>all setvar
variables are assumed to be</I> <A HREF="#distinct">distinct</A>.  If you click
on their links you will see the explicit distinct variable conditions.  (There
is also an <A HREF="mmzfcnd.html">unusual formalization</A> of these axioms
that does not require that their variables be distinct.)  There are no
restrictions on the variables that may occur in wff ` ph ` below.
</P>

<P>
<CENTER><TABLE BORDER CELLSPACING=0 BGCOLOR="#EEFFFA"
SUMMARY="Zermelo-Fraenkel Set Theory with Choice (ZFC)">
<CAPTION><B>Zermelo-Fraenkel Set Theory with Choice (ZFC)</B></CAPTION>

<TR ALIGN=LEFT><TD><A HREF="ax-ext.html">Axiom of Extensionality</A></TD>
<TD NOWRAP><FONT COLOR="#006633"><B>ax-ext</B></FONT></TD>
<TD>
` |- ( A. z ( z e. x <-> z e. y ) -> x = y ) ` </TD></TR>

<TR ALIGN=LEFT><TD><A HREF="ax-rep.html">Axiom of Replacement</A></TD>
<TD NOWRAP><FONT COLOR="#006633"><B>ax-rep</B></FONT></TD>
<TD>
` |- ( A. w E. y A. z ( A. y ph -> z = y ) -> E. y A. z ( z e. y <-> `
` E. w ( w e. x /\ A. y ph ) ) ) `
</TD></TR>

<TR ALIGN=LEFT><TD><A HREF="ax-pow.html">Axiom of Power Sets</A></TD>
<TD NOWRAP><FONT COLOR="#006633"><B>ax-pow</B></FONT></TD>
<TD>
` |- E. y A. z ( A. w ( w e. z -> w e. x ) -> z e. y ) `
</TD></TR>

<TR ALIGN=LEFT><TD><A HREF="ax-un.html">Axiom of Union</A></TD>
<TD NOWRAP><FONT COLOR="#006633"><B>ax-un</B></FONT></TD>
<TD>
` |- E. y A. z ( E. w ( z e. w /\ w e. x ) -> z e. y ) `
</TD></TR>

<TR ALIGN=LEFT><TD><A HREF="ax-reg.html">Axiom of Regularity (Foundation)</A>
</TD>
<TD NOWRAP><FONT COLOR="#006633"><B>ax-reg</B></FONT></TD>
<TD>
` |- ( E. y y e. x -> E. y ( y e. x /\ A. z ( z e. y -> -. z e. x ) ) ) `
</TD></TR>

<TR ALIGN=LEFT><TD><A HREF="ax-inf.html">Axiom of Infinity</A></TD>
<TD NOWRAP><FONT COLOR="#006633"><B>ax-inf</B></FONT></TD>
<TD>
` |- E. y ( x e. y /\ A. z ( z e. y -> E. w ( z e. w /\ w e. y ) ) ) `
</TD></TR>

<TR ALIGN=LEFT><TD><A HREF="ax-ac.html">Axiom of Choice</A></TD>
<TD NOWRAP><FONT COLOR="#006633"><B>ax-ac</B></FONT></TD>
<TD>
` |- E. y A. z A. w ( ( z e. w /\ w e. x ) -> E. v A. u ( E. t ( ( u e. w /\ `
` w e. t ) /\ ( u e. t /\ t e. y ) ) <-> u = v ) ) `
</TD>
</TR>
</TABLE>
</CENTER>

<!--
<P>
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.
</P>
-->

<P>
The ZFC axioms have several equivalent formalizations, and we generally
selected ones that are the shortest to state in terms of set theory primitives.
Our ~ ax-inf and ~ ax-ac are slighly unconventional in order to make them
shorter.  We also provide ~ ax-inf2 and ~ ax-ac2 for people who want to work
with equivalents to the conventional versions.  Specifically, ~ ax-reg is
needed to derive ~ ax-inf2 from ~ ax-inf and ~ ax-ac from ~ ax-ac2 .  The
reverse derivations do not need ~ ax-reg .
</P>

<P>
There you have it, the axioms for (essentially) all of mathematics!  Marvel 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.
</P>

<P>
<I>Note.</I> Books sometimes make statements like "(essentially) all of
mathematics can be derived from the ZFC axioms."  This should not be taken
literally&mdash;there's not much you can do with these 7 axioms by themselves!
The authors are assuming that you will combine the ZFC axioms with logic (that
is, the axioms and rules of propositional and predicate calculus).  Logic and
ZFC comprise a total of 20 axioms and 2 rules in our system.
</P>

<P>
<A NAME="groth"></A><B><FONT COLOR="#006633">The Tarski&ndash;Grothendieck
Axiom</FONT></B>
&nbsp;&nbsp;&nbsp;
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&ndash;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 that axiom (Theorem ~ grothomex ) as well as
the Axiom of Choice (Theorem ~ grothac ) and the Axiom of Power Sets (Theorem
~ grothpw ).
</P>

<!--
and the Axiom of Choice (as show by Theorem ~ grothac ; see also Tarski,
"<A HREF="http://matwbn.icm.edu.pl/ksiazki/fm/fm32/fm32115.pdf">On
well-ordered subsets of any set</A> [external]", <I>Fundamenta
Mathematicae</I> 32:176-183 (1939) and Bob Solovay's 29-Mar-2008 note on
<A HREF="http://www.cs.nyu.edu/pipermail/fom/2008-March/012783.html">AC and
strongly inaccessible cardinals</A> [external] - he points out that the
mere existence of strongly inaccessible cardinals doesn't imply AC, but
rather the particular form of the Tarski&ndash;Grothendieck axiom stating their
existence).  It also implies the Axiom of Power Sets, as mentioned in
Solovay's note (see Theorem ~ grothpw ).
-->

<P>
<CENTER>
<TABLE BORDER CELLSPACING=0 BGCOLOR="#EEFFFA" SUMMARY="The
Tarski&ndash;Grothendieck axiom">
<CAPTION><B>The Tarski&ndash;Grothendieck axiom</B></CAPTION>

<TR ALIGN=LEFT>
<TD> <A HREF="ax-groth.html">The Tarski&ndash;Grothendieck Axiom</A></TD> <TD
NOWRAP><FONT COLOR="#006633"><B>ax-groth</B></FONT></TD>
<TD>
` |- E. y ( x e. y /\ A. z `
` e. y ( A. w ( w C_ z -> w e. y ) /\ E. w e. y A. v ( v C_ z -> v e. w ) ) `
` /\ A. z ( z C_ y -> ( z ~~ y \/ z e. y ) ) ) `
</TD>
</TR>
</TABLE>
</CENTER>

<P>
What else is missing from our axioms?  G&ouml;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.
</P>

<P>
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&ndash;Grothendieck Axiom, to the point of
flirting with inconsistency (although G&ouml;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.  To study such an additional axiom with Metamath, we can assert it as a
new axiom, or alternately we can simply state it as a hypothesis to any theorem
making use of it.
</P>

<P>
<HR NOSHADE SIZE=1><A NAME="class"></A>
<B><FONT COLOR="#006633">The Theory of Classes</FONT></B>
&nbsp;&nbsp;&nbsp;
In <A HREF="#figure1">Figure 1</A> above that shows part of the proof of 2+2=4,
there are some purple-colored variables such as ` A ` and ` B ` that do not
appear in any of the axioms of logic and set theory that we just presented.
Even the number 2 is a symbol (a constant) that we cannot manipulate with the
axioms, because of the rule that only setvar variables (and not constants or
other expressions) can be substituted for setvar variables.  You may at this
point feel lost, wondering how our introductory 2+2=4 example bears any
relationship at all to the axioms!  In this section, we will discuss how this
notation ties into our axioms and how to convert it to the primitive or basic
language used by the axioms.
<!--- 4-Aug-2021 nm </P> here causes http://validator.w3.org failure -->

<P>
In principle, mathematics can be done using only the setvar and wff variables
that appear in the axioms.  But the notation can be awkward to work with and is
not always intuitive for humans.  To make mathematics more practical, we extend
the set theory language with a definitional notation called the <B>theory of
classes</B>.  An expression of the form ` { x | ph } ` , where ` x ` is any
setvar variable and ` ph ` is any wff, is interchangeably called a <B>class
builder</B>, <B>class abstract[ion]</B>, <B>class term</B>, or <B>class
comprehension</B> by different authors.  We call an object that can be
represented in this form a <B>class</B> and read ` { x | ph } ` as "the class
of all ` x ` such that ` ph ` holds".  Every class is a (possibly empty)
collection of sets, although not every such collection is itself a set (see the
discussion for Theorem ~ ru ).  For example, ` { x | ( x e. ZZ /\ 2 < x ) } `
is the class (and also set) of all integers greater than 2.
</P>

<P>
We use upper-case variables ` A ` , ` B ` ,... to range over class builders and
call them <B>class variables</B>.  More generally, we let them range over any
object representing a class, such as other class variables.  (A class variable
` A `  itself can be represented with the class builder ` { x | x e. A } ` and
thus qualifies as a class; see Theorem ~ abid2 .)  Our language will now have
three kinds of variables: ` ph ` , ` ps ` ,... ranging over wffs, ` x ` ,
` y ` ,... ranging over setvars, and ` A ` , ` B ` ,... ranging over classes.
</P>

<P>
In the basic language, the ` e. ` and ` = ` connectives must connect two setvar
variables, so all starting wffs (without wff variables) are of the form
` x e. y ` and ` x ` ` = y ` .  We extend the language syntax, i.e. the
definition of a wff, by allowing ` e. ` and ` = ` to connect two expressions
representing classes, as exemplified in the three definitions below.  Theorems
involving the extended syntax are derived making use of those three
definitions.
</P>

<P>
We can construct new classes from existing ones, a property we often exploit to
define new concepts.  For example, we introduce the symbol ` u. ` and define
the <B>union</B> of two classes ` A ` and ` B ` in ~ df-un :
 ` ( A u. ` ` B ) = { x | ( x e. A \/ x e. B ) } ` .
<!--
Without class variables, we should define the union of ` { y | ph } ` and
` { y | ps } ` as ` ( { y | ph } u. { y | ps } ) = { x | ( x e. { y | ph } \/ `
` x e. { y | ps } ) } ` .  This form is rather awkward, and in practice
we use class variables and ~ df-un .
-->
Here the defined expression on the left of the "=" abbreviates the expression
on the right.  When eliminating the defined expression, we can choose for ` x `
any variable not occurring in ` A ` or ` B ` (Theorem ~ unjust ); it is a
bound or dummy variable similar to the <I>x</I> in the integral from 0 to 1 of
<I>x</I>&nbsp;d<I>x</I>.  By introducing this definition, we effectively extend
the syntax with new class expressions of the form ` ( A u. B ) ` that can be
substituted for class variables.
<!--
Since such a defined expression can obviously be eliminated (and is verified by
the mmj2 program to be sure), such an extension does not strengthen the system
with the definition eliminated.
-->
</P>

<P>
The number 2 in <A HREF="#figure1">Figure 1</A> is another example of a defined
class builder, in this case a constant with no arguments.  Our definition
~ df-2 , 2 = ` ( 1 + 1 ) ` , involves yet more defined class constants (` 1 `
defined in ~ df-1 and ` + ` defined in ~ df-add ), so it is not obviously a
class builder at this point.  But if we backtrack far enough through several
definitions, we will eventually end up with 2 = ` { x | ` ...` } ` where "..."
is a wff in the extended language.
</P>

<P>
We still need to determine what the above examples correspond to in the basic
language used by the axioms.  In essence, there is an algorithm to translate
each wff containing class builders to a unique equivalent wff in the basic
language of predicate calculus used for set theory.  Later in this section, we
will show an example using the algorithm to provide a feel for how to recover
the basic language from a wff in the extended language.
</P>

<P>
<B><FONT COLOR="#006633">The class definitions</FONT></B>
&nbsp;&nbsp;&nbsp;
The algorithm for eliminating class builders is accomplished using the
following three definitions, which in effect provide the recursive definition
of wffs containing class builders.
</P>

<P>
<CENTER>
<TABLE BORDER CELLSPACING=0 BGCOLOR="#EEFFFA"
SUMMARY="Definitions for the theory of classes">
<CAPTION><B>Definitions for the theory of classes</B></CAPTION>

<TR ALIGN=LEFT><TD> <A HREF="df-clab.html">Definition of class
abstraction</A></TD>
<TD NOWRAP><FONT COLOR="#006633"><B>df-clab</B></FONT></TD>
<TD>
` |- ( x e. { y | ph } <-> [ x / y ] ph ) `
</TD>
</TR>

<TR ALIGN=LEFT>
<TD><A HREF="dfcleq.html">Definition of class equality</A></TD>
<TD NOWRAP><FONT COLOR="#006633"><B>dfcleq</B></FONT></TD>
<TD>
<!--
` |- ( A. x ( x e. y <-> x e. z ) -> y = z ) `
&nbsp;&nbsp;&nbsp;` => `&nbsp;&nbsp;&nbsp;
-->
` |- ( A = B <-> A. x ( x e. A <-> x e. B ) ) `
</TD>
</TR>

<TR ALIGN=LEFT>
<TD><A HREF="df-clel.html">Definition of class membership</A></TD>
<TD NOWRAP><FONT COLOR="#006633"><B>df-clel</B></FONT></TD>
<TD>` |- ( A e. B <-> E. x ( x = A /\ x e. B ) ) `</TD>
</TR>
</TABLE>
</CENTER>

<P>
Definition ~ df-clab extends the ` e. ` connective, and thus the definition of
a wff, to allow a class builder on the right-hand side of the ` e. `
connective, instead of (previously) only setvar variables on each side.  Note
that the ` ph ` in ~ df-clab is a wff in the extended language and thus may
itself contain class builders.  The proper substitution denoted by
` [ x / y ] ph ` has been previously defined by ~ df-sb .
</P>

<P>
Definition ~ df-cleq extends the ` = ` connective to allow classes on both
sides.  The definition itself has a hypothesis, and above we show the derived
version ~ dfcleq with the hypothesis eliminated for practical use.  Without its
hypothesis, ~ df-cleq would produce the axiom of extensionality ~ ax-ext as a
special case and thus is not sound (is not conservative) in the context of
predicate calculus without set theory.  If we assume our class theory
definitionally extends set theory rather than just predicate calculus, the
hypothesis is unnecessary and merely provides us with a somewhat nitpicking
isolation from set theory.  Most authors do not include this hypothesis.  An
advantage of the hypothesis for us is that we must explicitly use ~ ax-ext to
satisfy it as in Theorem ~ dfcleq , meaning we can more easily determine
exactly where ~ ax-ext was used by a proof.
</P>

<P>
Definition ~ df-clel similarly extends the ` e. ` connective to allow classes
on both sides.  We do not need a hypothesis as we did for ~ df-cleq because its
instances are theorems of predicate calculus (see Theorem ~ cleljust ).
</P>

<P>
As an important special case, a setvar variable ` x ` can be considered a class
because it equals the class builder ` { y | y e. x } ` (Theorem ~ cvjust ).
This is the justification for syntax builder ~ cv , which for convenience
allows us to substitute a setvar variable directly for a class variable.  (On
the other hand, we may not substitute a class variable for a setvar variable
directly.)
</P>

<P>
<B><FONT COLOR="#006633">An example</FONT></B>
&nbsp;&nbsp;&nbsp;
To see an example of the algorithm, let us eliminate the class builder from the
(extended) wff ` { x | x = a } = b ` .  For simplicity we will assume all
setvar variable pairs are <A HREF="#distinct">distinct</A>.  Treating the
setvar variable ` b ` as a class and applying ~ dfcleq , we get
` A. y ( y e. { x | x = a } <-> y e. b ) ` .
Applying ~ df-clab , we get
` A. y ( [ y / x ] x = a <-> y e.  b ) ` .
Applying ~ df-sb , we get
` A. y ( ( x = y -> x = a ) /\ E. x ( x = y /\ x = a ) ) <-> y e. b ) ` ,
which is our final expression in the basic language of predicate calculus
(implicitly assuming we have expanded the defined connectives ` E. ` , ` /\ ` ,
` <-> `).  This expression is unique provided we have some canonical convention
for traversing the extended wff syntax tree and for naming any new variables
introduced at each step.  By the way, this can be simplified with additional
applications of predicate calculus to become ` A. y ( y = a <-> y e. b ) ` .
</P>

<!-- which we can also obtain immediately from the penultimate step by noticing
that the substitution ` [ y / x ] x = a ` evaluates to ` y = a ` . -->

<P>
Our example showed the elimination of class builders from a wff with
no class variables.  If the wff also contains class variables, these can
be converted to wff variables by substituting ` { x | ph } `
for ` A ` , ` { y | ps } ` for ` B ` ,
and so on, where ` ph ` and ` ps ` are new wff variables that don't occur in
the original extended wff.  The variables ` x ` and ` y ` are arbitrary (and
may be the same) as long as they don't conflict with any distinct variable
requirements imposed on ` A ` and ` B ` .  We then would
follow the procedure of the above example.  The description of theorem
~ eqabb goes into more detail and gives some
actual database examples where this translation takes place.
</P>

<P>
<B><FONT COLOR="#006633">Justification</FONT></B>
&nbsp;&nbsp;&nbsp;
The theory of classes can be shown to be an eliminable and conservative
extension of set theory.
</P>

<!--
<B>Eliminable</B> means that each statement of
the extended language corresponds to (can be translated to) an
equivalent statement in the primitive language.  <B>Conservative</B>
means we cannot prove anything that, when translated to the primitive
language, could not be proved from the original set theory axioms (i.e.
it does not strengthen the system).
-->

The <B>eliminability</B> property shows that for every formula in the extended
language we can build a logically equivalent formula in the basic
language; so that even if the extended language provides more ease to
convey and formulate mathematical ideas for set theory, its expressive
power is not in fact stronger than the basic language's expressive
power.

The <B>conservation</B> property shows that for every proof of a formula of
the basic language in the extended system we can build another proof of
the same formula in the basic system; so that, concerning theorems on
sets only, the deductive powers of the extended system and of the basic
system are identical.

Together, these properties mean that the extended language can be treated as a
definitional extension that is <B>sound</B>.

<P>
A rigorous justification, which we will not give here, can be found in
[<A HREF="#Levy">Levy</A>] pp. 357-366, supplementing his informal introduction
to class theory on pp. 7-17.  Two other good treatments of class theory are
provided by [<A HREF="#Quine">Quine</A>] pp. 15-21 and
[<A HREF="#TakeutiZaring">TakeutiZaring</A>] pp. 10-14.  Quine's exposition is
nicely written and very readable.  Our purple class variables are Greek letters
in [Quine], and he uses an archaic dot notation instead of parentheses, but
this is a relatively minor hurdle especially since you can compare the Metamath
versions of many of the theorems.
</P>

<P>
<B><FONT COLOR="#006633">History</FONT></B>&nbsp;&nbsp;&nbsp;
According to [<A HREF="#Levy">Levy</A>] (p. 11), the way we introduce classes
was first explicitly stated by [<A HREF="#Quine">Quine</A>] (1963), who built
on ideas stemming from Paul Bernays, particularly in Bernays' book <I>Axiomatic
Set Theory</I> (1958).  Quine uses the term "virtual classes" for the theory of
classes we use here.  Also according to Levy (pp. 11, 6, and 87), the informal
idea of using classes that cannot belong to other classes occurred to Cantor in
1899 after he became aware of the <A HREF="onprc.html">Burali-Forti paradox</A>
(1897) and the fact that Cantor's theorem <A HREF="ncanth.html">fails</A> for
the universe V (1899).  (<A HREF="ru.html">Russell's paradox</A> came later, in
1901.)  There are other (different) axiomatic set theories, including Russell's
theory of types, New Foundations, Quine's previous "Mathematical Logic" system,
and von Neumann-Bernays-G&ouml;del (NBG).  A more detailed comparison of ZFC
using Quine's virtual classes with these other axiomatic set theories can be
found in [<A HREF="#Quine">Quine</A>] (1963) pp. 15-21 and pp. 241-332.
</P>

<P>
<B><FONT COLOR="#006633">Definitions or axioms?</FONT></B>&nbsp;&nbsp;&nbsp;
Levy presents our three definitions above as axioms rather than definitions.
There is nothing wrong with this in principle, but because they are
conservative and eliminable, they do not strengthen the underlying set theory.
They just specify a mechanical transformation to and from a different but
equivalent notation.
</P>

<P>
On the other hand, they have a character that is somewhat different from
"ordinary" definitions such as ~ df-an that simply introduce a new symbol (or
unique symbol combination) to abbreviate a longer string of symbols.  All such
ordinary definitions can be verified for soundness with a relatively
straightforward algorithm that is incorporated into the mmj2 program.  But
there is no simple way to verify automatically the soundness of our three class
definitions.  Instead, we must trust the relatively involved metamathematics of
Levy's (or other authors') eliminability and conservation proofs that exist
only on paper, at least until a sufficiently sophisticated definitional
soundness checker becomes available.  The requirement of such trust makes it
tempting to call them axioms, since that would relieve us of responsibility in
the unlikely event that a flaw is uncovered in one of the
eliminability/conservation proofs.
</P>

<P>
Personally I feel that despite their formal complexity, the
eliminability/conservation properties are still in some sense "obvious,"
particularly after gaining some experience with examples such as the
above.  Moreover, calling them axioms could be slightly misleading by
suggesting that the axioms of ZFC set theory are not sufficient.  For
these reasons I chose to call them definitions, at the risk of slightly
compromising the ideal of computer-verified perfect rigor.  It is rather
trivial in the Metamath language to switch them to axioms if we want to
achieve this rigor, since the distinction between the two is merely a
naming convention of "ax-" vs.  "df-" prefixes; see the discussion below
on <A HREF="#definitions">definitions</A>.
</P>

<P>
The specific reason that the current mmj2 definitional soundness checker will
reject our three definitions for classes is that they overload (and thus in a
naive sense redefine) existing connectives.  There is one other definition in
the set.mm database that mmj2 is unable to check: ~ df-bi , which does not
connect definiendum and definiens with ` <-> ` or ` = ` .  For these four
cases, it is assumed that we are satisfied with a soundness justification
outside of Metamath or its tools, and we specify them as exceptions in mmj2's
RunParms.txt file:
</P>

<P>
<PRE>
        SetMMDefinitionsCheckWithExclusions,ax-*,df-bi,df-clab,df-cleq,df-clel
</PRE>
<!--- 4-Aug-2021 nm </P> here causes http://validator.w3.org failure -->

<P>
A skeptic is free to rename these four to be axioms (with prefix "ax-"), but
currently we consider the compromise acceptable.  Moreover, the above mmj2
statement tells us exactly which definitions we are trusting without computer
verification, so we can easily determine exactly what is being assumed.
</P>

<P>
<HR NOSHADE SIZE=1><A NAME="theorems"></A><B>
<FONT COLOR="#006633">A Theorem Sampler</FONT></B>

<!--
<P><CENTER><FONT COLOR="#006633"><I>No one shall be able to drive us from
the paradise that Cantor has created for us.</I><BR>
 &mdash;David Hilbert</FONT></CENTER></P>
-->

<P>
<CENTER>
<FONT COLOR="#006633">
<I>Set theory can be viewed as a form of exact theology.</I>
<BR>
&mdash;Rudy Rucker
</FONT>
</CENTER>

<P>
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.
</P>

<!--  Warning:  2 + 2 = 4 quickly becomes very advanced if you try to dig too
deeply (see <A HREF="#trivia">trivia</A> below). -->

The <A HREF="mmtheorems.html">Theorem List</A> shows the complete set of
theorems in the database.  You may also find the
<A HREF="mmbiblio.html">Bibliographic Cross-Reference</A> useful.

The <a href="../mm_100.html">Metamath 100</a> list  identifies the progress of
Metamath formalizations of the "top 100" theorems as tracked by Freek Wiedijk.

Many people have contributed; you can even see a
<A HREF="https://www.youtube.com/watch?v=LVGSeDjWzUo">Youtube video showing a
Gource visualization of Metamath set.mm contributions over time</A>
(and we hope that you'll become another contributor!).

<P>
<TABLE BORDER=0>
<TR><TD VALIGN=TOP WIDTH="50%">
<B>Propositional calculus</B>
<MENU>
<LI>Law of identity ~ idALT</LI>

<LI>Peirce's axiom ~ peirce</LI>

<LI>Praeclarum theorema ~ anim12</LI>

<LI>Law of excluded middle ~ exmid</LI>

<LI>Proposition *5.18 from Principia Mathematica ~ pm5.18</LI>

<LI>The consensus theorem for logic circuits ~ consensus</LI>

<LI>Meredith's astonishing single axiom ~ meredith</LI>
</MENU>
<B>Predicate calculus</B>
<MENU>
<LI>Existential and universal quantifier swap ~ 19.12</LI>

<LI>Existentially quantified implication ~ 19.35</LI>

<LI><I>x</I> = <I>x</I> ~ equid</LI>

<LI>Definition of proper substitution ~ df-sb</LI>

<LI>Double existential uniqueness ~ 2eu5</LI>

</MENU>
<B>Set theory</B>
<MENU>
<LI>Commutative law for union ~ uncom</LI>

<LI>A basic relationship between class and wff
variables ~ eqabb</LI>

<LI>Two ways of saying &quot;is a set&quot; ~ isset</LI>

<LI>Kuratowski's ordered pair definition and Theorem ~ df-op</LI>

<LI>Russell's paradox ~ ru</LI>

<LI>The value of a function ~ df-fv</LI>

<LI>Cantor's theorem ~ canth</LI>

<LI>Mathematical (finite) induction ~ findes</LI>

<LI>Peano's postulates for arithmetic:
~ peano1 ~ peano2 ~ peano3 ~ peano4 ~ peano5</LI>

</MENU>
</TD>

<TD VALIGN=TOP>
<B>Set theory (cont.)</B>
<MENU>

<LI>The existence of omega (the gateway to
"Cantor's paradise") ~ omex</LI>

<LI>Burali-Forti paradox ~ onprc</LI>

<LI>Transfinite induction ~ tfindes</LI>

<LI>Transfinite recursion ~ tfr1 ~ tfr2 ~ tfr3</LI>

<LI>The amazing recursive definition generator ~ df-rdg</LI>

<LI>Schr&ouml;der-Bernstein Theorem ~ sbth</LI>

<LI>Pigeonhole principle ~ php</LI>

<LI>Axiom of Infinity equivalent (neat!) ~ inf5</LI>

<LI>Axiom of Choice equivalent (brainteaser!) ~ ac2</LI>

<LI>Zermelo's well-ordering theorem ~ weth</LI>

<LI>Zorn's Lemma ~ zorn2</LI>

<LI>Generalized Continuum Hypothesis (GCH)
 equivalent ~ gch-kn</LI>

</MENU>
<B>Real and complex numbers</B> (<A HREF="mmcomplex.html">27
postulates</A>)
<MENU>

<LI>Archimedean property of real numbers ~ arch</LI>

<LI>Ordered pair theorem for non-negative
integers ~ nn0opthi</LI>

<LI>The square root of 2 is irrational ~ sqrt2irr</LI>

<LI>The nesting of natural numbers, integers,
rationals, reals, and complex numbers ~ nthruc</LI>

<LI>Complex number in terms of real and imaginary
parts ~ replimi</LI>

<LI>Triangle inequality for absolute
value ~ abstrii</LI>

<LI>Euler's identity ` _e ^ ( _i x. _pi ) = -u 1 `
~ eulerid</LI>

<LI>There exist infinitely many primes ~ infpn</LI>

<LI>The real numbers are uncountable ~ ruc</LI>

</MENU>
</TD></TR>
</TABLE>

<HR NOSHADE SIZE=1>
<A NAME="trivia"></A>
<B><FONT COLOR="#006633">2 + 2 = 4 Trivia</FONT></B>
&nbsp;&nbsp;&nbsp;

<P>
<CENTER>
<FONT COLOR="#006633">
<I>We used to think that if we knew one, we knew two, because one and one are
two.  We are finding that we must learn a great deal more about 'and.'</I>
<BR>
&mdash;Sir Arthur Eddington
<!-- in Mackay, The Harvest of a Quiet Eye -->
</FONT>
</CENTER>

<P>
<CENTER>
<FONT COLOR="#006633">
<I>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.</I>
<BR>
&mdash;Jacques Futrelle,
<I>Best &quot;Thinking Machine&quot; Detective Stories</I>
</FONT>
</CENTER>

<!--
Best &quot;Thinking Machine&quot; Detective Stories,
Dover Publications, Inc., New York, 1973
-->

<P>
<CENTER>
<FONT COLOR="#006633">
<I>This is a one line proof...if we start sufficiently far to the left.</I>
<BR>
&mdash;Unknown
</FONT>
</CENTER>

<!--
<P><CENTER><FONT COLOR="#006633"><I>One and one is two, and two and two
is four, and five will get you ten if you know how to work it.  </I><BR>
&mdash;Mae West</FONT></CENTER>
-->

<P>
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.
<B>Trivia Question:</B> What is the longest path for the theorem 2 + 2 = 4?
</P>

<IMG SRC="_butterfly.jpg"
ALT="Orange julia butterfly with 2+2=4 dots. Credit: N. Megill 2004. Public domain."
TITLE="Orange julia butterfly with 2+2=4 dots. Credit: N. Megill 2004. Public domain."
WIDTH=102 HEIGHT=65 ALIGN=RIGHT STYLE="margin-bottom:0px">

<P>
<B>Trivia Answer:</B>
A longest path back to an axiom from 2 + 2 = 4 is <B>184 layers</B> 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.  (Hint:  hovering the mouse over the links below will
show their descriptions.)
</P>

<!-- The list below was made by hand as follows (last updated 22-Dec-2018):
1. 'show tr 2p2e4/e/ax/m a*' to determine the complex number axioms used;
  currently they are:   ax-resscn ax-1cn ax-icn ax-addcl ax-addrcl
  ax-mulcl ax-mulrcl ax-addass ax-i2m1 ax-1ne0 ax-rrecex ax-cnre
2. In a temporary copy of set.mm that will be used hereafter, after ax-cnre
   through 2p2e4, change the labels of these to eliminate the "-" e.g. change
   ax-resscn to axresscn
3. 'show tr 2p2e4/e/count' to get the basic list below
4. Change the last list entry to ax-2 instead of a2i.1.
5. Use the first line of the description in 'show statement 2p2e4/comment' etc.
   for the TITLE field.  Add "..." when line continues to next line (look
   for absence of either trailing '"' or "(Contributed").  Delete starting
   from "(Contributed" if line has "(Contributed".  Delete trailing '"'
   if any.
6. Assemble and format the information into the list below.
7. Change tilde to ~~, backquote to `` so that 'markup' won't process them
-->
<FONT SIZE=-1>
<A HREF="2p2e4.html" TITLE="Two plus two equals four.  For more information, see '2+2=4 Trivia' on the...">2p2e4</A>
&lt;- <A HREF="2cn.html" TITLE="The number 2 is a complex number.">2cn</A>
&lt;- <A HREF="2re.html" TITLE="The number 2 is real.">2re</A>
&lt;- <A HREF="1re.html" TITLE="`` 1 `` is a real number.  This used to be one of our postulates for...">1re</A>
&lt;- <A HREF="axrrecex.html" TITLE="Existence of reciprocal of nonzero real number.  Axiom 16 of 22 for real...">axrrecex</A>
&lt;- <A HREF="recexsr.html" TITLE="The reciprocal of a nonzero signed real exists.  Part of Proposition...">recexsr</A>
&lt;- <A HREF="sqgt0sr.html" TITLE="The square of a nonzero signed real is positive.">sqgt0sr</A>
&lt;- <A HREF="pn0sr.html" TITLE="A signed real plus its negative is zero.">pn0sr</A>
&lt;- <A HREF="distrsr.html" TITLE="Multiplication of signed reals is distributive.">distrsr</A>
&lt;- <A HREF="dmaddsr.html" TITLE="Domain of addition on signed reals.">dmaddsr</A>
&lt;- <A HREF="addclsr.html" TITLE="Closure of addition on signed reals.">addclsr</A>
&lt;- <A HREF="addsrpr.html" TITLE="Addition of signed reals in terms of positive reals.">addsrpr</A>
&lt;- <A HREF="enrer.html" TITLE="The equivalence relation for signed reals is an equivalence relation....">enrer</A>
&lt;- <A HREF="addcanpr.html" TITLE="Addition cancellation law for positive reals.  Proposition 9-3.5(vi) of...">addcanpr</A>
&lt;- <A HREF="ltapr.html" TITLE="Ordering property of addition.  Proposition 9-3.5(v) of [Gleason] p. 123....">ltapr</A>
&lt;- <A HREF="ltaprlem.html" TITLE="Lemma for Proposition 9-3.5(v) of [Gleason] p. 123.">ltaprlem</A>
&lt;- <A HREF="ltexpri.html" TITLE="Proposition 9-3.5(iv) of [Gleason] p. 123.">ltexpri</A>
&lt;- <A HREF="ltexprlem7.html" TITLE="Lemma for Proposition 9-3.5(iv) of [Gleason] p. 123.">ltexprlem7</A>
&lt;- <A HREF="ltaddpr.html" TITLE="The sum of two positive reals is greater than one of them.  Proposition...">ltaddpr</A>
&lt;- <A HREF="addclpr.html" TITLE="Closure of addition on positive reals.  First statement of Proposition...">addclpr</A>
&lt;- <A HREF="addclprlem2.html" TITLE="Lemma to prove downward closure in positive real addition.  Part of...">addclprlem2</A>
&lt;- <A HREF="addclprlem1.html" TITLE="Lemma to prove downward closure in positive real addition.  Part of...">addclprlem1</A>
&lt;- <A HREF="ltrnq.html" TITLE="Ordering property of reciprocal for positive fractions.  Proposition...">ltrnq</A>
&lt;- <A HREF="dmrecnq.html" TITLE="Domain of reciprocal on positive fractions.">dmrecnq</A>
&lt;- <A HREF="recclnq.html" TITLE="Closure law for positive fraction reciprocal.">recclnq</A>
&lt;- <A HREF="recidnq.html" TITLE="A positive fraction times its reciprocal is 1.">recidnq</A>
&lt;- <A HREF="recmulnq.html" TITLE="Relationship between reciprocal and multiplication on positive...">recmulnq</A>
&lt;- <A HREF="mulassnq.html" TITLE="Multiplication of positive fractions is associative.">mulassnq</A>
&lt;- <A HREF="mulerpq.html" TITLE="Multiplication is compatible with the equivalence relation.">mulerpq</A>
&lt;- <A HREF="nqereq.html" TITLE="The function `` /Q `` acts as a substitute for equivalence classes, and it...">nqereq</A>
&lt;- <A HREF="nqercl.html" TITLE="Corollary of ~~ nqereu : closure of `` /Q `` .">nqercl</A>
&lt;- <A HREF="nqerf.html" TITLE="Corollary of ~~ nqereu : the function `` /Q `` is actually a function....">nqerf</A>
&lt;- <A HREF="nqereu.html" TITLE="There is a unique element of `` Q. `` equivalent to each element of...">nqereu</A>
&lt;- <A HREF="enqer.html" TITLE="The equivalence relation for positive fractions is an equivalence...">enqer</A>
&lt;- <A HREF="mulcanpi.html" TITLE="Multiplication cancellation law for positive integers.">mulcanpi</A>
&lt;- <A HREF="nnmcan.html" TITLE="Cancellation law for multiplication of natural numbers.">nnmcan</A>
&lt;- <A HREF="nnmword.html" TITLE="Weak ordering property of ordinal multiplication.">nnmword</A>
&lt;- <A HREF="nnmord.html" TITLE="Ordering property of multiplication.  Proposition 8.19 of [TakeutiZaring]...">nnmord</A>
&lt;- <A HREF="nnmordi.html" TITLE="Ordering property of multiplication.  Half of Proposition 8.19 of...">nnmordi</A>
&lt;- <A HREF="nnaword1.html" TITLE="Weak ordering property of addition.">nnaword1</A>
&lt;- <A HREF="nnaword.html" TITLE="Weak ordering property of addition.">nnaword</A>
&lt;- <A HREF="nnaord.html" TITLE="Ordering property of addition.  Proposition 8.4 of [TakeutiZaring] p. 58,...">nnaord</A>
&lt;- <A HREF="nnaordi.html" TITLE="Ordering property of addition.  Proposition 8.4 of [TakeutiZaring]...">nnaordi</A>
&lt;- <A HREF="nnasuc.html" TITLE="Addition with successor.  Theorem 4I(A2) of [Enderton] p. 79....">nnasuc</A>
&lt;- <A HREF="onasuc.html" TITLE="Addition with successor.  Theorem 4I(A2) of [Enderton] p. 79.  (Note...">onasuc</A>
&lt;- <A HREF="frsuc.html" TITLE="The successor value resulting from finite recursive definition...">frsuc</A>
&lt;- <A HREF="rdgsucg.html" TITLE="The value of the recursive definition generator at a successor....">rdgsucg</A>
&lt;- <A HREF="rdgdmlim.html" TITLE="The domain of the recursive definition generator is a limit ordinal....">rdgdmlim</A>
&lt;- <A HREF="tfr1a.html" TITLE="A weak version of ~~ tfr1 which is useful for proofs that avoid the Axiom...">tfr1a</A>
&lt;- <A HREF="tfrlem16.html" TITLE="Lemma for finite recursion.  Without assuming ~~ ax-rep , we can show...">tfrlem16</A>
&lt;- <A HREF="tfrlem15.html" TITLE="Lemma for transfinite recursion.  Without assuming ~~ ax-rep , we can...">tfrlem15</A>
&lt;- <A HREF="tfrlem13.html" TITLE="Lemma for transfinite recursion.  If `` recs `` is a set function, then...">tfrlem13</A>
&lt;- <A HREF="tfrlem12.html" TITLE="Lemma for transfinite recursion.  Show `` C `` is an acceptable...">tfrlem12</A>
&lt;- <A HREF="tfrlem11.html" TITLE="Lemma for transfinite recursion.  Compute the value of `` C `` ....">tfrlem11</A>
&lt;- <A HREF="tfrlem10.html" TITLE="Lemma for transfinite recursion.  We define class `` C `` by extending...">tfrlem10</A>
&lt;- <A HREF="tfrlem7.html" TITLE="Lemma for transfinite recursion.  The union of all acceptable functions...">tfrlem7</A>
&lt;- <A HREF="tfrlem5.html" TITLE="Lemma for transfinite recursion.  The values of two acceptable functions...">tfrlem5</A>
&lt;- <A HREF="tfrlem2.html" TITLE="Lemma for transfinite recursion.  This provides some messy details...">tfrlem2</A>
&lt;- <A HREF="tfrlem1.html" TITLE="A technical lemma for transfinite recursion.  Compare Lemma 1 of...">tfrlem1</A>
&lt;- <A HREF="fvreseq.html" TITLE="Equality of restricted functions is determined by their values....">fvreseq</A>
&lt;- <A HREF="eqfnfv.html" TITLE="Equality of functions is determined by their values.  Special case of...">eqfnfv</A>
&lt;- <A HREF="mpteqb.html" TITLE="Bidirectional equality theorem for a mapping abstraction.  Equivalent to...">mpteqb</A>
&lt;- <A HREF="fvmpt2.html" TITLE="Value of a function given by the 'maps to' notation.">fvmpt2</A>
&lt;- <A HREF="fvmpt2i.html" TITLE="Value of a function given by the 'maps to' notation.">fvmpt2i</A>
&lt;- <A HREF="fvmpti.html" TITLE="Value of a function given in maps-to notation.">fvmpti</A>
&lt;- <A HREF="fvmptg.html" TITLE="Value of a function given in maps-to notation.">fvmptg</A>
&lt;- <A HREF="fvopab3ig.html" TITLE="Value of a function given by ordered-pair class abstraction....">fvopab3ig</A>
&lt;- <A HREF="funopfv.html" TITLE="The second element in an ordered pair member of a function is the...">funopfv</A>
&lt;- <A HREF="funbrfv.html" TITLE="The second argument of a binary relation on a function is the function's...">funbrfv</A>
&lt;- <A HREF="funeu.html" TITLE="There is exactly one value of a function.">funeu</A>
&lt;- <A HREF="funmo.html" TITLE="A function has at most one value for each argument.">funmo</A>
&lt;- <A HREF="dffun6.html" TITLE="Alternate definition of a function using 'at most one' notation....">dffun6</A>
&lt;- <A HREF="dffun6f.html" TITLE="Definition of function, using bound-variable hypotheses instead of...">dffun6f</A>
&lt;- <A HREF="dffun3.html" TITLE="Alternate definition of function.">dffun3</A>
&lt;- <A HREF="dffun2.html" TITLE="Alternate definition of a function.">dffun2</A>
&lt;- <A HREF="brcnv.html" TITLE="The converse of a binary relation swaps arguments.  Theorem 11 of...">brcnv</A>
&lt;- <A HREF="brcnvg.html" TITLE="The converse of a binary relation swaps arguments.  Theorem 11 of [Suppes]...">brcnvg</A>
&lt;- <A HREF="opelcnvg.html" TITLE="Ordered-pair membership in converse.">opelcnvg</A>
&lt;- <A HREF="brabg.html" TITLE="The law of concretion for a binary relation.">brabg</A>
&lt;- <A HREF="brabga.html" TITLE="The law of concretion for a binary relation.">brabga</A>
&lt;- <A HREF="opelopabga.html" TITLE="The law of concretion.  Theorem 9.5 of [Quine] p. 61.">opelopabga</A>
&lt;- <A HREF="copsex2g.html" TITLE="Implicit substitution inference for ordered pairs.">copsex2g</A>
&lt;- <A HREF="copsexg.html" TITLE="Substitution of class `` A `` for ordered pair `` <. x , y >. `` ....">copsexg</A>
&lt;- <A HREF="eqvinop.html" TITLE="A variable introduction law for ordered pairs.  Analog of Lemma 15 of...">eqvinop</A>
&lt;- <A HREF="opth2.html" TITLE="Ordered pair theorem.">opth2</A>
&lt;- <A HREF="opthg2.html" TITLE="Ordered pair theorem.">opthg2</A>
&lt;- <A HREF="opthg.html" TITLE="Ordered pair theorem. `` C `` and `` D `` are not required to be sets under...">opthg</A>
&lt;- <A HREF="opth.html" TITLE="The ordered pair theorem.  If two ordered pairs are equal, their first...">opth</A>
&lt;- <A HREF="opeq1d.html" TITLE="Equality deduction for ordered pairs.">opeq1d</A>
&lt;- <A HREF="opeq1.html" TITLE="Equality theorem for ordered pairs.">opeq1</A>
&lt;- <A HREF="ifbieq1d.html" TITLE="Equivalence/equality deduction for conditional operators.">ifbieq1d</A>
&lt;- <A HREF="ifeq1d.html" TITLE="Equality deduction for conditional operator.">ifeq1d</A>
&lt;- <A HREF="ifeq1.html" TITLE="Equality theorem for conditional operator.">ifeq1</A>
&lt;- <A HREF="dfif6.html" TITLE="An alternate definition of the conditional operator ~~ df-if as a simple...">dfif6</A>
&lt;- <A HREF="uneq12i.html" TITLE="Equality inference for union of two classes.">uneq12i</A>
&lt;- <A HREF="uneq12.html" TITLE="Equality theorem for union of two classes.">uneq12</A>
&lt;- <A HREF="uneq2.html" TITLE="Equality theorem for the union of two classes.">uneq2</A>
&lt;- <A HREF="uncom.html" TITLE="Commutative law for union of classes.  Exercise 6 of [TakeutiZaring]...">uncom</A>
&lt;- <A HREF="uneqri.html" TITLE="Inference from membership to union.">uneqri</A>
&lt;- <A HREF="elun.html" TITLE="Expansion of membership in class union.  Theorem 12 of [Suppes] p. 25....">elun</A>
&lt;- <A HREF="elab2g.html" TITLE="Membership in a class abstraction, using implicit substitution....">elab2g</A>
&lt;- <A HREF="elabg.html" TITLE="Membership in a class abstraction, using implicit substitution.  Compare...">elabg</A>
&lt;- <A HREF="elabgf.html" TITLE="Membership in a class abstraction, using implicit substitution.  Compare...">elabgf</A>
&lt;- <A HREF="vtoclgf.html" TITLE="Implicit substitution of a class for a setvar variable, with bound-variable...">vtoclgf</A>
&lt;- <A HREF="issetf.html" TITLE="A version of isset that does not require x and A to be distinct....">issetf</A>
&lt;- <A HREF="nfeq2.html" TITLE="Hypothesis builder for equality, special case.">nfeq2</A>
&lt;- <A HREF="nfeq.html" TITLE="Hypothesis builder for equality.">nfeq</A>
&lt;- <A HREF="nfcri.html" TITLE="Consequence of the not-free predicate.  (Note that unlike ~~ nfcr , this...">nfcri</A>
&lt;- <A HREF="nfcrii.html" TITLE="Consequence of the not-free predicate.">nfcrii</A>
&lt;- <A HREF="hblem.html" TITLE="Change the free variable of a hypothesis builder.  Lemma for ~~ nfcrii ....">hblem</A>
&lt;- <A HREF="clelsb1.html" TITLE="Substitution for the first argument of the membership predicate in an ....">clelsb1</A>
&lt;- <A HREF="sbco2.html" TITLE="A composition law for substitution.">sbco2</A>
&lt;- <A HREF="sbied.html" TITLE="Conversion of implicit substitution to explicit substitution (deduction...">sbied</A>
&lt;- <A HREF="sbie.html" TITLE="Conversion of implicit substitution to explicit substitution....">sbie</A>
&lt;- <A HREF="sbbi.html" TITLE="Equivalence inside and outside of a substitution are equivalent....">sbbi</A>
&lt;- <A HREF="sban.html" TITLE="Conjunction inside and outside of a substitution are equivalent....">sban</A>
&lt;- <A HREF="sbim.html" TITLE="Implication inside and outside of substitution are equivalent....">sbim</A>
&lt;- <A HREF="sbi2.html" TITLE="Introduction of implication into substitution.">sbi2</A>
&lt;- <A HREF="sbn.html" TITLE="Negation inside and outside of substitution are equivalent.">sbn</A>
&lt;- <A HREF="dfsb3.html" TITLE="An alternate definition of proper substitution ~~ df-sb that uses only...">dfsb3</A>
&lt;- <A HREF="dfsb2.html" TITLE="An alternate definition of proper substitution that, like ~~ df-sb , mixes...">dfsb2</A>
&lt;- <A HREF="sb4.html" TITLE="One direction of a simplified definition of substitution when variables...">sb4</A>
&lt;- <A HREF="equs5.html" TITLE="Lemma used in proofs of substitution properties.">equs5</A>
&lt;- <A HREF="axc15.html" TITLE="Derivation of set.mm's original ~~ ax-c15 from ~~ ax-c11n and the shorter...">axc15</A>
&lt;- <A HREF="ax13a2.html" TITLE="Derive ~~ ax-c15 from a hypothesis in the form of ~~ ax-12 . ~~ ax-c11n and...">ax13a2</A>
&lt;- <A HREF="ax13v2.html" TITLE="Recovery of ~~ ax-c15 from ~~ ax12v .  This proof uses ~~ ax-c11n and...">ax13v2</A>
&lt;- <A HREF="dveeq2.html" TITLE="Quantifier introduction when one pair of variables is distinct.  Revised...">dveeq2</A>
&lt;- <A HREF="ax12lem3.html" TITLE="Lemma for ~~ dveeq2 .  This lemma is equivalent to ~~ ax13v with one...">ax12lem3</A>
&lt;- <A HREF="19.36v.html" TITLE="Special case of Theorem 19.36 of [Margaris] p. 90.">19.36v</A>
&lt;- <A HREF="19.36.html" TITLE="Theorem 19.36 of [Margaris] p. 90.">19.36</A>
&lt;- <A HREF="19.9.html" TITLE="A wff may be existentially quantified with a variable not free in it....">19.9</A>
&lt;- <A HREF="19.9h.html" TITLE="A wff may be existentially quantified with a variable not free in it....">19.9h</A>
&lt;- <A HREF="19.9t.html" TITLE="A closed version of ~~ 19.9 .">19.9t</A>
&lt;- <A HREF="19.9ht.html" TITLE="A closed version of ~~ 19.9 .">19.9ht</A>
&lt;- <A HREF="a10e.html" TITLE="Abbreviated version of ~~ axc7 .">a10e</A>
&lt;- <A HREF="axc7.html" TITLE="Show that the original axiom ~~ ax-c7 can be derived from ~~ ax-10 and...">axc7</A>
&lt;- <A HREF="sp.html" TITLE="Specialization.  A universally quantified wff implies the wff without a...">sp</A>
&lt;- <A HREF="19.8a.html" TITLE="If a wff is true, it is true for at least one instance.  Special case of...">19.8a</A>
&lt;- <A HREF="equcoms.html" TITLE="An inference commuting equality in antecedent.  Used to eliminate the...">equcoms</A>
&lt;- <A HREF="equcomi.html" TITLE="Commutative law for equality.  Lemma 3 of [KalishMontague] p. 85.  See...">equcomi</A>
&lt;- <A HREF="equid.html" TITLE="Identity law for equality.  Lemma 2 of [KalishMontague] p. 85.  See also...">equid</A>
&lt;- <A HREF="eximii.html" TITLE="Inference associated with ~~ eximi .">eximii</A>
&lt;- <A HREF="eximi.html" TITLE="Inference adding existential quantifier to antecedent and consequent....">eximi</A>
&lt;- <A HREF="exim.html" TITLE="Theorem 19.22 of [Margaris] p. 90.">exim</A>
&lt;- <A HREF="alnex.html" TITLE="Theorem 19.7 of [Margaris] p. 89.">alnex</A>
&lt;- <A HREF="con2bii.html" TITLE="A contraposition inference.">con2bii</A>
&lt;- <A HREF="con1bii.html" TITLE="A contraposition inference.">con1bii</A>
&lt;- <A HREF="xchbinx.html" TITLE="Replacement of a subexpression by an equivalent one.">xchbinx</A>
&lt;- <A HREF="notbii.html" TITLE="Negate both sides of a logical equivalence.">notbii</A>
&lt;- <A HREF="notbi.html" TITLE="Contraposition.  Theorem *4.11 of [WhiteheadRussell] p. 117.">notbi</A>
&lt;- <A HREF="notbid.html" TITLE="Deduction negating both sides of a logical equivalence.">notbid</A>
&lt;- <A HREF="3bitr3g.html" TITLE="More general version of ~~ 3bitr3i .  Useful for converting definitions...">3bitr3g</A>
&lt;- <A HREF="syl5bbr.html" TITLE="A syllogism inference from two biconditionals.">syl5bbr</A>
&lt;- <A HREF="syl5bb.html" TITLE="A syllogism inference from two biconditionals.">syl5bb</A>
&lt;- <A HREF="bitrd.html" TITLE="Deduction form of ~~ bitri .">bitrd</A>
&lt;- <A HREF="bitri.html" TITLE="An inference from transitive law for logical equivalence.">bitri</A>
&lt;- <A HREF="sylibr.html" TITLE="A mixed syllogism inference from an implication and a biconditional....">sylibr</A>
&lt;- <A HREF="biimpri.html" TITLE="Infer a converse implication from a logical equivalence.">biimpri</A>
&lt;- <A HREF="bicomi.html" TITLE="Inference from commutative law for logical equivalence.">bicomi</A>
&lt;- <A HREF="bicom1.html" TITLE="Commutative law for equivalence.">bicom1</A>
&lt;- <A HREF="bi2.html" TITLE="Property of the biconditional connective.">bi2</A>
&lt;- <A HREF="dfbi1.html" TITLE="Relate the biconditional connective to primitive connectives.  See...">dfbi1</A>
&lt;- <A HREF="impbii.html" TITLE="Infer an equivalence from an implication and its converse.">impbii</A>
&lt;- <A HREF="bi3.html" TITLE="Property of the biconditional connective.">bi3</A>
&lt;- <A HREF="simprim.html" TITLE="Simplification.  Similar to Theorem *3.27 (Simp) of [WhiteheadRussell]...">simprim</A>
&lt;- <A HREF="impi.html" TITLE="An importation inference.">impi</A>
&lt;- <A HREF="con1i.html" TITLE="A contraposition inference.">con1i</A>
&lt;- <A HREF="nsyl2.html" TITLE="A negated syllogism inference.">nsyl2</A>
&lt;- <A HREF="mt3d.html" TITLE="Modus tollens deduction.">mt3d</A>
&lt;- <A HREF="con1d.html" TITLE="A contraposition deduction.">con1d</A>
&lt;- <A HREF="notnot1.html" TITLE="Converse of double negation.  Theorem *2.12 of [WhiteheadRussell] p. 101....">notnot1</A>
&lt;- <A HREF="con2i.html" TITLE="A contraposition inference.">con2i</A>
&lt;- <A HREF="nsyl3.html" TITLE="A negated syllogism inference.">nsyl3</A>
&lt;- <A HREF="mt2d.html" TITLE="Modus tollens deduction.">mt2d</A>
&lt;- <A HREF="con2d.html" TITLE="A contraposition deduction.">con2d</A>
&lt;- <A HREF="notnot2.html" TITLE="Converse of double negation.  Theorem *2.14 of [WhiteheadRussell] p. 102....">notnot2</A>
&lt;- <A HREF="pm2.18d.html" TITLE="Deduction based on reductio ad absurdum.">pm2.18d</A>
&lt;- <A HREF="pm2.18.html" TITLE="Proof by contradiction.  Theorem *2.18 of [WhiteheadRussell] p. 103.  Also...">pm2.18</A>
&lt;- <A HREF="pm2.21.html" TITLE="From a wff and its negation, anything is true.  Theorem *2.21 of...">pm2.21</A>
&lt;- <A HREF="pm2.21d.html" TITLE="A contradiction implies anything.  Deduction from ~~ pm2.21 ....">pm2.21d</A>
&lt;- <A HREF="a1d.html" TITLE="Deduction introducing an embedded antecedent....">a1d</A>
&lt;- <A HREF="syl.html" TITLE="An inference version of the transitive laws for implication ~~ imim2 and...">syl</A>
&lt;- <A HREF="mpd.html" TITLE="A modus ponens deduction.  A translation of natural deduction rule...">mpd</A>
&lt;- <A HREF="a2i.html" TITLE="Inference derived from Axiom ~~ ax-2 .">a2i</A>
&lt;- <A HREF="ax-2.html" TITLE="Axiom _Frege_.  Axiom A2 of [Margaris] p. 49.  One of the 3 axioms of...">ax-2</A>
</FONT>

<P>
(The list above was produced by typing the commands "read set.mm" then "show
trace_back 2p2e4 /essential /count_steps" in the
<A HREF="../index.html#mmprog">Metamath program</A>, after replacing the
references to the <A HREF="mmcomplex.html#axioms">complex number axioms</A> to
their corresponding theorems, such as "ax-rnegex" to "axrnegex".  The complex
numbers are a special case where we restate as axioms the theorems that derive
their properties, in order to reduce clutter in the axiom and definition lists
on the web pages.)
</P>

<!--
axioms the theorems that derive their properties, in order to isolate
them from their construction and also to reduce clutter on the "This
theorem was proved from axioms:"  and "This theorem depends on
definitions:" lists on the web pages.)
-->

<P>
The complete proof of 2 + 2 = 4 involves <B>2,913 subtheorems</B> including the
184 above.  (The command "show trace_back 2p2e4 /essential" will list them.)
These have a total of <B>26,323 steps</B>&mdash;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 of ZFC set theory.
(<A HREF="#2p2e4length">Later</A> we will compare Metamath's proof length to
that of formal proofs defined in logic textbooks.)
</P>

<P>
One of the reasons that the proof of 2 + 2 = 4 is so long is that 2 and 4 are
complex numbers&mdash;i.e. we are really proving (2+0i) + (2+0i) =
(4+0i)&mdash;and these have a complicated construction (see the
<A HREF="mmcomplex.html#axioms">Axioms for Complex Numbers</A>) 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 <I>Introduction to Axiomatic Set Theory</I> (and its predicate
calculus prerequisite) to obtain natural number (finite ordinal) arithmetic,
followed by essentially all of Landau's 136-page <I>Foundations of
Analysis</I>.
</P>

<P>
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.
</P>

<!--
, ~ 1p1e2 (shown
primarily to support a lame attempt at humor, with apologies to
frequent contributor Mel O'Cat).
-->

In <I>Principia Mathematica</I>, 1 and 2 are <I>cardinal</I>

<!-- numbers rather than
<I>real</I>
-->

numbers, so its proof of 1 + 1 = 2 is different:  see

<!--
Theorems ~ pm54.43 and
-->

~ dju1p1e2 for a translation into modern
notation.

<!--
We can also use the simpler natural numbers of ordinal arithmetic, which
are limited to the integers 0, 1, 2,...  . Although we haven't defined
the ordinal number 4 (because it hasn't been needed yet) and thus can't
show 2 + 2 = 4, the theorem 1 + 1 = 2 for ordinals is ~ o1p1e2 .
This theorem requires only 1,518
subtheorems with a total of 11,086 steps for its proof.
-->

<P>
<HR NOSHADE SIZE=1><A NAME="axiomnote"></A>
<B><FONT COLOR="#006633">Appendix 1:  A Note on the Axioms</FONT></B>
&nbsp;&nbsp;&nbsp;
The Metamath axiom system defined in set.mm is founded on a simplified
formalization of predicate calculus with equality published by logician Alfred
Tarski in 1965 (see [<A HREF="#Tarski">Tarski</A>], system S2 mentioned in the
last paragraph of p. 77; reproduced as system S3 in Section 6 of
[<A HREF="#bibmegill">Megill</A>]). Tarski's system is exactly equivalent to
the <A HREF="#traditional">traditional</A> textbook formalization, but (by
clever use of equality axioms) it eliminates the latter's primitive notions of
"proper substitution" and "free variable," replacing them with direct
substitution and the notion of a variable not occurring in a formula (which we
express with <A HREF="#distinct">distinct variable</A> conditions).
<!--- 4-Aug-2021 nm </P> here causes http://validator.w3.org failure -->

<P>
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"
[<A HREF="#Tarski">Tarski</A>, p. 61].
</P>

<!--
<P>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.
-->

<P>
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 some theorem schemes from his axioms, their
proofs require
<!--
nontrivial and somewhat ad hoc
-->
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.)
</P>

<P>
<A NAME="simplemetalogic"></A>
The Metamath axiom system (shown as <A HREF="#scaxioms">ax-1 through ax-13</A>
above) extends Tarski's system to eliminate this difficulty.  The additional
axiom schemes (as we will call them in this section; see below) endow Tarski's
system with a nice property we call <B>scheme completeness</B> (defined in
Remark 9.6 of [<A HREF="#bibmegill">Megill</A>] and called
"metalogical completeness" there).  As a result, we can prove
<I>any</I> theorem scheme expressable in the "simple metalogic" of Tarski's
system by using <I>only</I> Metamath's direct substitution rule applied to the
axiom system (and no other metalogical or set-theoretical notions "outside" of
the system).  <B>Simple metalogic</B> consists of schemes containing wff
metavariables (with no arguments) and/or setvar (also called "individual")
metavariables (i.e. in the form of the <A HREF="#wffsyntax">wff syntax</A>
described above), accompanied by optional conditions, each stating that two
specified setvar metavariables must be distinct or that a specified setvar
metavariable may not occur in a specified wff metavariable.  Metamath's logic
and set theory axiom and rule schemes are all examples of simple metalogic.
The schemes

<!--
~ stdpc4 , ~ stdpc5 , and ~ stdpc7
-->

of <A HREF="#traditional">traditional
predicate calculus with equality</A> are examples which are <I>not</I>
simple metalogic, because they use wff metavariables with
arguments and have "free for" and "not free in" side conditions.
</P>

<!--
<P><FONT SIZE="-1">[See also <A
HREF="../mmsolitaire/mms.html#q15">Question 15</A> 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.]</FONT></P>
-->

<P>
<A NAME="schemes"></A><B><FONT COLOR="#006633">Axioms vs. axiom
schemes</FONT></B>&nbsp;&nbsp;&nbsp;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 <A
HREF="#traditional">traditional predicate calculus</A>
of textbooks) but instead should be interpreted as <B>schemes</B>, or
recipes, for generating those axioms and theorems.  In particular, the
(red) "setvar variables" in Metamath's axioms are <I>not</I> 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&mdash;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.
</P>

<P>
The <I>actual</I> language (also called the object language) of first-order
logic consists of starting (or primitive or atomic) wffs (well-formed formulas)
constructed from actual individual variables
<I>v</I><FONT SIZE=-1><SUB>1</SUB></FONT>,
<I>v</I><FONT SIZE=-1><SUB>2</SUB></FONT>,
<I>v</I><FONT SIZE=-1><SUB>3</SUB></FONT>,... connected by ` = ` and ` e. `
(such as
"<I>v</I><FONT SIZE=-1><SUB>2</SUB></FONT> ` = `
 <I>v</I><FONT SIZE=-1><SUB>4</SUB></FONT>"
and
"<I>v</I><FONT SIZE=-1><SUB>3</SUB></FONT> ` e. `
 <I>v</I><FONT SIZE=-1><SUB>2</SUB></FONT>"),
which are then used to build up larger wffs with the connectives ` -> ` ,
` -. ` , and ` A. ` (such as
"` ( -. `
<I>v</I><FONT SIZE=-1><SUB>2</SUB></FONT> ` = `
<I>v</I><FONT SIZE=-1><SUB>4</SUB></FONT> ` -> A. `
<I>v</I><FONT SIZE=-1><SUB>6</SUB></FONT>
<I>v</I><FONT SIZE=-1><SUB>3</SUB></FONT> ` e. `
<I>v</I><FONT SIZE=-1><SUB>2</SUB></FONT>` ) `").
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 <I>there are no
variables representing wffs.</I> Each of our axiom schemes corresponds to
(generates) an infinite set of such actual formulas that match its pattern.
For example, "(` A. `
<I>v</I><FONT SIZE=-1><SUB>1</SUB></FONT> ` -. `
<I>v</I><FONT SIZE=-1><SUB>3</SUB></FONT> ` e. `
<I>v</I><FONT SIZE=-1><SUB>2</SUB></FONT> ` -> -. `
<I>v</I><FONT SIZE=-1><SUB>3</SUB></FONT> ` e. `
<I>v</I><FONT SIZE=-1><SUB>2</SUB></FONT>)"
is an actual axiom since it matches axiom scheme ~ ax-c5 ,
"` ( A. x ph -> ph ) ` ," when we substitute
"<I>v</I><FONT SIZE=-1><SUB>1</SUB></FONT>" for "` x `" and "` -. `
 <I>v</I><FONT SIZE=-1><SUB>3</SUB></FONT> ` e. `
 <I>v</I><FONT SIZE=-1><SUB>2</SUB></FONT>" for "` ph ` ."
</P>

<P>
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 &nbsp;
"` ( ph -> ( ps -> ph ) ) `"&nbsp;
nor the more restrictive substitution instance&nbsp;
"` ( x = y -> ( x = y -> x = y ) ) `"&nbsp;
is an actual axiom&mdash;both are schemes ranging over an infinite number of
actual axioms, with fewer (in the proper subset sense) actual axioms in the
second case, of course.  An example of an actual propositional calculus axiom
is the instance&nbsp;
"` ( `
<I>v</I><FONT SIZE=-1><SUB>3</SUB></FONT> ` = `
<I>v</I><FONT SIZE=-1><SUB>5</SUB></FONT> ` -> ( A. `
<I>v</I><FONT SIZE=-1><SUB>6</SUB></FONT>
<I>v</I><FONT SIZE=-1><SUB>1</SUB></FONT> ` e. `
<I>v</I><FONT SIZE=-1><SUB>4</SUB></FONT> ` -> `
<I>v</I><FONT SIZE=-1><SUB>3</SUB></FONT> ` = `
<I>v</I><FONT SIZE=-1><SUB>5</SUB></FONT>` ) ) ` ."
</P>

<P>
<A NAME="compare"></A><B><FONT COLOR="#006633">Our axiom schemes vs.
Tarski's original axiom schemes</FONT></B>
&nbsp;&nbsp;&nbsp;
In the figure below we compare Tarski's original axiom schemes for predicate
calculus with equality (rightmost column) with the extensions that provide
our system with "<A HREF="#simplemetalogic">scheme completeness</A>."
</P>

<!-- TODO: This image should be replaced with a table -->
<!--
<TABLE ALIGN=CENTER WIDTH="10%">
<TR><TD ALIGN=CENTER><B>Metamath's axiom schemes</B></TD>
    <TD ALIGN=CENTER><B>Tarski's system S2</B></TD></TR>
<TR><TD COLSPAN=2>
<IMG BORDER=0 SRC="_predmm-vs-tarski.png" WIDTH=629 HEIGHT=272
ALT="Metamath's axiom schemes vs. Tarski's. Credit: N. Megill 2014. Public domain."
TITLE="Metamath's axiom schemes vs. Tarski's. Credit: N. Megill 2014. Public domain."
ALIGN=RIGHT STYLE="margin-bottom:0px">
</TD></TR></TABLE>
-->

<CENTER>
<TABLE BORDER CELLSPACING=0 BGCOLOR="#EEFFFA"
SUMMARY="Axioms of predicate calculus with equality">

<TR ALIGN=LEFT>
<TD NOWRAP>&nbsp;</TD>
<TD><FONT COLOR="#006633"><B>Metamath's axiom schemes</B></FONT></TD>
<TD><FONT COLOR="#006633"><B>Tarski's system S2</B></FONT></TD></TR>

<TR ALIGN=LEFT>
<TD NOWRAP> ~ ax-gen </TD>
<TD>
` |- ph ` &nbsp;&nbsp;&nbsp; ` => ` &nbsp;&nbsp;&nbsp; ` |- A. x ph `
</TD>
<TD>
` |- ph ` &nbsp;&nbsp;&nbsp; ` => ` &nbsp;&nbsp;&nbsp; ` |- A. x ph `
</TD>
</TR>

<TR ALIGN=LEFT>
<TD NOWRAP> ~ ax-4 </TD>
<TD>
` |- ( A. x ( ph -> ps ) -> ( A. x ph -> A. x ps ) ) `
</TD>
<TD>
` |- ( A. x ( ph -> ps ) -> ( A. x ph -> A. x ps ) ) `
</TD>
</TR>

<TR ALIGN=LEFT>
<TD NOWRAP> ~ ax-5 </TD>
<TD>
` |- ( ph -> A. x ph ) ` , where ` x ` does not occur in ` ph `
</TD>
<TD>
` |- ( ph -> A. x ph ) ` , where ` x ` does not occur in ` ph `
</TD>
</TR>

<TR ALIGN=LEFT>
<TD NOWRAP> ~ ax-6 </TD>
<TD>
` |- -. A. x -. x = y `
</TD>
<TD>
` |- -. A. x -. x = y ` , where ` x ` and ` y ` are distinct
</TD>
</TR>

<TR ALIGN=LEFT>
<TD NOWRAP> ~ ax-7 </TD>
<TD>
` |- ( x = y -> ( x = z -> y = z ) ) `
</TD>
<TD>
` |- ( x = y -> ( x = z -> y = z ) ) `
</TD>
</TR>

<TR ALIGN=LEFT>
<TD NOWRAP> ~ ax-8 </TD>
<TD>
` |- ( x = y -> ( x e. z -> y e. z ) ) `
</TD>
<TD>
` |- ( x = y -> ( x e. z -> y e. z ) ) `
</TD>
</TR>

<TR ALIGN=LEFT>
<TD NOWRAP> ~ ax-9 </TD>
<TD>
` |- ( x = y -> ( z e. x -> z e. y ) ) `
</TD>
<TD>
` |- ( x = y -> ( z e. x -> z e. y ) ) `
</TD>
</TR>

<TR ALIGN=LEFT>
<TD NOWRAP> ~ ax-10 </TD>
<TD>
` |- ( -. A. x ph -> A. x -. A. x ph ) `
</TD>
<TD>&nbsp;</TD>
</TR>

<TR ALIGN=LEFT>
<TD NOWRAP> ~ ax-11 </TD>
<TD>
` |- ( A. x A. y ph -> A. y A. x ph ) `
</TD>
<TD>&nbsp;</TD>
</TR>

<TR ALIGN=LEFT>
<TD NOWRAP> ~ ax-12 </TD>
<TD>
` |- ( x = y -> ( A. y ph -> A. x ( x = y -> ph ) ) ) `
</TD>
<TD>&nbsp;</TD>
</TR>

<TR ALIGN=LEFT>
<TD NOWRAP> ~ ax-13 </TD>
<TD>
` |- ( -. x = y -> ( y = z -> A. x y = z ) ) `
</TD>
<TD>&nbsp;</TD>
</TR>
</TABLE>
</CENTER>

<P>
Our extensions ~ ax-10 through ~ ax-13 are provable (outside of Metamath) as
metatheorems of Tarski's original system, meaning that they are sound (and also
logically redundant).  Specifically, all instances of our extensions not
involving wff metavariables (and with all setvar metavariables mutually
distinct) can be proved inside of Metamath from Tarski's axiom schemes; see
theorem schemes ~ ax10w , ~ ax11w , ~ ax12w , and ~ ax13w . These theorem
schemes have hypotheses that can be eliminated for such instances.  Theorem ~
ax12wdemo shows an example of how we can eliminate the hypotheses of ~ ax12w .
Finally, we combine all such instances (outside of Metamath) to result in the
metatheorem represented by our extensions.
</P>

<P>
Except for ~ ax-6 , our system includes all axiom schemes of Tarski's
system.  In the case of ~ ax-6 , Tarski's version is weaker because it
includes a distinct variable condition.  If we wish, we can also weaken
our version in this way and still have a system that is scheme-complete.
Theorem ~ ax6 shows this by deriving, in the presence of the other
axioms, our ~ ax-6 from Tarski's weaker version ~ ax6v .  However, we chose
the stronger version for our system because it is simpler to state and
easier to use.  (Technically, our ~ ax-7 , ~ ax-8 , and ~ ax-9 are
sub-schemes of a single higher-order scheme in Tarski's system, but
these three suffice to make our system complete.  Breaking them out
makes our metalogic simpler by avoiding the need for a notion of
substitution into an atomic wff.)

<P>
<A NAME="schemesubst"></A><B><FONT COLOR="#006633">Substitution
instances of schemes</FONT></B>&nbsp;&nbsp;&nbsp;
In Metamath, by
default (i.e., when no distinct variable conditions are present; see <A
HREF="#axiomnotedv">below</A>) there are no restrictions on
substitutions that may be made into a scheme, provided we honor the
metavariable types (wff variable or setvar variable).  This is called
<B>direct substitution</B>, in contrast to a more complicated "proper
substitution" used in textbook predicate calculus.  Consider, for
example, axiom scheme ~ ax-6 , which can be abbreviated as "` E. x x = y `"
(theorem scheme ~ ax6e ), "there exists (` E. `) an ` x `
such that ` x ` equals ` y ` ".  In traditional predicate
calculus, the first argument (a variable) of the quantifier
` E. ` is considered "bound" in the wff serving as its second
argument (i.e., in the quantifier's "scope"), otherwise it is
"free".  Substitutions must follow careful rules taking into account
whether the variable is bound or free at a given position.  In the
Metamath language, ` E. `
is merely a 2-place prefix connective or "operation" that evaluates to a
wff, taking a setvar variable as its first argument and a wff as its
second, with no built-in concept of bound or free.  In ~ ax6e , we place no
restriction on what actual variables may be substituted for bound metavariable
` x ` and free metavariable ` y ` .  We can even substitute them with the same
variable, seemingly at odds with the traditional rule that free and
bound variables must not clash.
<!--
In fact, ` x ` and ` y ` are metavariables and not the actual individual
variables that predicate calculus refers to.
-->
(When we do need to prohibit certain substitutions, we use "distinct variable"
conditions, which we describe below, that apply to a theorem scheme as a
whole without consideration of whether a variable's occurrence is free or
bound.  This makes figuring out what substitutions are allowed very simple.)
</P>

<P>
The expression "` E. x x = y `" is just a recipe for generating an infinite
number of actual axioms.  In an actual axiom such as "` E. `
<I>v</I><FONT SIZE=-1><SUB>3</SUB></FONT>
<I>v</I><FONT SIZE=-1><SUB>3</SUB></FONT> ` = `
<I>v</I><FONT SIZE=-1><SUB>2</SUB></FONT>," symbols
<I>v</I><FONT SIZE=-1><SUB>2</SUB></FONT> and
<I>v</I><FONT SIZE=-1><SUB>3</SUB></FONT> always represent distinct variables
by definition, because they have different names.
<!--
(This is what
traditional predicate calculus means when it says that free variable
<I>v</I><FONT SIZE=-1><SUB>2</SUB></FONT> and bound variable
<I>v</I><FONT SIZE=-1><SUB>3</SUB></FONT> must be distinct, i.e., cannot
both be substituted with a common variable.)
-->
Another axiom that results from the recipe is "` E. `
<I>v</I><FONT SIZE=-1><SUB>3</SUB></FONT>
<I>v</I><FONT SIZE=-1><SUB>3</SUB></FONT> ` = `
<I>v</I><FONT SIZE=-1><SUB>3</SUB></FONT>,"
which has a different meaning but is still perfectly sound.
<!--
(Traditional predicate calculus will say that this expression has a bound
variable <I>v</I><FONT SIZE=-1><SUB>3</SUB></FONT> and no free variables.)
-->
On the other hand, when working with the <I>actual</I> axioms there is no rule
that allows us to infer "` E. `
<I>v</I><FONT SIZE=-1><SUB>3</SUB></FONT>
<I>v</I><FONT SIZE=-1><SUB>3</SUB></FONT> ` = `
<I>v</I><FONT SIZE=-1><SUB>3</SUB></FONT>"
from "` E. `
<I>v</I><FONT SIZE=-1><SUB>3</SUB></FONT>
<I>v</I><FONT SIZE=-1><SUB>3</SUB></FONT> ` = `
<I>v</I><FONT SIZE=-1><SUB>2</SUB></FONT>":
they are independent axioms generated by the scheme.  In the actual logic, the
only rules of inference are the (infinite) specific instances of the
<A HREF="ax-mp.html">modus ponens</A> and
<A HREF="ax-gen.html">generalization</A> schemes&mdash;for example, from
"` E. ` <I>v</I><FONT SIZE=-1><SUB>3</SUB></FONT>
<I>v</I><FONT SIZE=-1><SUB>3</SUB></FONT> ` = `
<I>v</I><FONT SIZE=-1><SUB>2</SUB></FONT>" we can infer
"` A. ` <I>v</I><FONT SIZE=-1><SUB>6</SUB></FONT>` E. `
<I>v</I><FONT SIZE=-1><SUB>3</SUB></FONT>
<I>v</I><FONT SIZE=-1><SUB>3</SUB></FONT> ` = `
<I>v</I><FONT SIZE=-1><SUB>2</SUB></FONT>"
by generalization&mdash;and there is no substitution rule built in as a
primitive notion.
</P>

<P>
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"&mdash;these are all metamathematical notions at the scheme
level.
</P>

<P>
See also the text in the section header for
<A HREF="mmtheorems.html#ax6dgen">"Logical redundancy of ax-10, ax-11, ax-12,
ax-13"</A> and technical notes 2 and 3 below.
</P>

<P>
<A NAME="mmname"></A>
<B><FONT COLOR="#006633">Metamath is a metalanguage that describes first-order
logic</FONT></B>
&nbsp;&nbsp;&nbsp;
...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.
</P>

<P>
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.
</P>

<P>
Metamath's key and very important difference is that an application of its
substitution rule <I>always creates a new scheme from an old one.</I>  Metamath
works <I>only</I> with schemes and <I>never</I> with actual axioms or theorems.

For example, the schemes "` ( x = y -> x = y ) `" and
"` ( ( ps -> ph ) -> ( ps -> ph ) ) `" are two substitution instances that we
can infer from the scheme "` ( ph -> ph ) ` ."  These substitution instances
are new schemes in their own right, into which we can make further
substitutions to specialize them further if we wish.
</P>

<P>
The setvar 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
<I>Metamath</I>, 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.  <A NAME="mentioned"></A> In fact, the
Metamath language cannot even express specific, actual theorems such as "` ( `
<I>v</I><FONT SIZE=-1><SUB>1</SUB></FONT> ` = `
<I>v</I><FONT SIZE=-1><SUB>2</SUB></FONT> ` -> `
<I>v</I><FONT SIZE=-1><SUB>1</SUB></FONT> ` = `
<I>v</I><FONT SIZE=-1><SUB>2</SUB></FONT>` ) ` ."
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.
</P>

<P>
<A NAME="2p2e4length"></A>
<FONT SIZE="-1">

[As an example of the savings we achieve by using only schemes, the ~ 2p2e4
proof described in <A HREF="#trivia">2 + 2 = 4 Trivia</A> above requires 26,323
proof steps to be proved from the axioms of logic and set theory.  If we were
not allowed to use different instances of intermediate theorem schemes but had
to show a direct object-language proof, where each step is an actual axiom or a
rule applied to previous steps, the complete formal proof would have
73,983,127,856,077,147,925,897,127,298 (about 7.4 x 10^28 or 74 octillion)
proof steps.  See also the remarks for Theorem ~ 1kp2ke3k .  Note:  this
calculation ignores the expansion of statements that use class notation, which
would require extra steps.]

</FONT>
</P>

<P>
<A NAME="axiomnotedv"></A>
<B><FONT COLOR="#006633">Distinct metavariables</FONT></B>
&nbsp;&nbsp;&nbsp;
Sometimes we must place restrictions on the formulas generated by a scheme in
order to ensure their soundness, and we use <A HREF="#distinct">distinct
variable</A> conditions for this purpose.  For example, the theorem scheme
~ dtru , ` -. A. x ` ` x = y ` , has the restriction that metavariables ` x `
and ` y ` cannot be substituted with the same actual variable, otherwise we
could end up with the nonsense substitution instance "` -. A. `
<I>v</I><FONT SIZE=-1><SUB>1</SUB></FONT>
<I>v</I><FONT SIZE=-1><SUB>1</SUB></FONT> ` = `
<I>v</I><FONT SIZE=-1><SUB>1</SUB></FONT>"
which would mean "it is not true that every object
<I>v</I><FONT SIZE=-1><SUB>1</SUB></FONT> equals itself."
The substitution rule of Metamath ensures that distinct variable conditions
"propagate" from axiom schemes having such restrictions into theorem schemes
using those axiom schemes; in other words, distinct variable conditions in
axiom schemes are inherited by theorems whose proofs make use of those schemes.
</P>

<P>
<A NAME="dtru"></A>
Note that distinct variable conditions are <I>metalogical</I> conditions
imposed on certain axiom and theorem <I>schemes.</I> They have no role in the
actual logic (object language), where two actual variables with different names
are distinct by definition&mdash;simply because they have different names,
which is what "distinct" means.  Thus in an actual theorem generated by
~ dtru , such as "` -. A. ` <I>v</I><FONT SIZE=-1><SUB>1</SUB></FONT> <I>v</I>
<FONT SIZE=-1><SUB>1</SUB></FONT> = <I>v</I><FONT SIZE=-1><SUB>2</SUB></FONT>,"
it would be redundant (and meaningless) to require that <I>v</I><FONT SIZE=-1>
<SUB>1</SUB></FONT> and <I>v</I><FONT SIZE=-1><SUB>2</SUB></FONT> be distinct.
There is no danger of inferring from this the falsehood "` -. A. ` <I>v</I>
<FONT SIZE=-1><SUB>1</SUB></FONT> <I>v</I><FONT SIZE=-1><SUB>1</SUB></FONT>
= <I>v</I><FONT SIZE=-1><SUB>1</SUB></FONT>", because there is no substitution
rule in the actual language that lets us do so.
</P>

<P>As we
<!--
<A HREF="#mentioned">mentioned</A>,
-->
mentioned (three paragraphs earlier), the Metamath language itself
cannot express actual theorems such as "` -. A. `
<I>v</I><FONT SIZE=-1><SUB>1</SUB></FONT> <I>v</I><FONT
SIZE=-1><SUB>1</SUB></FONT> = <I>v</I><FONT
SIZE=-1><SUB>2</SUB></FONT>."  Instead, the distinct variable
condition on ~ dtru is enforced at the level of
theorem schemes.  In this example, we are not allowed to substitute the
same metavariable, say ` z ` , for
both ` x ` and ` y ` whenever we reference ~ dtru in a proof step.
</P>

<!--
<P><B><FONT COLOR="#006633">Metamath vs. other proof
languages</FONT></B>&nbsp;&nbsp;&nbsp; Many automated theorem
provers, such as <A
HREF="http://www.cs.unm.edu/~~mccune/otter/">Otter</A> [external],
work
with symbols that are intended to serve as names for actual variables of
logic rather than metavariables ranging over them.  Their underlying
programs usually have built-in renaming rules (based on metatheorems) that
transform actual theorems into other equivalent actual theorems as
needed, in order to satisfy free variable and proper substitution
requirements.  Metamath seems unusual in that it works directly and only
with metavariables.  This allows its proof verification
algorithm to be relatively simple.  Whether this offers any advantages
for automated
theorem proving is unknown; the Metamath program is not a theorem prover
but merely a proof verifier.
-->

<P>
<A NAME="technote"></A>
<B><FONT COLOR="#006633">Technical notes</FONT></B>
&nbsp;&nbsp;&nbsp;
<B>1.</B> For anyone interested, here are some technical notes on the [<A
HREF="#bibmegill">Megill</A>] 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 ~ axc14 .
Axiom C16' is also redundant&mdash;see Theorem ~ axc16 , whose proof was
discovered in 2006 and not
known at the time of the paper.  The somewhat strange-looking axiom C10'
( ~ ax-c10 ) was found to be equivalent to the simpler ~ ax-6 after
the paper was submitted; see Theorem ~ ax6fromc10 .  In the
proof of the scheme (or "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 .
</P>

<P>
<B>2.</B> Some people find it counter-intuitive that ~ ax-6 combines
two conceptually different axiom schemes, one where ` x ` and ` y ` are
always distinct variables (one bound, one free) and another which really
means "` E. x ` ` x = x ` ." Raph Levien calls this "bundling" (see <A
HREF="https://web.archive.org/web/20130114072059/http://wiki.planetmath.org/cgi-bin/wiki.pl/Principal_instances_of_metatheorems">"Principal
instances of metatheorems"</A> [retrieved 14-Jul-2015]; related pages
are <A
HREF="https://web.archive.org/web/20130203222517/http://wiki.planetmath.org/cgi-bin/wiki.pl/Distinctors_vs_binders">
Distinctors vs. binder</A> [retrieved 18-Apr-2016] and <A
HREF="https://groups.google.com/d/msg/metamath/hJupn_hvqu8/KJg69J8BFAEJ">
Distinct variables</A> [retrieved 18-Apr-2016]).  We chose an
axiomatization with maximally bundled axiom schemes, making them more
general, fewer in number, and easier to use.
See also the text in the section header for <A HREF="mmtheorems.html#ax6dgen">
"Logical redundancy of ax-10, ax-11, ax-12, ax-13"</A>.
</P>

<!--  It also allows us to allow
us to postpone the introduction of <A HREF="#distinct">distinct
variables</A> and to study <A HREF="#dvfreesystem">subsystems with no
distinct variable conditions</A>.  Other (longer) axiomatizations with
less bundling are possible, of course.
-->

<!-- An interesting open problem is to devise an alternate
axiomatization using only non-bundled axiom schemes (more specifically,
schemes that don't allow a bound variable to be substituted for a free
variable in its scope).  If we want the system to have scheme
completeness, we must be able to derive our bundled axiom schemes as
theorems.  For example, we can prove our bundled ~ ax-6 from the weaker
non-bundled version that requires its variables to be distinct, as theorem
~ ax6 shows, but the proof is not trivial and makes use of all of the
other axioms. -->

<P>
<B>3.</B> Tarski used the bundled axiom scheme "` E. x ` ` x = y `" in one
of his systems without requiring that ` x ` and ` y ` be distinct variables
(see [<A HREF="#KalishMontague">KalishMontague</A>], footnote on p. 81).  In
other words, he bundled it like we do to make it more general and able
to prove instances of "` E. x ` ` x = x `" without
requiring a separate axiom scheme.  On the other hand, he required that
` x ` and ` y ` be distinct in this scheme of his system S2
mentioned above, since instances of "` E. x ` ` x = x `" could be derived
in another way (see the proof of ~ equid1 ).  Tarski considered it better to
include the distinct variable condition since he wanted to show the weakest
possible axiom scheme needed for completeness, even though it made the
statement of the scheme more complex.
</P>

<P>
<B>4.</B> An interesting feature of Metamath's axiom system is that
it is <I>finitely axiomatized</I> 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 <I>most general theorem</I>
that that results.  This fact is exploited and illustrated in the <A
HREF="../mmsolitaire/mms.html">Metamath Solitaire</A> 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,
<I>without</I> 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.)
</P>

<P>
<B>5.</B> Interestingly, Raph Levien has shown (see Item 16 on the <A
HREF="../award2003.html#16">Workshop Miscellany</A> page) that in the
actual logic, if we are given "` E. ` <I>v</I><FONT SIZE=-1><SUB>3</SUB></FONT>
<I>v</I><FONT SIZE=-1><SUB>3</SUB></FONT> = <I>v</I>
<FONT SIZE=-1><SUB>3</SUB></FONT>"
as a hypothesis, it is impossible to infer from it, in the absence of
scheme ~ ax-6 , even the obvious equivalent "` E. ` <I>v</I><FONT
SIZE=-1><SUB>4</SUB></FONT> <I>v</I><FONT SIZE=-1><SUB>4</SUB></FONT> =
<I>v</I><FONT SIZE=-1><SUB>4</SUB></FONT>."
<!-- This illustrates
 that bound variable renaming (related to substitution)
 is not part of the axioms themselves
but only of the metamathematics that describes them. -->
<!-- That also shows that a single axiom
representative of ~ ax-6 is not sufficient for the
logic to be complete; we need the infinite number of axioms
corresponding to this Metamath scheme. -->
</P>

<P>
<HR NOSHADE SIZE=1><A NAME="traditional"></A><B><FONT
COLOR="#006633">Appendix 2:  Traditional Textbook Axioms of Predicate
Calculus with Equality</FONT></B>&nbsp;&nbsp;&nbsp;
<!--- 4-Aug-2021 nm </P> here causes http://validator.w3.org failure -->

<P>
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 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 and concept of two variables
being <A
HREF="#distinct">distinct</A>, 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.
</P>

<P>
For classical propositional calculus, the traditional axiom and rule
schemes are exactly the same as Metamath's axioms and rule (interpreted
as <A HREF="#schemes">schemes</A>), 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.
</P>

<P>
<CENTER>
<TABLE BORDER CELLSPACING=0 BGCOLOR="#EEFFFA"
SUMMARY="Traditional axioms of predicate calculus with equality">
<TR ALIGN=LEFT>
<TD> ~ stdpc4 </TD>
<TD> ` |- A. x ph ( x ) -> ph ( y ) ` ,
provided that ` y ` is free for ` x ` in ` ph ( x ) `
</TD>
</TR>
<TR ALIGN=LEFT>
<TD> ~ stdpc5 </TD>
<TD> ` |- A. x ( ph -> ps ) -> ( ph -> A. x ps ) ` , provided that ` x ` is not
free in ` ph ` </TD>
</TR>
<TR ALIGN=LEFT>
<TD> ~ ax-gen </TD>
<TD>` |- ph `&nbsp;&nbsp;&nbsp; ` => `&nbsp;&nbsp;&nbsp; ` |- A. x ph `</TD>
</TR>
<TR ALIGN=LEFT>
<TD> ~ stdpc6 </TD>
<TD> ` |- A. x ` ` x = x ` </TD>
</TR>
<TR ALIGN=LEFT>
<TD> ~ stdpc7 </TD>
<TD> ` |- x = y -> ( ph ( x , x ) -> ph ( x , y ) ) ` , provided that ` y ` is
free for ` x ` in ` ph ( x , x ) ` </TD>
</TR>
</TABLE>
</CENTER>

<P>Three of these axiom schemes have informal English-language
conditions on them.  These conditions are somewhat awkward to formalize
(see for example [<A HREF="#Tarski">Tarski</A>] pp. 63-67),
but they are not hard to grasp intuitively.  You can look them up in any
elementary logic book.  For example, they are explained in Hirst and
Hirst's
<A HREF="http://www.appstate.edu/~~hirstjl/primer/hirst.pdf"><I>A Primer
for Logic and Proof</I></A> [retrieved 17-Sep-2017] (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, &amp; 64 for the propositional calculus, predicate calculus, and
equality axioms respectively.
</P>

<P>
Stefan Bilaniuk's <A HREF="http://euclid.trentu.ca/math/sb/pcml/"><I>A Problem
Course in Mathematical Logic</I></A> [retrieved 21-Dec-2016], another free
on-line book, provides a more extensive study of logic.
</P>

<P>
Even though the traditional axiom system looks different from Metamath's, the
two axiom systems generate exactly the same set of <I>actual</I> theorems.
(Read about <A HREF="#schemes">schemes</A> in the previous section to
understand what "actual" means.)  Specifically, all of Metamath's axiom schemes
<A HREF="#pcaxioms">ax-4 through ax-13</A> 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.  Because people familiar with the traditional system have sometimes
felt there is something wrong with ours, particularly since it dispenses with
the alpha conversion required by proper substitution in the traditional axiom
system, this bears repeating: &nbsp;

<B>Our axiom schemes generate precisely the same object-language axioms and
rules, no more and no fewer, as the traditional schemes</B> (Theorem 5 of
[<A HREF="#Tarski">Tarski</A>], p. 78).
</P>

<P>
Although in some sense the traditional axiom schemes are more compact than
Metamath's <A HREF="#pcaxioms">ax-4 through ax-13</A> (4 schemes instead of
10), their purpose 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 <I>only</I> 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
<A HREF="#simplemetalogic">simple metalogic</A>).
</P>

<P>
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 <I>is</I> a scheme of the traditional system) with
conventions that are based on a formula's <I>logical</I> properties (rather
than its <I>structure,</I> as is the case with the traditional axioms).
</P>

<P>
To say that "` x ` is effectively not free in ` ph ` ," we can use the
hypothesis ` ph -> A. x ph ` .  This hypothesis holds in all cases where ` x `
is not free in ` ph ` in the traditional system (and in a few other cases as
well, which is why we say "effectively"&mdash;for example, the wff ` x = x `
will satisfy the hypothesis, as shown by Theorem ~ hbequid , even though ` x `
is technically free in it).

Because the idiom for "effectively not free in" is so frequently used, we
define a special logical connective, ` F/ x ph ` , that stands for
` A. x ( ph -> A. x ph ) ` .  See Definition ~ df-nf .
</P>

<P>
We can emulate "free for" through the use of our definition of proper
substitution ~ df-sb , as shown for example in the approximate equivalent to
~ stdpc4 in the table above.
</P>

<!-- In all, the traditional schemes requiring the notions of "not free
in" and "free for" can be emulated with Metamath schemes ~ stdpc4 , ~ stdpc5 ,
and ~ stdpc7 , assisted by some technical lemmas (needed
to prove, for example, theorems of the form ` ph -> A. x ph ` in order to
satisfy the hypothesis of ~ stdpc5 &mdash;in particular our hb* theorems such
as ~ hbim and also ~ ax-5 ).  -->

<P>
Both our system and the traditional system are called <B>Hilbert-style</B>
systems.  Two other approaches, called <B>natural deduction</B> and
<B>Gentzen-style</B> systems, are closely related to each other and embed the
<A HREF="mmdeduction.html"> deduction (meta)theorem</A> into its axiom system.
Natural deduction is straightforward to emulate in our Hilbert-style system by
exploiting the properties of wff metavariables, using the rules described on
the <A HREF="natded.html">deduction form and natural deduction</A> page.
</P>

<!--
<P><A NAME="tradopn"></A><B><FONT COLOR="#006633">An open
problem</FONT></B>&nbsp;&nbsp;&nbsp; Several people have asked whether
Metamath's axioms <A HREF="#pcaxioms">ax-4 through ax-13</A> can be
replaced with the more traditional-looking (and presumably more
familiar) theorems ~ stdpc4 , ~ stdpc5 , ~ stdpc6 , and ~ stdpc7 .
This would indeed result in a
<I>logically</I> complete system, in the sense that we would have
schemes for all actual axioms of predicate calculus.  However, we would
still need some of the axioms ax-c5 through ax-5 in order to achieve a
system with <I>scheme completeness</I>, so that we can eliminate the need
for informal rules outside of the system, or more specifically, so that
we can prove ax-c5 through ax-5 as theorems.  An <A
HREF="../award2003.html#17">open problem (Item 17)</A> is:  Which of the
"technical" axioms ax-c5 through ax-5 would become redundant in the
presence of the "logical" axioms stdpc4 through stdpc7?
-->

<P>
<HR NOSHADE SIZE=1><A NAME="distinct"></A>
<B><FONT COLOR="#006633">Appendix 3:  Distinct Variables</FONT></B>
&nbsp;&nbsp;&nbsp;
In logic and set theory literature, theorems (or more precisely, theorem
schemes) are often accompanied by side conditions, or provisos, written in
informal English.  Typically, these are written after the statement of the
theorem and expressed in a form such as "where ` x ` is a variable that
[satisfies some constraint]".  In order to satisfy the metalogical requirements
of <A HREF="#axiomnote">Tarski's axiom system</A> on which it is based,
Metamath implements three kinds of provisos through the use of its "distinct
variable" conditions.  These restrict what substitutions are allowed, and often
you will see a condition such as the following accompanying an axiom or theorem
(for example, ~ ax-5 and ~ dtru ):
<!--- 4-Aug-2021 nm </P> here causes http://validator.w3.org failure -->

<P>
<CENTER>Distinct variable groups:
&nbsp; ` x , y ` &nbsp; ` x , ph ` &nbsp; ` x , A `
</CENTER>

<P>
These three groups (in this example, three pairs) have the following meanings,
respectively, as side conditions of the theorem scheme or axiom scheme shown
above them:
<OL>
<LI>
where ` x ` and ` y ` may not be substituted with the same setvar variable,
</LI>
<LI>
where whatever setvar variable is substituted for ` x ` may not appear in the
wff expression substituted for ` ph ` , and
</LI>
<LI>
where whatever setvar variable is substituted for ` x ` may not appear in the
class expression substituted for ` A ` .
</LI>
</OL>
For brevity we may say more informally,
<OL>
<LI>
where ` x ` and ` y ` are distinct,
</LI>
<LI>
where ` x ` does not occur in ` ph ` , and
</LI>
<LI>
where ` x ` does not occur in ` A ` .
</LI>
</OL>

<P>
<FONT SIZE="-1">
[Actually, there is only <I>one</I> rule in the Metamath language itself: 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 setvar variable should always appear in a distinct variable pair, so these are
the only cases you will see.  Under this convention, a distinct variable pair
such as "` A , ph `" will never occur, even though technically it is not
illegal.]
</FONT>
</P>

Note that
<P>
<CENTER>
Distinct variable group: &nbsp; ` ph , x `
</CENTER>
means the same thing as
<P>
<CENTER>
Distinct variable group: &nbsp; ` x , ph `
</CENTER>

<P>
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,
<P>
<CENTER>
Distinct variable group: &nbsp; ` x , y , ph `
</CENTER>
means the same thing as
<P>
<CENTER>
Distinct variable groups: &nbsp;
` x , y ` &nbsp; ` x , ph ` &nbsp; ` y , ph `
</CENTER>

<P>
The basic rule to remember is that <B>distinct variable conditions are inherited
by substitutions</B> (that take place in a proof step).  For example, look at
Step 1 of the proof of ~ cleljustALT , which has a substitution instance of
~ ax-5 .  As you can see, ~ ax-5 requires the distinct variable pair ` x , ph ` .

Step 1  substitutes ` z ` for ` x ` and ` x e. y ` for ` ph ` .

This substitution transforms the original distinct variable requirement into
the two distinct variable pairs ` z , x ` and ` z , y ` , which will
implicitly accompany Step 1 (although not shown explicitly in step 1 of the
proof listing).  Thus, Step 1 can be read in full,
"` |- ( x e. y -> A. z x e. y ) ` where ` z , x ` are distinct and
` z , y ` are distinct".
The proof verifier will check that this requirement accompanies the final
theorem, otherwise it will flag the proof step as invalid.  You can see this
requirement in the "Distinct variable groups" list on the ~ cleljustALT page.
</P>

<P>
<A NAME="dvexample"></A>This can be confusing if you do not understand
how distinct variables conditions are inherited from referenced axioms
or theorems in order to satisfy their distinct variable conditions.
Let us consider an example (courtesy of G&eacute;rard Lang).  Naively,
one might think that ~ ax-13 (which has no
distinct variable conditions) is derivable from ~ ax-5 , arguing as follows.
Since the letter ` x ` has no occurrence in
the wff ` y = z ` , one might think that a direct
application of ~ ax-5 would give (` y = z -> A. x ` ` y = z `) as a theorem
with no distinct variable conditions, so that ~ ax-13 easily
follows by adding an antecedent with ~ a1i .
However, "distinct" does not <I>merely</I> mean that two setvar variables
have different names; it means that we also must prevent them from being
substituted with the same setvar variable in the future.  (To be precise,
they must represent object language variables with different names; see
<A HREF="#schemes">Axioms vs. axiom schemes</A> and <A
HREF="#axiomnotedv">Distinct metavariables</A> above.)  To apply ~ ax-5 ,
we must explicitly ensure that ` x ` is distinct from both
` y ` and ` z ` in ` y = z ` by adding two distinct variable conditions.
Otherwise, we could further substitute ` x ` for ` y ` to
arrive at (` x = z -> A. x x = z `); this violates the distinct variable
condition of ~ ax-5 since ` x ` <I>does</I> appear in ` x = z ` .
In fact, from ~ ax-5 we can conclude only the
very restricted Theorem ~ ax13w , which because of
its distinct variable conditions is much weaker than Axiom ~ ax-13 .
(If we omit them, the Metamath proof verifier will give an error message.)
We say that the distinct variable conditions in ~ ax13w are inherited
from ~ ax-5 .
</P>

<P>
In the Metamath language, distinct variable conditions are specified with $d
statements, placed before an assertion ($a or $p) and  in the same scope.  Each
theorem must be accompanied by those $d statements needed to satisfy all
distinct variable conditions implicitly attached the proof steps.
</P>

<P>
To get a concrete feel for distinct variable conditions, you can temporarily
comment out the "$d x z $." condition for Theorem ~ cleljustALT in the database
file set.mm.   When you try to verify the proof with the
<A HREF="../index.html#mmprog">Metamath program</A>, the resulting error
message will read as follows.  (Note that the "normal" proof format is used,
which you can convert to with "save proof cleljustALT /normal", and step 25
here corresponds to step 1 on the web page; steps 1&ndash;24 are syntax
building steps that can be seen with "show proof cleljustALT /all" while step
25 is the first essentiel step.)
<PRE>
MM> verify proof cleljustALT
cleljustALT
?Error at statement 5819, label "cleljustALT", type "$p":
      wel vz ax-5 vz vx vy elequ1 equsexhv bicomi $.
             ^^^^
There is a disjoint variable ($d) violation at proof step 25.  Assertion "ax-5"
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 condition in the
assertion being proved, "cleljustALT".
</PRE>
Such error messages can also be used to determine any missing $d statements
during proof development.  Alternately, the
<A HREF="../index.html#mmj2">mmj2</A> program will compute the necessary $d's
automatically.

<!-- To get a concrete feel for distinct
variable conditions, temporarily comment out a $d statement in a
theorem in the database file set.mm then type "read set.mm" then "verify
proof *" in the <A HREF="../index.html#mmprog">Metamath program</A> to
see the effect.  You will see a detailed explanation of the $d
violation.  If you are having trouble understanding the distinct
variable concept, you should really do this experiment to help you
understand it better.
-->
<!--- 4-Aug-2021 nm </P> here causes http://validator.w3.org failure -->

<P>
For a dynamic example of distinct variable inheritance in action, enter the
<A HREF="../mmsolitaire/mms.html#q7">first proof</A> of ` x = x ` into the
Metamath Solitaire applet, which automatically computes the distinct variable
conditions needed for a theorem being proved.  Watch the transformation of
the distinct variable condition that is inherited at the tenth step (ax-16).
</P>

<P>
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 .
</P>

<P>
<A NAME="dv-history"></A>
<CENTER>
<B><FONT COLOR="#006633">History of distinct variables</FONT></B>
</CENTER>

<P>
The idea of using distinct variable conditions in place of the more
complicated free-variable concept of <A HREF="#traditional">traditional
predicate calculus</A> was first stated by Tarski in 1951, with proofs
published in 1965 [<A HREF="#Tarski">Tarski</A>, p. 61, footnote].  It
also allows us to dispense with proper substitution as a primitive
notion in the axiom system:  "Instead of the general notion of proper
substitution we use...a much more elementary and special notion:  that
of replacement, of one variable by another, in an atomic formula."  [<A
HREF="#Tarski">Tarski</A>, p. 62].
</P>

<P>Below we show the two axiom schemes of Tarski's system that involve
distinct variable conditions, in their original form:

<TABLE ALIGN=CENTER WIDTH="10%">
<TR><TD>
 <IMG BORDER=1 SRC="_tarski-dv.gif"
WIDTH=307 HEIGHT=52
ALT="Tarski's axiom schemes with distinct variable conditions"
TITLE="Tarski's axiom schemes with distinct variable conditions"
ALIGN=RIGHT STYLE="margin-bottom:0px">
</TD></TR>
<TR><TD ALIGN=CENTER><B>Tarski's original axiom schemes with
        distinct variable conditions [<A
HREF="#Tarski">Tarski</A>, p. 75]</B></TD></TR>
</TABLE>

<P>
Tarski uses <!-- &wedge; fails w3c validator --> "` /\ `" and "&equiv;" in
place of our "` A. `" and "=" respectively (which allows him to use "=" for
the side condition of (B7)), and the notation "OC(<I>&phi;</I>)" means "the
set of all variables occurring in <I>&phi;</I>".  These two schemes are
identical to our ~ ax-5 and ~ ax6v , which are accompanied by distinct variable
conditions that can be read "where ` x ` doesn't occur in ` ph `" and "where
` x ` and ` y ` are distinct" respectively.  (Our official ~ ax-6 does not have
a distinct variable condition in order to make it simpler to state and use.)
</P>

<P>
<A NAME="dv-notes"></A>
<CENTER>
<B><FONT COLOR="#006633">Notes on distinct variables</FONT></B>
</CENTER>

<P>
<A NAME="dvnote1"></A>
<B><FONT COLOR="#006633">Note 1</FONT></B>
&nbsp;&nbsp;&nbsp;
Sometimes new or "dummy" variables are used inside of a proof that do not
appear in the theorem being proved.  On the web pages we omit them from the
"Distinct variable group(s)" list, which is intended to show only those
distinct variable conditions that need to be satisfied by any proof that
<I>references</I> the theorem.
</P>

<P>
If a proof uses dummy variables, we list them on a separate line beginning
"Dummy variables...".  For simplicity, we assume that dummy variables are
mutually distinct and distinct from all other variables, and this assumption
is indicated after the list.
</P>

<P>
Sometimes it is not strictly necessary for a dummy variable to be distinct from
certain other variables, for example when those variables do not participate in
the part of the proof using the dummy variable.  In that case, it is
<I>optional</I> whether or not we include those variables paired with the dummy
variable in $d statements in the set.mm file.  Sometimes you will see such
optional $d statements omitted, depending on the preferences of the person who
created the proof.
</P>

<P>
In principle, we could list on the web page only those pairs with dummy
variables that are actually specified to be distinct in the set.mm file.
However, that would make the "Dummy variable" list very long for some theorems
with many variables, full of gaps and hard to read.  (We used to do something
like that, and people didn't like it.)  So for simplicity, we just assume that
all possible variable pairs with dummy variables are distinct, which is a
conservative assumption that will always work.  This assumption makes it
easiest to follow the proof since you don't have to keep checking a distinct
variable list.  If you want to see which ones were actually specified for a
particular proof, you can consult the set.mm source file or use the metamath
program command 'show statement ...  /full'.
</P>

<P><A NAME="dvnote2"></A>
<B><FONT COLOR="#006633">Note 2</FONT></B>
&nbsp;&nbsp;&nbsp;
An issue that has been debated is whether the Metamath language specification
should be changed so that $d statements associated with dummy variables are
assumed implicitly.  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.  Beginners may find an explicit list helpful for understanding
proofs, since nothing is hidden.  Making it optional would complicate the
Metamath spec slightly, since it would  require an exception added to $d
verification.  If we want to use a proof step as a theorem (such as when
breaking a proof into lemmas), its subproof may fail if the step has previously
dummy variables whose $d statements are hidden.
<!-- And importantly, existing databases are
compatible with either method, whereas if someday we make $d statements
optional for dummy variables, it would be hard to go back. -->
</P>

<P>
Some people who dislike this requirement have made $d statements for dummy
variables optional for their Metamath language verifiers (although strictly
speaking this violates the current Metamath spec); an example is
<A HREF="../other.html#hmm">Hmm</A>.  There is nothing wrong with this in
principle, and we could even make <I>all</I> $d statements for theorems
optional&mdash;see <A HREF="#dvnote5">Note 5</A> below.
</P>

<P>
<A NAME="dvnote3"></A> <A NAME="allowedsubst"></A>
<B><FONT COLOR="#006633">Note 3</FONT></B>
&nbsp;&nbsp;&nbsp;
Textbooks often use the notation ` ph `(` x `) to denote that variable ` x `
may appear in a wff substituted for ` ph ` .  The Metamath language doesn't
have a notation like this, but we can achieve the logical equivalent simply by
<I>omitting</I> the distinct variable group ` x ` ,` ph ` , as the example
~ axsep shows.
</P>

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

<P>
In a sense, Metamath is opposite from the usual textbook convention: in
Metamath, <I>any</I> variable may appear in a substitution instance of a wff by
default; it is the <I>exceptions</I> that must be made explicit with distinct
variable conditions.  Keeping this in mind may make the comparison to logic
textbooks a little easier.
</P>
-->

<P>
We can reconstruct the ` ph `(` x `) notation from the distinct variable
conditions that are omitted.  On the individual web pages, this reconstruction
for wff and class variables is shown under the "Distinct variable groups" list
and called "Allowed substitution hints".  <!-- It is essentially the complement
of the distinct variable groups involving wff or class variables.  --> The
notation ` ph `(` x `) there means that ` x ` may appear (free, bound, or
both) in any expression substituted for wff variable ` ph ` .  Note that
this is an informal, unofficial notation, not part of the Metamath language.
<!-- , and shouldn't be confused with the notation ` [ x / y ] ph `
which means "the proper substitution of ` x ` for ` y `" ( ~ df-sb ).  -->
</P>

<P>
Keep in mind that the "Allowed substitution hints" are <I>not</I> necessarily a
complete list of all possible substitutions but are provided as a convenience
to help you more easily determine what substitutions are allowed, in contrast
to the "Distinct variable groups" which tell you which ones are forbidden.
There are six things to be aware of.
</P>

<P>
1. If the theorem has no "Distinct variable groups", such as ~ mpteq2ia , any
substitution at all (honoring the variable types) is permissable, so an
"Allowed substitution hints" list would be pointless and is not shown to reduce
possibly-confusing clutter.
</P>

<P>
2. If the theorem has "Distinct variable groups" and a wff or class variable is
missing from the "Allowed substitution hints", such as the ` A ` in ~ copsexg ,
it means (in this case) that neither of the setvar variables ` x ` or ` y ` may
appear in a class expression substituted for ` A ` .  It is acceptable to
substitute any class expression for ` A ` that <I>doesn't</I> contain these two
variables but possibly contains others such as ` z ` .
</P>

<P>
3. If the theorem has "Distinct variable groups" but does not have an "Allowed
substitution hints" list, such as ~ dftr5 , it means that none of the setvar
variables in the theorem or its hypotheses may appear in expressions
substituted for its wff or class variables; in this case, neither ` x ` nor
` y ` may appear in an expression substituted for ` A ` .  Other setvar
variables such as ` z ` may appear, though.  This includes any dummy variables
that may be used by the proof, since they do not appear in the theorem or its
hypotheses.
</P>

<P>
4. The list of variables in parentheses after a wff or class variable shows the
permissable setvar variables that may appear in a substitution <I>among those
in the theorem</I> (or its hypotheses).  There is nothing preventing the use of
setvar variables that do not appear in the theorem.  For example, in ~ axsep ,
` x ` and ` w ` may appear in an expression substituted for ` ph ` , but not
` y ` or ` z ` .
</P>

<P>
5. The setvar variable list in parentheses says nothing about whether those
setvar variables need to be mutually distinct.  Only the "Distinct variable
groups" list provides this information.  For example, ` ph `(` x ` ,` y `)
appears in the "Allowed substitution hints" for both ~ ralcom and ~ ralcom2 ;
` x ` and ` y ` must be distinct in the former but not the latter.
</P>

<P>
6. The hypotheses of a theorem may impose additional conditions on how the
variables in parentheses may appear in the wff or class variable.  For example,
in ~ vtoclef , although ` x ` may appear in the expression substituted for
` ph ` , it must appear in a way that allows the first hypothesis

<!--
` ( ph -> `
` A. x ph ) `
-->

` F/ x ph ` to be satisfied.
Thus ` x ` usually can't occur as a free variable in  ` ph ` because the
first hypothesis won't be satisfied.  This is in contrast to informal
textbook usage where ` ph `(` x `) typically means ` x ` occurs as a free
variable in ` ph ` .  The way to tell whether the meaning
is "may occur free or bound" or "may occur
if bound by a quantifier" is to look for a hypothesis of this form.
</P>

<!-- The list of allowed substitutions is shown only when (1) the theorem has
distinct variable conditions and (2) at least one wff or class variable may
contain one or more set variables belonging to the theorem.
Your feedback is welcome.  -->

<P>
<A NAME="dvnote4"></A>
<B><FONT COLOR="#006633">Note 4</FONT></B>
&nbsp;&nbsp;&nbsp;
Distinct variable conditions 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 ` x ` in ` A. x ph `); 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 "` A. `" 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 (wff, setvar, or class), and that any distinct
variable conditions are satisfied.  This different paradigm may take
some getting used to by someone used to traditional "proper
substitution" (which involves analyzing the scopes of bound variables
and renaming them if necessary), even though it is significantly
<I>simpler</I> than the traditional approach.  (Indeed, as described
above, this simplicity was a primary motivation for Tarski's predicate
calculus that Metamath's set.mm axioms are based on.)  Unless
otherwise restricted by a distinct variable condition, a quantified (or
any other) variable is by default <I>not necessarily distinct</I> from
other variables in the same expression, whether bound or not.  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
(particularly since
one is bound and the other is free), but in Metamath this requirement
must be made explicit.  (On the other hand, in an <I>instance</I> of
dtru in the <I>actual</I> logic, which Metamath cannot express directly,
the two variables are implicitly distinct by definition, as explained
the <A HREF="#dtru">"Distinct variables"</A> subsection of Appendix 1
above.)
</P>

<!--
<P>Another reason for confusion may be distinct variable conditions
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 condition, 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 &amp; D =&gt; 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).
</P>
-->

<P>
<A NAME="dvnote5"></A>
<B><FONT COLOR="#006633">Note 5</FONT></B>
&nbsp;&nbsp;&nbsp;
Interestingly, the
distinct variable conditions ($d statements) accompanying theorems are
theoretically redundant, because the proof verifier could in principle
infer and propagate them forward from the distinct variable conditions
of the axioms.  The <A HREF="../mmsolitaire/mms.html#q7">Metamath
Solitaire</A> applet does this, inferring both the resulting proof steps
and their distinct variable conditions as you feed it axioms to
build a proof.  (The <A HREF="../index.html#mmj2">mmj2</A> program will
also infer the necessary $d statements for a proof under development.)
The Metamath language spec, on the other hand, requires them to be
explicit partly to speed up the verifier (for example, otherwise
we couldn't
verify a proof in isolation but would have to analyze every proof it
depends on), but making them explicit also allows someone writing a
proof to easily determine by inspection the distinct variable
conditions of a theorem he or she wishes to reference.
</P>

<P>
<A NAME="dvnote6"></A>
<B><FONT COLOR="#006633">Note 6</FONT></B>
&nbsp;&nbsp;&nbsp;
Introducing unnecessary distinct variable groups in a theorem is always allowed
and doesn't affect its proof in any way; all it does is weaken the theorem so
that later theorems may also have to be weaker in order to make use of it.  We
rarely do this, but when we do (for the purpose of creating a weaker starting
axiom), it has confused some people.  I put a comment explaining this in
~ ax6v , which is an example of such a weakening.
</P>

<P>
<A NAME="dvnote7"></A>
<B><FONT COLOR="#006633">Note 7</FONT></B>
&nbsp;&nbsp;&nbsp;
Is it possible to do mathematics without using distinct variables (in any form,
including their implicit use in the traditional "not free in" and "free for"
concepts)?  The answer is a qualified yes, but with some complications; see the
discussion about <A HREF="mmzfcnd.html#distinctors">distinctors</A>.
</P>

<!-- 4</FONT></B>&nbsp;&nbsp;&nbsp; A distinct variable condition on
two setvar (meta)variables ` x `
and ` y ` means that the
<I>names</I> of the <A HREF="#schemes">actual variables</A> assigned to
` x ` and ` y ` must be different.  It does not mean that the
<I>values</I> or sets assigned to these actual variables must be
different.  For example, if we instantiate ` x ` with the actual variable
<I>v</I><FONT SIZE=-1><SUB>1</SUB></FONT> and ` y ` with
<I>v</I><FONT SIZE=-1><SUB>2</SUB></FONT>, that would
satisfy the distinct variable condition, because <I>v</I><FONT
SIZE=-1><SUB>1</SUB></FONT> and <I>v</I><FONT
SIZE=-1><SUB>2</SUB></FONT> are different names.  On the other hand, in
the final application, both <I>v</I><FONT SIZE=-1><SUB>1</SUB></FONT>
and <I>v</I><FONT SIZE=-1><SUB>2</SUB></FONT> could represent the same
set, such as the empty set or the number 3, and thus be equal to each
other.  See also the <A HREF="#axiomnotedv">"Distinct variables"</A>
subsection of Appendix 1 above.  -->


<P><A NAME="dvcurious"></A><B><FONT COLOR="#006633">A
curiosity</FONT></B>&nbsp;&nbsp;&nbsp; Two otherwise identical theorems
with different distinct variable conditions can express different
mathematical facts.  Compare, for example, ~ dvdemo1 and ~ dvdemo2 .
</P>

<!-- <P>It can be proved that distinct variable conditions on two setvar
variables can be replaced with logical hypotheses ($e statements) of the
form "` -. A. x x = y ` ," provided that (unlike regular $e
hypotheses) we are allowed to drop them whenever one of their variables
appears nowhere else in the theorem or its regular $e hypotheses.  This
method could replace ~ ax-c16 and ~ ax-5 to provide a logically complete system
without explicit distinct variable conditions.  We would manipulate
these "<A HREF="mmzfcnd.html#distinctors">distinctor</A>" hypotheses in
exactly the same way as regular hypotheses.  This can be done with the
existing set.mm and Metamath language if we provide a method "outside of
the system" (or by extending the language and verifier) to recognize
those $e's that have the the form of distinctors and can be dropped.
Even though this would be awkward in practice, it can provide us with a
mental picture of how distinct variable conditions are, in effect, not
very different from additional logical hypotheses.  -->

<!--
<P>Scott Fenton writes,

<BLOCKQUOTE> I'll bet what the problem is with $d is that you have a lot
of CSers looking at Metamath, and we're used to variables being scoped
[by quantifiers], so that substitution of distinct variables happens
behind the scenes.  Probably some clarification could be made by
mentioning that all variables in MM are "global" in a
sense.</BLOCKQUOTE>

Frederic Line writes,

<BLOCKQUOTE>

<P>Concerning the $d statement, here is the way I understand the whole
thing.  Perhaps it can be of some interest for you to understand the
point of view of a non-mathematician having spent some time playing with
metamath.

<P>Predicate calculus needs provisos.  These provisos have a very
strange status in logic books since they are not formalized but are
expressed informally using words.  It is as if they don't belong to the
system (I think you would say they belong to the metalogic).  Some are
not clearly expressed at all (the necessity for the variables to be
distinct).

<P>But in Metamath, provisos are expressed in a formalized way like the
rest.  Metamath knows very little about logic.  The only thing it can do
is verify substitutions.  Provisos don't belong to the metalogic world in
Metamath.  They are formalized:  necessity for a "not free" variable is
expressed by

"` ph -> A. x ph `"

and necessity for distinct variables by

"` -. A. x x = y `".

So the $d statement in fact is absolutely unnecessary in principle.
[See the discussion on the page <A HREF="mmzfcnd.html#distinctors">ZFC
Axioms With No Distinct Variable Conditions</A> - -nm.]

<P>But $d statement can help for two reasons (as I see it).  (1) Dummy
variables are unavoidable (this a consequence of the theorem
[Andr&eacute;ka's theorem] you cite in your <A
HREF="#bibmegill">article</A> in the Notre Dame journal), and it would
be strange to have an antecedent [of the form ` -. A. x x = y `]
involving a [dummy] variable that does not appear in the theorem.  (2)
It can be tedious to have to add antecedents for every variable pair
used in the theorem's proof [i.e. if there are n variables that are all
distinct, you would need n(n-1)/2 antecedents - -nm].

<P>Thus (as I see it) it's for practical reasons that the $d
statement has been added.

</BLOCKQUOTE>

-->

<!--
<P>Sometimes distinct variable conditions
can be made to disappear from the final theorem through
the clever use of dummy variables inside the proof.  An example of this
is in the proof of ~ axc14 , where the distinct
variable condition of ~ ax-5 is eliminated
via the use of ~ dvelim .
-->


<P><HR NOSHADE SIZE=1><A NAME="definitions"></A><B><FONT
COLOR="#006633">Appendix 4:  A Note on
Definitions</FONT></B>&nbsp;&nbsp;&nbsp;

<P><B><FONT COLOR="#006633">The bottom
line</FONT></B>&nbsp;&nbsp;&nbsp; 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.
<!--
Some people may view this as a
deficiency, so we will discuss its rationale and philosophy in some detail.
-->

<P>
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.
</P>

<P>
Thus, the soundness of definitions must be verified independently of the
Metamath proof verifier, either by hand or through the use of a separate
automated tool customized for the logic used by the database.
</P>

<P>
For the specific case of the set theory database set.mm, Mario Carneiro added
an enhancement to the <A HREF="../index.html#mmj2">mmj2</A> program that will
verify the soundness of all but four definitions.  There is a specification
for this definition checker in the "additional rules for definitions" section
of the ~ conventions page.  The mmj2 definition checker can be turned on
by adding
<BLOCKQUOTE>
<TT>
SetMMDefinitionsCheckWithExclusions,ax-*,df-bi,df-clab,df-cleq,df-clel
</TT>
</BLOCKQUOTE>
to the RunParms.txt file.  (The 4 excluded definitions, ~ df-bi , ~ df-clab ,
~ df-cleq , and ~ df-clel , need to be justified with metalogic outside of
mmj2's capabilities.  You can consider them additional axioms if it bothers
you.  See also the discussion "Definitions or Axioms?" in the
<A HREF="#class">Theory of Classes</A> section above.)
<!--- 4-Aug-2021 nm </P> here causes http://validator.w3.org failure -->

<!--
<P>Raph Levien has written a program to translate Metamath's set.mm database
into his <A HREF="http://ghilbert-app.appspot.com">Ghilbert</A>
[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.
</P>
-->

<P>
<B><FONT COLOR="#006633">Discussion</FONT></B>
&nbsp;&nbsp;&nbsp;
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"&mdash;to Metamath, definitions merely
extend the formal system with new patterns and are indistinguishable
from axioms by the proof verifier.
</P>

<P>
For convenience, we usually make an artificial distinction by
prefixing definition names with "df-".  But every definition is assumed
to have been metalogically justified <I>outside</I> of the Metamath
formalism as being sound.  A definition is <B>sound</B> provided (1) it
is eliminable (the wff for any theorem containing a defined symbol can
be converted to an equivalent wff without it) and (2) it is conservative
(a theorem should be provable from the original axioms after the
definition is eliminated).
</P>

<P>
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 ).
</P>

<P>
One extreme viewpoint is to consider all definitions to <I>be</I> additional
axioms, following <!-- ultraconservative --> logicians such as Le&#347;niewski
[C.  Lejewski, "On implicational definitions," <I>Studia Logica</I>
8:189-208 (1958)].

<BLOCKQUOTE>
Le&#347;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.
<I>[p. 190]</I>
</BLOCKQUOTE>

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.)
<!--- 4-Aug-2021 nm </P> here causes http://validator.w3.org failure -->

<!--
But except for four cases ( ~ df-bi , ~ df-clab , ~ df-cleq , and ~ df-clel ),
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.
-->

<P>
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.
</P>

<!--
<P>
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 <A
HREF="mmcomplex.html">complex numbers</A>:  our only goal is to
construct an object ` CC ` with
the desired properties, and we don't really care what "throwaway"
definitions (about 28 of them in the present construction) we use along
the way as long as they are sound.
</P>

<P>
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.
</P>
-->

<P>
The <A HREF="mmdefinitions.html">definition list (3MB)</A> shows all of the
definitions in the database.  The web page for each 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.
</P>

<P>
<I>
(Thanks to Raph Levien, Freek Wiedijk, Bob Solovay, and Mario Carneiro for
discussions on this topic.)
</I>
</P>

<!--
<P>
<B>Note added 8-Jun-03, updated 29-Nov-03:</B> &nbsp; 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 <A
HREF="http://www.ghilbert.org/">Ghilbert</A> [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.
</P>
-->

<P>
<HR NOSHADE SIZE=1><A NAME="assume"></A><B><FONT
COLOR="#006633">Appendix 5:  How to Find Out What Axioms a Proof Depends
On</FONT></B>&nbsp;&nbsp;&nbsp; At the end of each proof there is a list
called &quot;This theorem was proved from these axioms.&quot; These are
the axioms needed to prove the theorem from scratch, if all definitions
were eliminated.  (You can also do this from within the <A
HREF="../index.html#mmprog">Metamath program</A>:  after "read set.mm",
type "show trace_back tfr2 /essential /axioms" to get the list for
Transfinite Recursion Theorem ~ tfr2 .)
<!--- 4-Aug-2021 nm </P> here causes http://validator.w3.org failure -->

<P>
You shouldn't expect to see immediately the relationship between the
axioms and the proof you are looking at&mdash;it is typically 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 we also usually
try to do, so this list is often the minimum axiom set needed for the
proof you are seeing.
</P>

<P>
For example, we see that the Axiom of Choice ~ ax-ac was not needed to
prove ~ tfr2 , but we did need the Axiom of Replacement ~ ax-rep .
</P>

<P>
In order to find out all theorems in the path(s) from ~ tfr2 back to the
Axiom of Replacement, type "show trace_back tfr2 /to ax-rep".  The following
list results, with the theorems in the order that they occur in set.mm:

<BLOCKQUOTE>
~ ax-rep
~ axrep1
~ axrep2
~ axrep3
~ axrep4
~ funimaexg
~ resfunexg
~ fnex
~ funex
~ tfrlem14
~ tfr1
</BLOCKQUOTE>

This is particularly useful when "debugging" a proof that we think
shouldn't require a particular axiom.  It will let us identify where
exactly the undesired axiom snuck in, so that the proof can be modified
to avoid it if possible.

<P>
Sometimes a proof becomes much longer if we want to avoid a certain
axiom.  For example, Theorems ~ ondomon and ~ hartogs are the same except
for their proofs.  Compare the relatively short proof of ~ ondomon ,
which uses ~ ax-ac2 , with the much longer proof
of ~ hartogs and its lemmas needed to avoid ~ ax-ac2 .
</P>

<!--
<P>
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 setvar variables.)
But the place where Infinity is used is buried deep inside the proof
tree&mdash;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
<A HREF="#trivia">2 + 2 = 4 Trivia</A> path list above.  Then branch off from
that path and follow this one back to the Axiom of Infinity:
~ mulpipq
&lt;- ~ enqex
&lt;- ~ niex
&lt;- ~ omex
&lt;- ~ zfinf &lt;- ~ ax-inf2 .
</P>

<P>
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.
</P>
-->

<P>
<HR NOSHADE SIZE=1><A NAME="function"></A>
<B><FONT COLOR="#006633">
Appendix 6:  Notation for Function and Operation Values
</FONT></B>
&nbsp;&nbsp;&nbsp;
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.  Traditional notation includes many prefix and infix
operations; parsing this in an unambiguous way can be complicated.  Sometimes
I favored simplicity and consistency over convention.  An important example is
the notation for a <B>function value</B> ~ cfv , expressed by
&quot;` ( F `` A ) `&quot;.  Here &quot;` F `&quot; is a class that normally
is a function, the argument &quot;` A `&quot; is a class that normally belongs
to the domain of the function, and &quot;` ( F `` A ) `&quot; 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 our definition ends up evaluating to the empty set when it is not
meaningful&mdash;see for example Theorem ~ ndmfv .)
<!--- 4-Aug-2021 nm </P> here causes http://validator.w3.org failure -->

<P>
Textbooks often use the familiar notation &quot;` F ( A ) `&quot; for the value
of a function.  Outside of context, this notation is ambiguous:  it could also
mean the expression that results when ` A ` is substituted into the expression
that ` F ` 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.
</P>

<P>
For special functions such as square root, textbooks indicate function values
with an assortment of two-dimensional glyphs 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 ~ sqrtthi , the square root symbol &quot;` sqrt `&quot;
is a function i.e. a class ( ~ csqrt ), and we display the square root of 2 as
"` ( sqrt `` 2 ) `&quot;.  Two other examples are the real part of a complex
number <I><FONT COLOR="#CC33CC">A</FONT></I >, where we use &quot;` ( Re `` A )
`&quot; instead of &quot;` Re A `", and the conjugate of a complex number,
where we use &quot;` ( * `` A ) `&quot; instead of
&quot;` A `<sup>*</sup>&quot; (or sometimes with an overbar), both of which you
can see in Theorem ~ cjval .  Another example is the factorial function, which
we express as &quot;` ( ! `` A ) `&quot; instead of &quot;` A ! `&quot; 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.
</P>

<P>
There is an exception to the above convention:  the unary minus function
~ df-neg is so common that I decided to create a special syntax for it.  So,
the negative of a complex number is represented as the visually more familiar
&quot;` -u A `&quot; rather than the more tedious &quot;` ( -u `` A ) `&quot;.
One 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 . Moreover, the bare symbol &quot;` -u `&quot; has no meaning in
isolation, in contrast to say the bare symbol &quot;` sqrt `&quot;, which is
itself a set and can be manipulated as a stand-alone function for various
purposes.
</P>

<P>
Another very important exception is the notation for an <B>operation
value</B>, which is the function value of an ordered pair as defined by
~ df-ov .  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 ), "` ( A u. B ) `", 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
"` u. `" is not.  (We do not define the union of two classes as an operation
because it must work with proper classes as arguments&mdash;not to mention that
the operation value definition ultimately depends on it anyway.)
</P>

<P>
Prefix expressions (those beginning with a constant, such as the unary minus
above, logical negation, and the "for all" quantifier) have tighter binding
than infix expressions and don't require parentheses.  Also, whenever an infix
expression is a predicate&mdash;i.e. has class variable arguments but evaluates
to a wff, such as A = B&mdash;parentheses are not needed for disambiguation.
Some infix predicates that are not surrounded by parentheses are:
<PRE>
A = B
x = y
A e. B
x e. y
A =/= B
A e/ B
A C_ B
A C. B
A R B
R Po A
R Or A
R Fr A
R We A
A Fn B
R _Se A
R _FrSe A
</PRE>
(To find out where say "A Fn B" is defined, type "search * 'A Fn B'" in the
metamath program after reading in set.mm.  In this case, df-fn matches, and you
can look at the web page ~ df-fn for more information.)
<!--- 4-Aug-2021 nm </P> here causes http://validator.w3.org failure -->

<P>
There are a several other cases in the notation where infix is used without
parentheses; they include:
<PRE>
F : A --> B
F : A -1-1-> B
F : A -onto-> B
F : A -1-1-onto-> B
H Isom R , S ( A , B )
</PRE>
<!--- 4-Aug-2021 nm </P> here causes http://validator.w3.org failure -->

<P>
<HR NOSHADE SIZE=1><A NAME="subsys"></A>
<B>
<FONT COLOR="#006633">Appendix 7:  Some Predicate Calculus Subsystems</FONT>
</B>

<P>
In the set.mm database, there are 10 other axiom schemes of predicate calculus
( ~ ax-c4 , ~ ax-c5 , ~ ax-c7 , ~ ax-c9 , ~ ax-c10 , ~ ax-c11 , ~ ax-c11n ,
~ ax-c14 , ~ ax-c15 , and ~ ax-c16 ) that are not included in our "official"
list of 10 <A HREF="#pcaxioms">predicate calculus axiom schemes</A> (and one
rule) above, because they can be derived as theorems from the official ones.
These used to be part of our official list but were removed or replaced as
redundancies and simplifications were found.  We have kept them in a deprecated
section of set.mm for historical purposes, and they are not used outside of
that section.  Each of these obsolete axioms is proved as a theorem whose name
is the same with the "-" omitted.  For example, obsolete axiom ~ ax-c5 is
proved as Theorem ~ axc5 from using Axioms ~ ax-4 through ~ ax-13 .
</P>

<P>
Axioms with names starting "ax-c" are part of system S3' in Remark 9.6 of
[<A HREF="#bibmegill">Megill</A>]; for example, ~ ax-c4 is axiom C4' there.
Axiom ~ ax-c11n was a newer alternative to ~ ax-c11 , although eventually we
proved it redundant (Theorem ~ axc11n ).
</P>

<P>
From the set consisting of these 10 obsolete axiom schemes plus the 10 official
ones, several subsystems can be of interest for certain studies.  For brevity,
"axiom" always means "<A HREF="#schemes">axiom scheme</A>" in the table below.
In the table, we assume that all 20 axiom schemes and 1 rule (23 axioms and 2
rules if we include propositional calculus) are present, except for the ones
listed in the "Omit axioms" column.
</P>

<P>
<CENTER>
<TABLE BORDER CELLSPACING=0 WIDTH="100%"
SUMMARY="Variations of axiom system">

<TR>
<TH>Omit axioms</TH>
<TH>Discussion of resulting subsystem</TH>
</TR>

<TR>
<TD>
~ ax-c5 , ~ ax-c4 , ~ ax-c7 , ~ ax-c10 , ~ ax-c11 , ~ ax-c11n , ~ ax-c15 ,
~ ax-c9 , ~ ax-c14 , and ~ ax-c16
</TD>
<TD>
<P>
As mentioned above, these 10 omitted axioms can be derived from the others (see
Theorems ~ axc5 , ~ axc4 , ~ axc7 , ~ axc10 , ~ axc11 , ~ axc11n , ~ axc15 ,
~ axc9 , ~ axc14 , ~ axc16 ).  This system is
<A HREF="#axiomnote">scheme-complete</A> and is the one we ordinarily
use.  It is equivalent to system S3' in Remark 9.6 of
[<A HREF="#bibmegill">Megill</A>].
</P>

<!--
<P>
Even though we reference these 10 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.
</P>
-->
</TD>
</TR>
<TR>
<TD> ~ ax-5 </TD>
<TD>
<P>
This system is logically complete (see comments in ~ ax5ALT ), but we lose the
powerful metalogic afforded by the concept of "a variable not occurring in a
wff".  It is conjectured that ~ ax-c5 , ~ ax-c15 , and ~ ax-c14 (and possibly
other otherwise redundant ones as well) cannot be derived from the others in
this system.  Proofs in any system omitting ~ ax-5 tend to be long.
</P>
</TD>
</TR>

<TR>
<TD>
<!-- ~ ax-12 , ~ ax-c15 -->
Omit all predicate calculus axioms <I>except</I> ~ ax-4 , ~ ax-5 , ~ ax-6 ,
~ ax-7 , ~ ax-8 , ~ ax-9 , and ~ ax-gen
</TD>
<TD>
<P>
This is Tarski's system S2 and is logically (though not <I>scheme</I>)
complete.  This means that any substitution instance of the omitted axioms that
contains no wff metavariables and whose setvar variables are mutually distinct
can be derived from the axioms of this subsystem.  However, many schemes with
wff metavariables or bundled setvar variables cannot be derived.  In
particular, ~ ax-10 , ~ ax-11 , ~ ax-12 , and ~ ax-13 are conjectured not to be
derivable.
</P>
</TD>
</TR>

<TR><TD> ~ ax-c11n , ~ ax-12 ,
~ ax-c15 , ~ ax-c16 , ~ ax-5 </TD>
<TD>
<A NAME="dvfreesystem"></A>
<P>
<B>System with no distinct variable conditions.</B>
This system has no distinct variable conditions, 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 [<A HREF="#bibmegill">Megill</A>].  The primary drawback of this system is
that for it to be considered complete, we must ignore antecedents called
"<A HREF="mmzfcnd.html#distinctors">distinctors</A>" that stand in for what
would be distinct variable conditions (see the linked discussion).
</P>

<P>
We can optionally include ~ ax-c15 or ~ ax-12 for a somewhat more powerful
metalogic, since these also involve no distinct variable conditions (although
without them we can still derive any instance of them not containing wff
metavariables).
</P>

<P>Proofs in this system tend to be long.</P>
</TD>
</TR>

<TR>
<TD> ~ ax-c15 , ~ ax-c16 , ~ ax-5 </TD>
<TD>
<P>
It is conjectured that ~ ax-c15 cannot be derived from the axioms of this
subsystem.  See Item 9b on the
<A HREF="../award2003.html#9b">Workshop Miscellany</A> page.
</P>
</TD>
</TR>

<TR>
<TD> ~ ax-12 , ~ ax-c16 , ~ ax-5 </TD>
<TD>
<P>
It is known that ~ ax-12 can be derived from the axioms of this subsystem (see
Theorem ~ ax12fromc15 ).
</P>
</TD>
</TR>

<TR>
<TD> ~ ax-c11 and ~ ax-12 </TD>
<TD>
<P>
It is conjectured that ~ ax-c11 cannot be derived from the axioms of this
subsystem.
</P>
</TD>
</TR>

<TR>
<TD>
Omit all predicate calculus axioms <I>except</I> ~ ax-c5 , ~ ax-4 , ~ ax-10 ,
~ ax-11 , and ~ ax-gen
</TD>
<TD>
<A NAME="pure"></A>
<P>
The subsystem <A HREF="ax-4.html">ax-1</A> through ~ ax-11 , ~ 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
<A HREF="#traditional">traditional predicate calculus</A> 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-7 through ~ ax-5 .  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-11 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 <A HREF="../award2003.html#12">Workshop Miscellany</A> page.
</P>

<P>
Optionally, we can replace ~ ax-4 and ~ ax-10 with ~ ax-c4 and ~ ax-c7
(provided we replace them both) to obtain an equivalent subsystem.  Theorems
~ ax4fromc4 , ~ ax10fromc7 , ~ axc4 , and ~ axc7 prove the equivalence.  In
this subsystem, ~ axc5c711 can replace ~ ax-c5 , ~ ax-c7 , and ~ ax-11 .
</P>
</TD>
</TR>
</TABLE>
</CENTER>

<P>
<HR NOSHADE SIZE=1><A NAME="oldaxioms"></A>
<B>
<FONT COLOR="#006633">Appendix 8:  Axiom Numbering Before December 2018</FONT>
</B>
&nbsp;&nbsp;&nbsp;
On 20-Dec-2018, the <A HREF="#pcaxioms">predicate calculus</A> axiom schemes
were renumbered to eliminate gaps caused by obsolete or redundant axiom
schemes, as well as to order them according to their current organization.
Older papers, slide presentations, and websites may reference the old
numbering, and the table below provides a cross reference.
<!--- 4-Aug-2021 nm </P> here causes http://validator.w3.org failure -->

<P>
For further information about this renumbering, see this <A
HREF="https://groups.google.com/d/msg/metamath/OS4I_A32RTQ/6J2DmsJWCwAJ">Google
Group discussion</A> [retrieved 27-Dec-2018] and this
<A HREF="https://github.com/metamath/set.mm/issues/703">GitHub discussion</A>
[retrieved 27-Dec-2018].
</P>

<P>
Axioms with names starting "ax-c" are now obsolete, but they were part of
system S3' in Remark 9.6 of [<A HREF="#bibmegill">Megill</A>]; for example,
~ ax-c4 is axiom C4' there.  Axiom ~ ax-c11n was a newer alternative to
~ ax-c11 , although eventually we proved it redundant (Theorem ~ axc11n ).
Axiom C5 (not primed) is taken from system S3 but is included in S3' as stated
in the paper.  The obsolete axioms ~ ax-c4 through ~ ax-c16 are kept for
historical reasons in a deprecated section of set.mm and shouldn't be used
outside of that section.
</P>

<P>
In the "Proof" column, the referenced theorem has two meanings.  In the rows
for new axiom numbers ~ ax-4 through ~ ax-13 , the "Proof" column theorem shows
a proof of the axiom from the obsolete ones ~ ax-c4 through ~ ax-c16 .  This is
useful to see how our current axioms can be derived from the original ones in
[<A HREF="#bibmegill">Megill</A>].  In the rows for ~ ax-c4 through ~ ax-c16 ,
the "Proof" column theorem shows a derivation of the obsolete axiom from our
current system ~ ax-4 through ~ ax-13 .  Together, these proofs show that our
current system is equivalent to the one in [<A HREF="#bibmegill">Megill</A>].
</P>

<!-- Note that &#8203; is a zero-width space that prevents the label from being
changed if a global substitution is done. -->

<CENTER>
<TABLE BORDER CELLSPACING=0 BGCOLOR="#EEFFFA"
SUMMARY="Cross reference between orginal and new predicate calculus axioms">

<TR ALIGN=LEFT>
<TD><FONT COLOR="#006633"><B>New number</B></FONT></TD>
<TD><FONT COLOR="#006633"><B>Old number</B></FONT></TD>
<TD><FONT COLOR="#006633"><B>Proof</B></FONT></TD>
<TD><FONT COLOR="#006633"><B>[<A HREF="#bibmegill">Megill</A>]</B></FONT></TD>
<TD><FONT COLOR="#006633"><B>Content</B></FONT></TD>
<TD><FONT COLOR="#006633"><B>Description</B></FONT></TD>
</TR>

<TR ALIGN=LEFT>
<TD> ~ ax-4 </TD><TD> ax-5&#8203; </TD><TD> ~ ax4fromc4 </TD><TD> - </TD>
<TD> ` |- ( A. x ( ph -> ps ) -> ( A. x ph -> A. x ps ) ) ` </TD>
<TD> Quantified Implication </TD></TR>

<TR ALIGN=LEFT>
<TD> ~ ax-5 </TD><TD> ax-17&#8203; </TD><TD> - </TD><TD> C5 </TD>
<TD> ` |- ( ph -> A. x ph ) ` , where ` x ` does not occur in ` ph ` </TD>
<TD> Distinctness </TD></TR>

<TR ALIGN=LEFT>
<TD> ~ ax-6 </TD><TD> ax-9&#8203; </TD><TD> ~ ax6fromc10 </TD><TD> - </TD>
<TD> ` |- -. A. x ` ` -. x = y ` </TD>
<TD> Existence </TD></TR>

<TR ALIGN=LEFT>
<TD> ~ ax-7 </TD><TD> ax-8&#8203; </TD><TD> - </TD><TD> C8' </TD>
<TD> ` |- ( x = y -> ( x = z -> y = z ) ) ` </TD>
<TD> Equality </TD></TR>

<TR ALIGN=LEFT>
<TD> ~ ax-8 </TD><TD> ax-13&#8203; </TD><TD> - </TD><TD> C12' </TD>
<TD> ` |- ( x = y -> ( x e. z -> y e. z ) ) ` </TD>
<TD> Left Equality for Binary Predicate </TD></TR>

<TR ALIGN=LEFT>
<TD> ~ ax-9 </TD><TD> ax-14&#8203; </TD><TD> - </TD><TD> C13' </TD>
<TD> ` |- ( x = y -> ( z e. x -> z e. y ) ) ` </TD>
<TD> Right Equality for Binary Predicate </TD></TR>

<TR ALIGN=LEFT>
<TD> ~ ax-10 </TD><TD> ax-6&#8203; </TD><TD> ~ ax10fromc7 </TD><TD> - </TD>
<TD> ` |- ( -. A. x ph -> A. x -. A. x ph ) ` </TD>
<TD> Quantified Negation </TD></TR>

<TR ALIGN=LEFT>
<TD> ~ ax-11 </TD><TD> ax-7&#8203; </TD><TD> - </TD><TD> C6' </TD>
<TD> ` |- ( A. x A. y ph -> A. y A. x ph ) ` </TD>
<TD> Quantifier Commutation </TD></TR>

<TR ALIGN=LEFT>
<TD> ~ ax-12 </TD><TD> ax-11&#8203; </TD><TD> ~ ax12fromc15 </TD><TD> - </TD>
<TD> ` |- ( x = y -> ( A. y ph -> A. x ( x = y -> ph ) ) ) ` </TD>
<TD> Substitution </TD></TR>

<TR ALIGN=LEFT>
<TD> ~ ax-13 </TD><TD> ax-12&#8203; </TD><TD> ~ ax13fromc9 </TD><TD> - </TD>
<TD> ` |- ( -. x = y -> ( y = z -> A. x ` ` y = z ) ) ` </TD>
<TD> Quantified Equality </TD></TR>

<TR ALIGN=LEFT>
<TD COLSPAN=6> </TD></TR>

<TR ALIGN=CENTER><TD COLSPAN=6><B>Obsolete axioms</B></TD></TR>

<TR ALIGN=LEFT>
<TD> ~ ax-c4 </TD><TD> ax-5o&#8203; </TD><TD> ~ axc4 </TD><TD> C4' </TD>
<TD> ` |- ( A. x ( A. x ph -> ps ) -> ( A. x ph -> A. x ps ) ) ` </TD>
<TD> Quantified Implication </TD></TR>

<TR ALIGN=LEFT>
<TD> ~ ax-c5 </TD><TD> ax-4&#8203; </TD><TD> ~ axc5 </TD><TD> C5' </TD>
<TD> ` |- ( A. x ph -> ph ) ` </TD>
<TD> Specialization </TD></TR>

<TR ALIGN=LEFT>
<TD> ~ ax-c7 </TD><TD> ax-6o&#8203; </TD><TD> ~ axc7 </TD><TD> C7' </TD>
<TD> ` |- ( -. A. x -. A. x ph -> ph ) ` </TD>
<TD> Quantified Negation </TD></TR>

<TR ALIGN=LEFT>
<TD> ~ ax-c9 </TD><TD> ax-12o&#8203; </TD><TD> ~ axc9 </TD><TD> C9' </TD>
<TD> ` |- ( -. A. z ` ` z = x -> ( -. A. z `
` z = y -> ( x = y -> A. z ` ` x = y ) ) ) ` </TD>
<TD> Quantified Equality </TD></TR>

<TR ALIGN=LEFT>
<TD> ~ ax-c10 </TD><TD> ax-9o&#8203; </TD><TD> ~ axc10 </TD><TD> C10' </TD>
<TD> ` |- ( A. x ( x = y -> A. x ph ) -> ph ) ` </TD>
<TD> Existence </TD></TR>

<TR ALIGN=LEFT>
<TD> ~ ax-c11 </TD><TD> ax-10o&#8203; </TD><TD> ~ axc11 </TD><TD> C11' </TD>
<TD> ` |- ( A. x ` ` x = y -> ( A. x ph -> A. y ph ) ) ` </TD>
<TD> Quantifier Substitution </TD></TR>

<TR ALIGN=LEFT>
<TD> ~ ax-c11n </TD><TD> ax-10&#8203; </TD><TD> ~ axc11n </TD><TD> - </TD>
<TD> ` |- ( A. x ` ` x = y -> A. y ` ` y = x ) ` </TD>
<TD> Quantifier Substitution </TD></TR>

<TR ALIGN=LEFT>
<TD> ~ ax-c14 </TD><TD> ax-15&#8203; </TD><TD> ~ axc14 </TD><TD> C14' </TD>
<TD> ` |- ( -. A. z ` ` z = x -> ( -. A. z `
` z = y -> ( x e. y -> A. z ` ` x e. y ) ) ) ` </TD>
<TD> Quantified Binary Predicate </TD></TR>

<TR ALIGN=LEFT>
<TD> ~ ax-c15 </TD><TD> ax-11o&#8203; </TD><TD> ~ axc15 </TD><TD> C15' </TD>
<TD>
` |- ( -. A. x ` ` x = y -> ( x = y -> ( ph -> A. x ( x = y -> ph ) ) ) ) `
</TD>
<TD> Variable Substitution </TD></TR>

<TR ALIGN=LEFT>
<TD> ~ ax-c16 </TD><TD> ax-16&#8203; </TD><TD> ~ axc16 </TD><TD> C16' </TD>
<TD> ` |- ( A. x ` ` x = y -> ( ph -> A. x ph ) ) ` , where ` x ` and ` y ` are
distinct </TD>
<TD> Distinct Variables </TD></TR>
</TABLE>
</CENTER>

<P>
<HR NOSHADE SIZE=1><A NAME="read"></A>
<B><FONT COLOR="#006633">Reading Suggestions</FONT></B>
&nbsp;&nbsp;&nbsp;
Logic and set theory provide a foundation for all of mathematics.  One possible
way to start to learn about them is to use the Metamath Proof Explorer in
conjunction with one or more textbooks listed in the Bibliography of the next
section.  The textbooks provide a motivation for what we are doing, whereas the
Metamath Proof Explorer lets you see in detail all hidden and implicit steps.
Most standard theorems are accompanied by <A HREF="mmbiblio.html">literature
cross references</A>, and it will probably be easier to acquire a higher-level
understanding of them if you consult these.
<!--- 4-Aug-2021 nm </P> here causes http://validator.w3.org failure -->

<P>
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 <I>A Primer for Logic
and Proof</I>, mentioned <A HREF="#traditional">above</A>, uses modern notation
and is also highly recommended.
</P>

<P>
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 <FONT COLOR="#CC33CC">purple</FONT> class variables (which in Quine are
Greek letters).  (See also the <A HREF="#class">Theory of Classes</A> above.)
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 <I>avoid</I> 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.
</P>

<P>
Margaris and Quine give only an informal explanation of their dot notation that
may not satisfy everyone.  A good explanation can be found in Copi's
<I>Symbolic Logic</I> (5th edition), Section 9.3, with multiple examples.
(Thanks to Patrick Clot for this suggestion.)
</P>

<P>
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.
</P>

<UL>
<LI> Axioms of propositional calculus&mdash;Margaris.
</LI>
<LI>
Theorems of propositional calculus&mdash;Whitehead and Russell.
</LI>
<LI>
Axioms of predicate calculus&mdash;Megill (System S3' in the article
referenced).
</LI>
<LI>
Theorems of pure predicate calculus&mdash;Margaris.
</LI>
<LI>
Theorems of equality and substitution&mdash;Monk2, Tarski, Megill.
</LI>
<LI>
Axioms of set theory&mdash;Bell and Machover.
</LI>
<LI>
Virtual classes in set theory (our class builder notation and
our purple class variables)&mdash;Quine.
</LI>
<LI> Development of set theory (including most of the notation we
use)&mdash;Takeuti and Zaring.
</LI>
<LI>
Construction of real and complex numbers&mdash;Gleason.
</LI>
<LI>
Elementary theorems about real numbers&mdash;Apostol.
</LI>
</UL>

<HR NOSHADE SIZE=1><A NAME="bib"></A>
<B><FONT COLOR="#006633">Bibliography</FONT></B>
&nbsp;&nbsp;&nbsp;

This is the complete list of books and articles that are
<A HREF="mmbiblio.html">cross referenced</A> in the Metamath Proof Explorer
database.  The numbers in brackets are the Library of Congress classifications
to make them easier to find on your university library shelves.  These may
differ slightly for resources assigned by the libary itself, and the ones we
show are used by the MIT libraries.

<OL>
<LI>
<A NAME="Adamek"></A> [Adamek] Ji&#345;&iacute; Ad&aacute;mek, Horst
Herrlich, George E. Strecker, <I>Abstract and Concrete Categories:  The Joy of
Cats</I>, Dover Publications, Mineola, New York (2004); available at <A
HREF="http://katmat.math.uni-bremen.de/acc">
http://katmat.math.uni-bremen.de/acc</A> (retrieved 2-Jan-2017).
</LI>
<LI>
<A NAME="AhoHopUll"></A> [AhoHopUll] Alfred V. Aho, John E. Hopcroft and
Jeffrey D. Ullman, <I>The Design and Analysis of Computer Algorithms</I>,
Addison-Wesley, Reading, Massachusetts (1974) [QA76.6 .A36].
</LI>
<LI>
<A NAME="AitkenIBG"></A> [AitkenIBG] Aitken, Wayne, "Incidence Betweenness
Geometry," Handout (2008); available at
<A HREF="http://public.csusm.edu/aitken_html/m410/betweenness.08.pdf"
>http://public.csusm.edu/aitken_html/m410/betweenness.08.pdf</A>
(retrieved 6 Apr 2016). [The series of handouts is available at
<A HREF="http://public.csusm.edu/aitken_html/m410/"
>http://public.csusm.edu/aitken_html/m410/</A> (retrieved 6 Apr 2016).]
</LI>
<LI>
<A NAME="AitkenIBCG"></A> [AitkenIBCG] Aitken, Wayne, "IBC
Geometry," Handout (2008); available at <A
HREF="http://public.csusm.edu/aitken_html/m410/congruence.08.pdf"
>http://public.csusm.edu/aitken_html/m410/congruence.08.pdf</A>
(retrieved 6 Apr 2016).
</LI>
<LI>
<A NAME="AitkenNG"></A> [AitkenNG] Aitken, Wayne, "Neutral
Geometry," Handout (2010); available at <A
HREF="http://public.csusm.edu/aitken_html/m410/neutral.10.pdf"
>http://public.csusm.edu/aitken_html/m410/neutral.10.pdf</A>
(retrieved 6 Apr 2016).
</LI>
<LI>
<A NAME="AitkenEG"></A> [AitkenEG] Aitken, Wayne, "Euclidean
Geometry," Handout (2010); available at <A
HREF="http://public.csusm.edu/aitken_html/m410/euclidean.10.pdf"
>http://public.csusm.edu/aitken_html/m410/euclidean.10.pdf</A>
(retrieved 6 Apr 2016).
</LI>
<LI>
<A NAME="AitkenQ"></A> [AitkenQ] Aitken, Wayne, "Quadrilaterals,"
Handout (2008); available at <A
HREF="http://public.csusm.edu/aitken_html/m410/quad.08.pdf"
>http://public.csusm.edu/aitken_html/m410/quad.08.pdf</A>
(retrieved 6 Apr 2016).
</LI>
<LI>
<A NAME="AitkenLDZT"></A> [AitkenLDZT] Aitken, Wayne, "Legendre's Defect
Zero Theorem,"  Handout (2008); available at <A
HREF="http://public.csusm.edu/aitken_html/m410/defectzero.08.pdf"
>http://public.csusm.edu/aitken_html/m410/defectzero.08.pdf</A>
(retrieved 6 Apr 2016).
</LI>
<LI>
<A NAME="AitkenEHC"></A> [AitkenEHC] Aitken, Wayne, "Euclidean
and Hyperbolic Conditions," Handout (2008); available at <A
HREF="http://public.csusm.edu/aitken_html/m410/conditions.08.pdf"
>http://public.csusm.edu/aitken_html/m410/conditions.08.pdf</A>
(retrieved 6 Apr 2016).
</LI>
<LI>
<A NAME="AitkenTHG"></A> [AitkenTHG] Aitken, Wayne, "Topics
in Hyperbolic Geometry," Handout (2008); available at <A
HREF="http://public.csusm.edu/aitken_html/m410/hyperbolic.08.pdf"
>http://public.csusm.edu/aitken_html/m410/hyperbolic.08.pdf</A>
(retrieved 6 Apr 2016).
</LI>
<LI>
<A NAME="AkhiezerGlazman"></A> [AkhiezerGlazman] Akhiezer, N. I.,
and I. M. Glazman, <I>Theory of Linear Operators in Hilbert Space</I>,
Vol.  I, Dover Publications, Mineola, New York (1993) [QA322.4.A3813
1993].
</LI>
<LI>
<A NAME="Alling"></A> [Alling] Alling, Norman L., <I>Foundations of
Analysis Over Surreal Number Fields,</I> Elsevier Science Publishing
Company, Inc. (1987) [QA1.N79].
</LI>
<LI>
<A NAME="Apostol"></A> [Apostol] Apostol, Tom M.,
<I>Calculus,</I> vol. 1, 2nd ed.,
John Wiley &amp; Sons Inc. (1967) [QA300.A645 1967].</LI>

<LI><A NAME="ApostolNT"></A> [ApostolNT] Apostol, Tom M.,
<I>Introduction to analytic number theory,</I> Springer-Verlag, New York,
Heidelberg, Berlin (1976) [QA241.A6].</LI>

<LI><A NAME="Baer"></A> [Baer] Baer, Reinhold, <I>Linear Algebra and
Projective Geometry,</I> Academic Press, New York (1952)
[QA471.B34].
</LI>

<LI><A NAME="Bauer"></A> [Bauer] Bauer, Andrej, &quot;Five stages of
accepting constructive mathematics,&quot; <I>Bulletin (New Series) of
the American Mathematical Society</I>, 54:481-498 (2017),
DOI: <A HREF="http://dx.doi.org/10.1090/bull/1556">10.1090/bull/1556</A> .</LI>

<LI>
<A NAME="BeauregardFraleigh"></A> [BeauregardFraleigh] Beauregard, Raymond A.,
and Fraleigh, John B., <I>A First Course In Linear Algebra: with Optional
Introduction to Groups, Rings, and Fields,</I> Houghton Mifflin Company,
Boston (1973).
</LI>

<LI>
<A NAME="BellMachover"></A> [BellMachover] Bell, J. L., and M.
Machover, <I>A Course in Mathematical Logic,</I> North-Holland,
Amsterdam (1977) [QA9.B3953].
</LI>
<LI>
<A NAME="Beeson2016"></A> [Beeson2016] Beeson, Michael, and
Larry Wos, "Finding Proofs in Tarskian Geometry",
2016-06-22, <I>Journal of Automated Reasoning</I>,
Volume 58, DOI 10.1007/s10817-016-9392-2,
<A HREF="https://www.researchgate.net/publication/304350412_Finding_Proofs_in_Tarskian_Geometry">
ResearchGate</A> or
<A HREF="http://www.michaelbeeson.com/research/papers/Tarski-JAR.pdf">
Prepublication</A>.
</LI>
<LI>
<A NAME="BeltramettiCassinelli1"></A> [BeltramettiCassinelli1] Enrico
G. Beltrametti and Gianni Cassinelli, "Logical and Mathematical Structures
of Quantum Mechanics," <I>La Rivista del Nuovo cimento</I> 6:321-404 (1976)
[QC.R625].
</LI>
<LI>
<A NAME="BeltramettiCassinelli"></A> [BeltramettiCassinelli] Enrico
G. Beltrametti and Gianni Cassinelli, <I>The Logic of Quantum
Mechanics</I> (Encyclopedia of Mathematics and Its Applications; v. 15,
Mathematics of Physics), Addison-Wesley, Reading, Massachusetts (1981)
[QC174.12.B45].
</LI>
<LI>
<A NAME="Beran"></A> [Beran] Ladislav Beran, <I>Orthomodular
Lattices; Algebraic Approach</I>, D. Reidel, Dordrecht (1985)
[QA171.5.B4].
</LI>
<LI>
<A NAME="Berge"></A> [Berge] Berge, Claude <I>Hypergraphs</I>,
Elsevier Science B.V., Amsterdam (1989) [QA166.23.B4813 1989]
</LI>
<LI>
<A NAME="Bobzien"></A> [Bobzien] Bobzien, Susanne, "Stoic Logic",
<I>The Cambridge Companion to Stoic Philosophy</I>,
Brad Inwood (ed.), Cambridge University Press (2003-2006),
<A HREF="https://philpapers.org/rec/BOBSL">
https://philpapers.org/rec/BOBSL</A>.
</LI>
<LI>
<A NAME="Bogachev"></A> [Bogachev] Bogachev, V.I., <I>Measure Theory,
Volume I</I> Springer-Verlag, Berlin, New York, (2007)
[QC20.7.M34.B64 2007].
</LI>
<LI>
<A NAME="Bollobas"></A> [Bollobas] B&eacute;la Bollob&aacute;s, <I>Modern
Graph Theory</I>, Graduate Texts in Mathematics, Springer Science+Media New
York (1998)
[QA166.B663].
</LI>
<LI>
<A NAME="BourbakiEns"></A> [BourbakiEns] Bourbaki, Nicolas,
<I>Th&eacute;orie des ensembles,</I> Springer-Verlag,
Berlin Heidelberg (2007); available in English (for purchase) at
<A HREF="http://www.springer.com/us/book/9783540225256">
http://www.springer.com/us/book/9783540225256</A> (retrieved
15-Aug-2016). Page references in set.mm are for the French edition.
</LI>
<LI>
<A NAME="BourbakiAlg1"></A> [BourbakiAlg1] Bourbaki, Nicolas,
<I>Alg&egrave;bre, Chapitres 1 &agrave; 3,</I> Springer-Verlag,
Berlin Heidelberg (2007); available in English (for purchase) at
<A HREF="http://www.springer.com/us/book/9783540642435">
http://www.springer.com/us/book/9783540642435</A> (retrieved
15-Aug-2016). Page references in set.mm are for the French edition.
</LI>
<LI>
<A NAME="BourbakiTop1"></A> [BourbakiTop1] Bourbaki, Nicolas, <I>Topologie
g&eacute;n&eacute;rale, Chapitres 1 &agrave; 4,</I> Springer-Verlag,
Berlin Heidelberg (2007); available in English (for purchase) at
<A HREF="http://www.springer.com/us/book/9783540642411">
http://www.springer.com/us/book/9783540642411</A> (retrieved
15-Aug-2016). Page references in set.mm are for the French edition.
</LI>
<LI>
<A NAME="BourbakiTop2"></A> [BourbakiTop2] Bourbaki, Nicolas, <I>Topologie
g&eacute;n&eacute;rale, Chapitres 5 &agrave; 10,</I> Springer-Verlag,
Berlin Heidelberg (2007); available in English (for purchase) at
<A HREF="http://www.springer.com/us/book/9783540645634">
http://www.springer.com/us/book/9783540645634</A> (retrieved
15-Aug-2016). Page references in set.mm are for the French edition.
</LI>
<LI>
<A NAME="BourbakiFVR"></A> [BourbakiFVR] Bourbaki, Nicolas, <I>Fonctions
d'une variable r&eacute;elle,</I> Springer-Verlag,
Berlin Heidelberg (2007); available in English (for purchase) at
<A HREF="http://www.springer.com/us/book/9783540653400">
http://www.springer.com/us/book/9783540653400</A> (retrieved
15-Aug-2016). Page references in set.mm are for the French edition.
</LI>
<LI>
<A NAME="BrosowskiDeutsh"></A> [BrosowskiDeutsh] Bruno Brosowsky and
Frank Deutsh, "An elementary proof of the Stone-Weierstrass theorem",
Proc.  Amer.  Math.  Soc. 81 (1981), 89-92; available at <A
HREF="http://www.ams.org/journals/proc/1981-081-01/S0002-9939-1981-0589143-8/">
http://www.ams.org/journals/proc/1981-081-01/S0002-9939-1981-0589143-8/</A>
(retrieved 24-Apr-2017).
</LI>
<LI>
<A NAME="Bruck"></A> [Bruck] Bruck, Richard Hubert <I>A survey of binary
systems</I>, 3rd ed., Springer-Verlag Berlin Heidelberg New York (1971)
</LI>
<LI>
<A NAME="ChoquetDD"></A> [ChoquetDD] Choquet-Bruhat, Yvonne and Cecile
DeWitt-Morette, with Margaret Dillard-Bleick, <I>Analysis, Manifolds and
Physics,</I> Elsevier Science B.V., Amsterdam (1982) [QC20.7.A5C48
1981].
</LI>
<LI>
<A NAME="Church"></A> [Church] Church, Alonzo, <I>Introduction to
Mathematical Logic,</I> Princeton University Press, 1956.
</LI>
<LI>
<A NAME="Clemente"></A> [Clemente] Clemente Laboreo, Daniel
<I>Introduction to natural deduction</I> (2014); available
at <A HREF="http://www.danielclemente.com/logica/dn.en.pdf">
http://www.danielclemente.com/logica/dn.en.pdf</A> (PDF) and
<A HREF="http://www.danielclemente.com/logica/dn.en.html">
http://www.danielclemente.com/logica/dn.en.html</A> (HTML)
(retrieved 10 Feb 2017).
</LI>
<LI>
<A NAME="Cohen"></A> [Cohen] Cohen, David, <I>Precalculus With Unit-Circle
Trigonometry,</I> Brooks-Cole, Pacific Grove, CA (1988)
[QA331.3.C64].
</LI>
<LI>
<A NAME="Cohen4"></A> [Cohen4] Cohen, David, <I>Precalculus With Unit-Circle
Trigonometry</I>, 4th ed., Brooks-Cole, Pacific Grove, CA (2006)
[QA331.3.C64].
</LI>
<LI>
<A NAME="Cohn"></A> [Cohn] Cohn, Paul Moritz, <I>Universal Algebra,</I>
D. Reidel, Dordrecht (1981) [QA251.C55].
</LI>
<LI>
<A NAME="CohnMT"></A> [CohnMT] Cohn, Donald L., <I>Measure Theory,</I>
 Birkh&auml;user, New York (2013).
</LI>
<LI>
<A NAME="Connell"></A> [Connell] Edwin H. Connell, <I>Elements of Abstract
and Linear Algebra,</I> Orange Grove Texts Plus (October 21, 2009); ISBN
978-1616100032; available at <A HREF="http://www.math.miami.edu/~~ec/book">
http://www.math.miami.edu/~~ec/book</A> (retrieved 10 Dec 2019).
</LI>
<LI>
<A NAME="Conway"></A> [Conway] John H. Conway, <I>On Numbers and Games,</I>
2nd ed., A K Peters Ltd (2001) [QA241.C69].
</LI>
<LI>
<A NAME="CormenLeisersonRivest"></A> [CormenLeisersonRivest] Cormen,
Thomas, Charles E. Leiserson, and Ronald L. Rivest, <I>Introduction to
Algorithms,</I> The MIT Press, Cambridge, Massachusetts (1989)
[QA76.6.C662].
</LI>
<LI>
<A NAME="Crawley"></A> [Crawley] Crawley, Peter and Robert P.
Dilworth, <I>Algebraic Theory of Lattices,</I> Prentice-Hall, Englewood
Cliffs, New Jersey (1973) [QA171.5.C7].
</LI>
<LI>
<A NAME="Diestel"></A> [Diestel] Diestel, Reinhard, <I>Graph Theory,
5th Electronic Edition,</I> Springer-Verlag, Heidelberg (2016)
[QA166.D51413].
<!-- old url
URL: <A HREF="http://www.math.uni-hamburg.de/home/diestel/books/graph.theory/">
http://www.math.uni-hamburg.de/home/diestel/books/graph.theory/</A>
-->
URL: <A HREF="http://diestel-graph-theory.com/index.html">
http://diestel-graph-theory.com/index.html</A>
</LI>
<LI>
<A NAME="Eisenberg"></A> [Eisenberg] Eisenberg, Murray,
<I>Axiomatic Theory of Sets and Classes,</I>
Holt, Rinehart and Winston, Inc., New York (1971)
[QA248.E36].
</LI>
<LI>
<A NAME="Enderton"></A> [Enderton] Enderton, Herbert B., <I>Elements of Set
Theory,</I> Academic Press, Inc., San Diego, California (1977)
[QA248.E5].
</LI>
<LI>
<A NAME="Euclid1"></A> [Euclid1] Euclid, <I>The Thirteen Books of
Euclid's Elements,</I> Vol. I:  Introduction and books I&mdash;II,
translated by Thomas L. Heath, Cambridge University Press, Cambridge
(1908); available at
<A HREF="https://archive.org/details/thirteenbookseu02heibgoog">
https://archive.org/details/thirteenbookseu03heibgoog</A> (retrieved 9
Apr 2016).  See also David Joyce's web pages at
<A HREF="http://aleph0.clarku.edu/~~djoyce/java/elements/">
http://aleph0.clarku.edu/~~djoyce/java/elements/</A> for interactive Java
applets and detailed expositions.
</LI>
<LI>
<A NAME="Euclid2"></A> [Euclid2] Euclid, <I>The Thirteen Books of
Euclid's Elements,</I> Vol. II:  Books III&mdash;IX, translated by
Thomas L. Heath, Cambridge University Press, Cambridge (1908); available
at <A HREF="https://archive.org/details/thirteenbookseu00heibgoog">
https://archive.org/details/thirteenbookseu03heibgoog</A> (retrieved 9
Apr 2016).
</LI>
<LI>
<A NAME="Euclid3"></A> [Euclid3] Euclid, <I>The Thirteen Books of
Euclid's Elements,</I> Vol. III:  Books X&mdash;XIII and appendix,
translated by Thomas L. Heath, Cambridge University Press, Cambridge
(1908); available at
<A HREF="https://archive.org/details/thirteenbookseu03heibgoog">
https://archive.org/details/thirteenbookseu03heibgoog</A> (retrieved 9
Apr 2016).
</LI>
<LI>
<A NAME="FaureFrolicher"></A> [FaureFrolicher] Faure, Claude-Alain
and Fr&ouml;licher, Alfred, <I>Modern Projective Geometry,</I>
Springer, Dordrecht (2000) [QA471.F33 2000].
</LI>
<LI>
<A NAME="Frege1879"></A> [Frege1879] Frege, Gottlob, <I>Begriffsschrift</I>
(German for "concept-script"),
<A HREF="https://gallica.bnf.fr/ark:/12148/bpt6k65658c">
https://gallica.bnf.fr/ark:/12148/bpt6k65658c</A>.
</LI>
<LI>
<A NAME="Fremlin1"></A> [Fremlin1] Fremlin, D. H., <I>Measure
Theory, Vol. 1:  The Irreducible Minimum</I>, 2nd ed., Lulu Press,
Morrisville, North Carolina (2011) [QA312.F72]; available at
<A HREF="https://wiki.math.ntnu.no/_media/tma4225/2011/fremlin-mt1.pdf"
>https://wiki.math.ntnu.no/_media/tma4225/2011/fremlin-mt1.pdf</A>
(retrieved 14 Apr 2015).
</LI>
<LI>
<A NAME="Fremlin5"></A> [Fremlin5] Fremlin, D. H., <I>Measure
Theory, Vol. 5:  Set-theoretic Measure Theory</I>  Lulu Press,
Morrisville, North Carolina (2008)  [QA312.F72]; available
at <A HREF="https://www.essex.ac.uk/maths/people/fremlin/mt.htm"
>https://www.essex.ac.uk/maths/people/fremlin/mt.htm</A> (retrieved 14
Apr 2015).
</LI>
<LI>
<A NAME="FreydScedrov"></A> [FreydScedrov] Freyd, Peter J. and Andre
Scedrov, <I>Categories, Allegories,</I> Elsevier Science Publishers
B.V., Amsterdam (1990) [QA169.F73 1990].
</LI>
<LI>
<A NAME="Gleason"></A> [Gleason] Gleason, Andrew M., <I>Fundamentals of
Abstract Analysis,</I> Jones and Bartlett Publishers, Boston (1991)
[QA300.G554].
</LI>
<LI>
<A NAME="Golan"></A> [Golan] Golan, Jonathan S., <I>Semirings and their
Applications,</I> Kluwer Academic Publishers, Dordrecht (1999)
[QA251.5 .G642 1999].
</LI>
<LI>
<A NAME="Gonshor"></A> [Gonshor] Gonshor, Harry, <I>An Introduction to
the Theory of Surreal Numbers,</I> London Mathematical Society (1986)
[QA241.G63 1986].
</LI>
<LI>
<A NAME="Gratzer"></A> [Gratzer] Gr&auml;tzer, George, <I>Universal
Algebra,</I> 2nd ed. with updates, Springer, New York (2008)
[QA251.G68 2008].
</LI>
<LI>
<A NAME="GramKnuthPat"></A> [GramKnuthPat] Gram, Ronald L., Knuth, Donald
E., and Patashnik, Oren, <I>Concrete Mathematics,</I> 2nd Ed., Addison-Wesley
Publishing Company, Reading, MA (1994) [QA39.2.G733].
</LI>
<LI>
<A NAME="EGA"></A> [EGA] Grothendieck, Alexandre and Dieudonn&eacute;,
Jean <I>&Eacute;l&eacute;ments de g&eacute;om&eacute;trie alg&eacute;brique</I>
Institut des hautes &eacute;tudes scientifiques, Publ. Math. No. 4 (1960),
available at <A HREF="http://www.numdam.org/item/PMIHES_1960__4__5_0.pdf">
NumDam</A>.
</LI>
<LI>
<A NAME="Hall"></A> [Hall] Hall, Marshall Jr., <I>The Theory of Groups,</I>
The Macmillan Company, New York (1959) [QA171.H27 2018].
</LI>

<LI><A NAME="Halmos"></A> [Halmos] Paul R. Halmos, <I>Introduction to
Hilbert Space and the Theory of Spectral Multiplicity</I>, AMS Chelsea
Publishing, Providence, Rhode Island (1957) [QA691.H194 1957].  </LI>

<LI>
<A NAME="Hamilton"></A> [Hamilton] Hamilton, A. G., <I>Logic for
Mathematicians,</I> Cambridge University Press, Cambridge, revised
edition (1988) [QA9.H298 1988].
</LI>
<LI>
<A NAME="Hatcher"></A> [Hatcher] Hatcher, Allen, <I>Algebraic
Topology,</I> Cambridge University Press, Cambridge (2002)
[QA612.H42 2002];
available at
<A HREF="http://www.math.cornell.edu/~~hatcher/AT/ATpage.html">
http://www.math.cornell.edu/~~hatcher/AT/ATpage.html</A>
(retrieved 11 Nov 2014).
</LI>
<LI>
<A NAME="Hefferon"></A> [Hefferon] Hefferon, Jim, <I>Linear Algebra</I>,
3rd edition, Lightning Source Inc. (2017), ISBN-13: 978-1944325039,
available at <A HREF="http://joshua.smcvt.edu/linearalgebra">
http://joshua.smcvt.edu/linearalgebra</A> (retrieved 26 Nov 2019).
</LI>
<LI>
<A NAME="Helfgott"></A> [Helfgott] Helfgott, Harald A.,
<I>The ternary Goldbach conjecture is true</I> arXiv:1312.7748v2 (17-Jan-2014);
available at <A HREF="https://arxiv.org/abs/1312.7748">
https://arxiv.org/abs/1312.7748</A> (retrieved 2 Aug 2020). See also
<A HREF="https://webusers.imj-prg.fr/~~harald.helfgott/anglais/book.html">
https://webusers.imj-prg.fr/~~harald.helfgott/anglais/book.html</A>
</LI>
<LI>
<A NAME="Herstein"></A> [Herstein] Herstein, I. N., <I>Abstract
Algebra,</I> Macmillan Publishing Company, New York (1986) [QA162.H47
1986].
</LI>
<LI>
<A NAME="Hitchcock"></A> [Hitchcock] Hitchcock, David, <I>The
peculiarities of Stoic propositional logic</I>, McMaster University;
available at
<A HREF="http://www.humanities.mcmaster.ca/~~hitchckd/peculiarities.pdf">
http://www.humanities.mcmaster.ca/~~hitchckd/peculiarities.pdf</A>
(retrieved 3 Jul 2016).
</LI>
<LI>
<A NAME="Holland95"></A> [Holland95] Holland, Samuel S.,
&quot;Orthomodularity in infinite dimensions; a theorem of M.
Sol&egrave;r,&quot; <I>Bull.  Am.  Math.  Soc.</I> 32:205-234 (1995)
[QA.A513]; available at <A HREF="http://arxiv.org/abs/math/9504224v1">
http://arxiv.org/abs/math/9504224v1</A> (retrieved 11 Nov 2014).
</LI>
<LI>
<A NAME="Holmes"></A> [Holmes] Holmes, Robert, <I>Elementary Set Theory With a
Universal Set</I>; available at
<A HREF="https://randall-holmes.github.io/head.pdf">
https://randall-holmes.github.io/head.pdf</A> (retrieved 7 Feb 2022).
</LI>
<LI>
<A NAME="Huneke"></A> [Huneke] Huneke, Craig L.,
&quot;The Friendship Theorem&quot; <I>American Mathematical Monthly</I>
109:192-194 (2002); available at <A
HREF="https://www.researchgate.net/publication/268313555_The_Friendship_Theorem">
https://www.researchgate.net/publication/268313555_The_Friendship_Theorem</A>
(retrieved 30 Dec 2017).
</LI>
<LI>
<A NAME="Indrzejczak"></A> [Indrzejczak] Indrzejczak, Andrzej,
<I>Natural Deduction, Hybrid Systems and Modal Logic</I>,
Trends in Logic Vol. 30, Springer (2010).
</LI>
<LI>
<A NAME="Jech"></A> [Jech] Jech, Thomas, <I>Set Theory,</I>
Academic Press, San Diego (1978) [QA248.J42].
</LI>
<LI>
<A NAME="JonesMatijasevic"></A> [JonesMatijasevic] Jones, J. P.
and Y. V. Matijasevi&#269; (Matiyasevich), &quot;Proof of
Recursive Unsolvability of Hilbert's Tenth Problem,&quot; <I>American
Mathematical Monthly,</I> 98:689-709 (1991) [QA.A5125]; available at <A
HREF="https://www.williamstein.org/edu/Spring2003/21n/papers/hilbert10.pdf"
>https://www.williamstein.org/edu/Spring2003/21n/papers/hilbert10.pdf</A>
(retrieved 11 Nov 2014).
</LI>
<LI>
<A NAME="Juillerat"></A> [Juillerat] Jacob Juillerat, "Transcendental Numbers",
Lake Forest College, Senior Thesis, April 25, 2016 ; available at <A
HREF="https://publications.lakeforest.edu/seniortheses/62/">
https://publications.lakeforest.edu/seniortheses/62/</A>
(retrieved 5-Apr-2020).
</LI>
<LI>
<A NAME="JustWeese"></A> [JustWeese] Just, Winfried, and Martin Weese,
<I>Discovering Modern Set Theory I:  The Basics,</I> The American
Mathematical Society, Providence, R.I. (1995) [QA248.J87].
</LI>
<LI>
<A NAME="KalishMontague"></A> [KalishMontague] Kalish, D. and R.
Montague, &quot;On Tarski's formalization of predicate logic with
identity,&quot; <I>Archiv f&uuml;r Mathematische Logik und
Grundlagenforschung,</I> 7:81-101 (1965) [QA.A673]; available at <A
HREF="http://gdz.sub.uni-goettingen.de/dms/load/img/?PID=GDZPPN002043211"
>http://gdz.sub.uni-goettingen.de/dms/load/img/?PID=GDZPPN002043211</A>
(retrieved 29-Apr-2017).
</LI>
<LI>
<A NAME="Kalmbach"></A> [Kalmbach] Kalmbach, Gudrun <I>Orthomodular
Lattices</I>, Academic Press, London (1983) [QA171.5.K34].
</LI>
<LI>
<A NAME="KanamoriPincus"></A> [KanamoriPincus] Kanamori, A. and D.
Pincus, &quot;Does GCH Imply AC Locally?&quot;, in G&aacute;bor
Hal&aacute;sz, et al.(eds.), <I>Paul Erd&#337;s and his Mathematics,</I>
<I>Bolyai Society Mathematical Studies</I> 11:413-426, J&aacute;nos
Bolyai Mathematical Society, Budapest (2002) [QA1.P194 2002]; available
at <A HREF="http://math.bu.edu/people/aki/7.pdf"
>http://math.bu.edu/people/aki/7.pdf</A> (retrieved 4 Jun 2015).
</LI>
<LI>
<A NAME="Kreyszig"></A> [Kreyszig] Kreysig, Erwin, <I>Introductory
Functional Analysis with Applications</I>, John Wiley &amp; Sons, New
York (1989) [QA320.K74].
</LI>
<LI>
<A NAME="Kulpa"></A> [Kulpa] Kulpa, Wladislaw, "The Poincar&eacute;-
Miranda Theorem", <I>American Mathematical Monthly</I> 104:545-550 (1997);
available at <A HREF="https://www.jstor.org/stable/2975081">
https://www.jstor.org/stable/2975081</A> (retrieved 6 Feb 2019).
</LI>
<LI>
<A NAME="Kunen"></A> [Kunen] Kunen, Kenneth, <I>Set Theory:  An
Introduction to Independence Proofs,</I> Elsevier Science B.V.,
Amsterdam (1980) [QA248.K75].
</LI>
<LI>
<A NAME="KuratowskiMostowski"></A> [KuratowskiMostowski] Kuratowski, K.
and A. Mostowski, <I>Set Theory: with an Introduction to
Descriptive Set Theory,</I> 2nd ed., North-Holland,
Amsterdam (1976) [QA248.K7683 1976].
</LI>
<LI>
<A NAME="Lang"></A> [Lang] Serge Lang, <I>Algebra</I>, revised 3rd edition,
Graduate Texts in Mathematics, Springer-Verlag New York (2002)
[QA154.3.L3].
</LI>
<LI>
<A NAME="LarsonHostetlerEdwards"></A> [LarsonHostetlerEdwards]
Larson, Ron, Robert P. Hostetler, and Bruce H. Edwards, <I>Calculus:
Early Transcendental Functions,</I> 3rd ed., Houghton Mifflin Company
(2003) [QA303.L3274 2003]
</LI>
<LI>
<A NAME="LeBlanc"></A> [LeBlanc]  LeBlanc, Hugues,
"On Meyer and Lambert's Quantificational Calculus FQ,"
<I>J. Symb. Logic</I> 33:275-280 (1968)   [QA.J87].
</LI>
<LI>
<A NAME="Levy58"></A> [Levy58] L&eacute;vy, A., &quot;The independence
of various definitions of finiteness,&quot; <I>Fundamenta
Mathematicae</I>, 46:1-13 (1958) [QA.F981]
</LI>
<LI>
<A NAME="Levy"></A> [Levy] Levy, Azriel, <I>Basic Set Theory</I>,
Dover Publications, Mineola, N.Y. (2002) [QA248.L398 2002].
</LI>
<LI>
<A NAME="Lipparini"></A> [Lipparini] Lipparini, Paolo,
<I>A clean way to separate sets of surreals</I> arXiv:1712.03500 (20-May-2018);
available at <A HREF="https://arxiv.org/abs/1712.03500">
https://arxiv.org/abs/1712.03500</A> (retrieved 7 Dec 2021).
</LI>
<LI>
<A NAME="Lopez-Astorga"></A> [Lopez-Astorga] Lopez-Astorga, Miguel,
"The First Rule of Stoic Logic and its Relationship with the
Indemonstrables", <I>Revista de Filosof&iacute;a T&oacute;picos</I> (2016);
available at <A HREF="http://www.scielo.org.mx/pdf/trf/n50/n50a1.pdf">
http://www.scielo.org.mx/pdf/trf/n50/n50a1.pdf</A> (retrieved 3 Jul
2016).
</LI>
<LI>
<A NAME="MaedaMaeda"></A> [MaedaMaeda]  Maeda, Fumitomo (1897-1965)
and Shuichiro Maeda, <I>Theory of Symmetric Lattices</I>,
Springer-Verlag, New York (1970) [Q171.5.M184].
</LI>
<LI>
<A NAME="Margaris"></A> [Margaris] Margaris, Angelo, <I>First Order
Mathematical Logic,</I> Blaisdell Publishing Company, Waltham,
Massachusetts (1967) [QA9.M327].
</LI>
<LI>
<A NAME="McKMegPav"></A> [McKMegPav] McKay, B., N. Megill, and M.
Pavicic, &quot;Algorithms for Greechie Diagrams,&quot; <I>Int.  J.
Theor.  Phys.,</I> 39:2393-2417 (2000) [QC.I626]; available at  <A
HREF="http://xxx.lanl.gov/abs/quant-ph/0009039">
http://xxx.lanl.gov/abs/quant-ph/0009039</A>
(retrieved 11 Nov 2014).
</LI>
<LI>
<A NAME="Megill"></A><A NAME="bibmegill"></A> [Megill] Megill, N.,
&quot;A Finitely Axiomatized Formalization of Predicate Calculus with
Equality,&quot; <I>Notre Dame Journal of Formal Logic,</I> 36:435-453
(1995) [QA.N914]; available at
<A HREF="http://projecteuclid.org/euclid.ndjfl/1040149359"
>http://projecteuclid.org/euclid.ndjfl/1040149359</A> (retrieved
11 Nov 2014); the <A HREF="../downloads/finiteaxiom.pdf">PDF
preprint</A> has the same content (with corrections) but pages are
numbered 1-22, and the database references use the numbers printed on the
page itself, not the PDF page numbers.  See <A HREF="#technote">technical
note 1</A> above for some additional notes on this paper.
</LI>
<LI>
<A NAME="MegPav2000"></A> [MegPav2000] Megill, N. and M.
Pavi&#269;i&#263;, "Equations, States, and Lattices of
Infinite-Dimensional Hilbert Space," <I>Int.  J. Theor.  Phys.</I>
39:2337-2379 (2000) [QC.I626]; available at
<A HREF="http://xxx.lanl.gov/abs/quant-ph/0009038"
>http://xxx.lanl.gov/abs/quant-ph/0009038</A> (retrieved 11 Nov 2014).
</LI>
<LI>
<A NAME="MegPav2002"></A> [MegPav2002] Megill, N. and M.
Pavi&#269;i&#263; "Deduction, Ordering, and Operations in Quantum
Logic," <I>Found.  Phys.</I> 32:357-378 (2002) QC.F771; available at
<A HREF="http://xxx.lanl.gov/abs/quant-ph/0108074"
>http://xxx.lanl.gov/abs/quant-ph/0108074</A> (retrieved 11 Nov 2014).
</LI>
<LI>
<A NAME="Mendelson"></A> [Mendelson] Mendelson, Elliott, <I>Introduction to
Mathematical Logic,</I> 2nd ed., D. Van Nostrand (1979) [QA9.M537].
</LI>
<LI>
<A NAME="MertziosUnger"></A> [MertziosUnger] George B. Mertzios, Walter Unger,
<I>The friendship problem on graphs</I>,
ROGICS'08, 12-17 May 2008, Mahida, Tunisia, pp. 152-158, or Journal of
Multiple-Valued Logic and Soft Computing, Vol. 27(2-3), 2016, pp. 275-285 (Page
references in set.mm are for the ROGICS'08 paper); available at <A
HREF="http://community.dur.ac.uk/george.mertzios/papers/Conf/Conf_Windmills.pdf">
http://community.dur.ac.uk/george.mertzios/papers/Conf/Conf_Windmills.pdf</A>
(retrieved 28-Nov-2017).
</LI>
<LI>
<A NAME="Monk1"></A> [Monk1] Monk, J. Donald, <I>Introduction to Set
Theory,</I> McGraw-Hill, Inc. (1969) [QA248.M745].
</LI>
<LI>
<A NAME="Monk2"></A> [Monk2] Monk, J. Donald, &quot;Substitutionless
Predicate Logic with Identity,&quot; <I>Archiv f&uuml;r Mathematische
Logik und Grundlagenforschung,</I> 7:103-121 (1965) [QA.A673]; available
at <A HREF="http://euclid.colorado.edu/~~monkd/monk07.pdf"
>http://euclid.colorado.edu/~~monkd/monk07.pdf</A> (retrieved
29-Apr-2017) or <A
HREF="http://gdz.sub.uni-goettingen.de/dms/load/img/?PID=GDZPPN00204322X"
>http://gdz.sub.uni-goettingen.de/dms/load/img/?PID=GDZPPN00204322X</A>
(retrieved 29-Apr-2017).
</LI>
<LI>
<A NAME="Moore"></A>[Moore] Moore, Eliakim Hastings, <I>Introduction to
a Form of General Analysis,</I> Yale University Press, New Haven (1910)
[QA331.M78].
</LI>
<LI>
<A NAME="Moschovakis"></A> [Moschovakis] Moschovakis, Yiannis N.,
<I>Notes on Set Theory,</I> Springer, New York,
second edition (2006) [QA248.M665 2006].
</LI>
<LI>
<A NAME="Munkres"></A> [Munkres] Munkres, James Raymond,
<I>Topology:  a first course,</I> Prentice-Hall, Englewood Cliffs, New
Jersey (1975) [QA611.M82].
</LI>
<LI>
<LI>
<A NAME="Nathanson"></A> [Nathanson] Nathanson, Melvyn B.,
<I>Additive Number Theory: The Classical Bases</I> Springer-Verlag (1996) [QA241.N347 1996].
</LI>
<LI>
<A NAME="OeSilva"></A> [OeSilva] Tom&aacute;s Oliveira e Silva, Siegfried
Herzog, and Silvio Pardi, <I>Empirical verification of the even Goldbach
conjecture and computation of prime gaps up to 4 x 10^18,</I> Mathematics of
Computation, vol. 83, no. 288, pp. 2033-2060, July 2014 (published
electronically on November 18, 2013); available at
<A HREF="https://www.ams.org/journals/mcom/2014-83-288/S0025-5718-2013-02787-1/home.html">
https://www.ams.org/journals/mcom/2014-83-288/S0025-5718-2013-02787-1/home.html</A>.
</LI>
<LI>
<A NAME="Pfenning"></A> [Pfenning] Pfenning, Frank,
<I>Automated Theorem Proving,</I> Carnegie-Mellon University (April 13, 2004);
available at
<A HREF="http://www.cs.cmu.edu/~~fp/courses/atp/handouts/atp.pdf">
http://www.cs.cmu.edu/~~fp/courses/atp/handouts/atp.pdf</A>
and <A
HREF="http://web.archive.org/web/20160304013704/http://www.cs.cmu.edu/~~fp/courses/atp/handouts/atp.pdf">
http://web.archive.org/web/20160304013704/http://www.cs.cmu.edu/~~fp/courses/atp/handouts/atp.pdf</A>
(retrieved 7 Feb 2017).
</LI>
<LI>
<A NAME="Peano"></A> [Peano]
Peano, Giuseppe. <I>Arithmetices principia: Nove Methodo Ezposita</I>, 1889.
</LI>
<LI>
<A NAME="Ponnusamy"></A> [Ponnusamy] Ponnusamy, S., <I>Foundations
of Functional Analysis,</I> Alpha Science International Ltd., Pangbourne
(2002) [QA320.P66 2002].
</LI>
<LI>
<A NAME="PtakPulmannova"></A> [PtakPulmannova] Pavel Pt&aacute;k and
Sylvia Pulmannov&aacute;, <I>Orthomodular Structures as Quantum
Logics</I>, Kluwer Academic Publishers, Dordrecht (1991)
[QC174.17.M35P7713].
</LI>
<LI>
<A NAME="Quine"></A> [Quine] Quine, Willard van Orman, <I>Set Theory
and Its Logic,</I> Harvard University Press, Cambridge, Massachusetts,
revised edition (1969) [QA248.Q7 1969].
</LI>
<LI>
<A NAME="ReedSimon"></A> [ReedSimon] Michael Reed and Barry Simon,
<I>Methods of Modern Mathematical Physics</I>, Vol.  I:  Functional
Analysis, Academic Press, New York (1972) [QC20.7.F84.R43].
</LI>
<LI>
<A NAME="Roman"></A> [Roman] Steven Roman, <I>Advanced Linear Algebra</I>,
3rd edition, Graduate Texts in Mathematics, Springer Science+Business Media,
New York (2008) [QA184.R65 1992].
</LI>
<LI>
<A NAME="Rosenlicht"></a> [Rosenlicht] Maxwell Rosenlicht, <I>Introduction
to Analysis,</I> Dover Publications, Inc., New York (1986) [QA300.R63].
</LI>
<LI>
<A NAME="Rosser"></a> [Rosser] Rosser, John B.,
<I>Logic for Mathematicians</I>, Dover Publications, Mineola, N.Y. (2008)
[BC135.R58 2008].
</LI>
<LI>
<A NAME="RosserSchoenfeld"></a> [Rosser2] Rosser, J. Barkley and Schoenfeld, Lowell,
<I>Approximate formulas for some functions of prime numbers</I>, Illinois J. Math. 6:64-94 (1962);
available at <A
HREF="https://projecteuclid.org/journals/illinois-journal-of-mathematics/volume-6/issue-1/Approximate-formulas-for-some-functions-of-prime-numbers/10.1215/ijm/1255631807.full">Project Euclid</A>
(retrieved 27 Dec 2021).
</LI>
<LI>
<A NAME="Rotman"></A> [Rotman] Rotman, Joseph J., <I>The theory of
groups,</I> Allyn and Bacon, Inc., Boston (1973).
</LI>
<LI>
<A NAME="Rudin"></A> [Rudin] Rudin, Walter, <I>Principles of Mathematical
Analysis,</I> McGraw-Hill, New York, second edition (1964) [QA300.R916
1964].
</LI>
<LI>
<A NAME="Sanford"></A> [Sanford] Sanford, David H., <I>If P, then Q:
Conditionals and the Foundations of Reasoning</I>, 2nd ed., Routledge
Taylor &amp; Francis Group (2003); ISBN 0-415-28369-8; available at <A
HREF="https://books.google.com/books?id=h_AUynB6PA8C&amp;pg=PA39#v=onepage&amp;q&amp;f=false">https://books.google.com/books?id=h_AUynB6PA8C&amp;pg=PA39#v=onepage&amp;q&amp;f=false</A>
(retrieved 3 Jul 2016).
</LI>
<LI>
<A NAME="Schechter"></A> [Schechter] Schechter, Eric,
<I>Handbook of Analysis and Its Foundations</I>,
Academic Press, San Diego (1997) [QA300.S339].
</LI>
<LI>
<A NAME="Schloeder"></A> [Schloeder] Schl&ouml;der, Julian J., <I>Ordinal
Arithmetic</I>, Tutorial notes on Set Theory, Bonn (2012); available at <A
HREF="https://jjsch.github.io/output/oa.pdf">https://jjsch.github.io/output/oa.pdf</A>
(retrieved 5 Feb 2025).
</LI>
<LI>
<A NAME="Schwabhauser"></A> [Schwabhauser] Schwabhauser, Wolfram,
Wanda Szmielew, and Alfred Tarski, <I>Metamathematische Methoden in der
Geometrie</I>, Springer-Verlag, Berlin, New York (1983) [QA481.S38]
</LI>
<LI>
<A NAME="Shapiro"></A> [Shapiro] Shapiro, Harold N.,
<I>Introduction to the Theory of Numbers,</I>
Dover Publications, Inc. (2008) [QA241.S445 1983].
</LI>
<LI>
<A NAME="Stoll"></A> [Stoll] Stoll, Robert R., <I>Set Theory and Logic,</I>
Dover Publications, Inc. (1979) [QA248.S7985 1979].
</LI>
<LI>
<A NAME="Strang"></A> [Strang] Strang, Gilbert, <I>Calculus</I>, 1st
ed., Wellesley-Cambridge Press (1991) [QA303.S8839 1991]; ISBN
978-09802327-45; available at <A
HREF="http://ocw.mit.edu/resources/res-18-001-calculus-online-textbook-spring-2005/">
http://ocw.mit.edu/resources/res-18-001-calculus-online-textbook-spring-2005/</A>
(retrieved 24 Nov 2015).
</LI>
<LI>
<A NAME="Sullivan2004"></A> [Sullivan2004] Sullivan, Peter M,
"Frege's Logic", <I>Handbook of the History of Logic, Volume 3: The Rise of
Modern Logic from Leibniz to Frege</I>, Edited by Dov M. Gabbay and John WOods,
2004, Elsevier, ISBN 0-444-51611-5.
</LI>
<LI>
<A NAME="Suppes"></A> [Suppes] Suppes, Patrick, <I>Axiomatic Set Theory,</I>
Dover Publications, Inc. (1972) [QA248.S959].
</LI>
<LI>
<A NAME="Szendrei"></A> [Szendrei] Szendrei, &Aacute;gnes, <I>Clones in Universal Algebra</I>, Les Presses de l'Universit&eacute; de Montr&eacute;al, Montreal, Quebec (1986).
</LI>
<LI>
<A NAME="Siegrist"></A> [Siegrist] Siegrist, Kyle &amp;al
<I>Random: Probability, Mathematical Statistics, Stochastic Processes</I>
available at <A HREF="http://www.randomservices.org/random/index.html">
http://www.randomservices.org/random/index.html</A> (retrieved Oct 2017).
</LI>
<LI>
<A NAME="TakeutiZaring"></A> [TakeutiZaring] Takeuti, Gaisi, and
Wilson M. Zaring, <I>Introduction to Axiomatic Set Theory,</I>
Springer-Verlag, New York, second edition (1982) [QA248.T136 1982].
</LI>
<LI>
<A NAME="Tarski"></A> [Tarski] Tarski, Alfred, &quot;A Simplified
Formalization of Predicate Logic with Identity,&quot; <I>Archiv f&uuml;r
Mathematische Logik und Grundlagenforschung,</I> 7:61-79 (1965)
[QA.A673]; available at <A
HREF="http://gdz.sub.uni-goettingen.de/dms/load/img/?PID=GDZPPN002043203"
>http://gdz.sub.uni-goettingen.de/dms/load/img/?PID=GDZPPN002043203</A>
(retrieved 29-Apr-2017).
</LI>
<LI>
<A NAME="Tarski1999"></A> [Tarski1999] Tarski, Alfred, and Steven Givant,
&quot;Tarski's System of Geometry&quot;
<I>The Bulletin of Symbolic Logic</I>, Volume 5, Number 2, June 1999,
pp. 175-214.
</LI>
<LI>
<A NAME="Truss"></A> [Truss] Truss, John Kenneth, <I>Foundations of
Mathematical Analysis,</I> Oxford University Press, Oxford (1997)
[QA299.8.T78 1997].
</LI>
<LI>
<A NAME="vandenDries"></A> [vandenDries] van den Dries,  Lou,
&quot;Recursion Theory Notes, Fall 2011,&quot; available at <A
HREF="http://www.math.uiuc.edu/~~vddries/recursion.pdf"
>http://www.math.uiuc.edu/~~vddries/recursion.pdf</A>
(retrieved 11 Nov 2014).
</LI>
<LI>
<A NAME="Viaclovsky7"></A> [Viaclovsky7] Viaclovsky, Jeff, <I>Measurability
and Integration, Fall 2003, Lecture 7,</I> available at <A
HREF="https://ocw.mit.edu/courses/mathematics/18-125-measure-and-integration-fall-2003/lecture-notes/18125_lec7.pdf">
https://ocw.mit.edu/courses/mathematics/18-125-measure-and-integration-fall-2003/lecture-notes/18125_lec7.pdf
</A> (retrieved 23-Mar-2018).
</LI>
<LI>
<A NAME="Viaclovsky8"></A> [Viaclovsky8] Viaclovsky, Jeff, <I>Measurability
and Integration, Fall 2003, Lecture 8,</I> available at <A
HREF="https://ocw.mit.edu/courses/mathematics/18-125-measure-and-integration-fall-2003/lecture-notes/18125_lec8.pdf">
https://ocw.mit.edu/courses/mathematics/18-125-measure-and-integration-fall-2003/lecture-notes/18125_lec8.pdf
</A> (retrieved 21-Feb-2018).
</LI>
<LI>
<A NAME="Weierstrass"></A> [Weierstrass] Weierstra&szlig;, Karl,
<I>Zur Determinantentheorie,</I>
1886/87, posthumously published 1903 in &quot;Mathematische Werke&quot;,
vol. III, 271-287, J. Knoblauch,
Ed. Berlin: Mayer &amp; M&uuml;ller; available at <A
HREF="https://www.yumpu.com/de/document/read/20688945/mathematische-werke-von-karl-weierstrass-herausgegeben-unter-"
>https://www.yumpu.com/de/document/read/20688945/mathematische-werke-von-karl-weierstrass-herausgegeben-unter-</A>
(retrieved 18-Feb-2019).
</LI>
<LI>
<A NAME="WhiteheadRussell"></A> [WhiteheadRussell] Whitehead, Alfred
North, and Bertrand Russell, <I>Principia Mathematica to *56,</I>
Cambridge University Press, Cambridge, 1962 [QA9.W592 1962]; available
at <A
HREF="https://ia600602.us.archive.org/35/items/PrincipiaMathematicaVolumeI/WhiteheadRussell-PrincipiaMathematicaVolumeI_text.pdf"
>https://ia600602.us.archive.org/35/items/PrincipiaMathematicaVolumeI/WhiteheadRussell-PrincipiaMathematicaVolumeI_text.pdf</A>
(retrieved 22-Jan-2018).
</LI>
</OL>

<P>
<HR NOSHADE SIZE=1><A NAME="textonly"></A>
<B><FONT COLOR="#006633">Browsers and Fonts</FONT></B>

<P>
<A NAME="unicode"></A><B>
<FONT COLOR="#006633">Browsing with the Unicode font </FONT></B>
&nbsp;&nbsp;&nbsp;
By default, the Metamath Proof Explorer uses a Unicode font for math symbols.
Some browsers may render Unicode incorrectly, although the problem is becoming
less frequent.  On each page with a proof, at the top there is a link to switch
to the GIF version.  You will stay in the GIF directory (you will see "mpegif"
instead of "mpeuni" in the URL) until you switch back to the Unicode font
version on a page with a proof.
</P>

<!--
<P>
Unfortunately, Internet Explorer versions 6 and 7 do not implement some of the
standard Unicode math symbols, which is
<A HREF="../symbols/symbols.html#why">why</A> I chose GIF images as the
default.  The missing symbols are displayed as
<A HREF="../fontcompare.gif">blank rectangular boxes</A>, making the page
unreadable.  The free <A HREF="http://mozilla.org/">Firefox and
Mozilla</A> [retrieved 21-Dec-2016] browsers implement them correctly.
Safari on MacOS X (10.3.9) has also been reported to work.
</P>
-->

<P>
If you know of any 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
<A HREF="mmascii.html">ASCII token chart</A>.
</P>

<P>
<A NAME="font"></A><B><FONT COLOR="#006633">Display font</FONT></B>
&nbsp;&nbsp;&nbsp;
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 -&gt; Options -&gt; Content -&gt;
Default font.  In Internet Explorer 11, select (gear symbol) -&gt; Internet
Options -&gt; General -&gt; 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.
</P>

<!--
<P>
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.
</P>
-->

<P>
<B><FONT COLOR="#006633">Viewing with a text browser</FONT></B>
&nbsp;&nbsp;&nbsp;
The GIF version of the Metamath Proof Explorer can be viewed with a text-only
browser.  All symbols will be shown as the <A HREF="mmascii.html">ASCII
tokens</A> shown in the set.mm source file.  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 browser
<A HREF="http://w3m.sourceforge.net/">w3m</A> [retrieved 21-Dec-2016].
</P>

<P>
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&mdash;I would be interested in
any feedback on this.
</P>

<!--
<P>
<HR NOSHADE SIZE=1><A NAME="copyright"></A>
<B><FONT COLOR="#006633">Copyright Terms</FONT></B>
&nbsp;&nbsp;&nbsp;
All text and images displayed on this web page, other than any short
attributed quotations from other copyrighted sources, are placed in the
public domain by the author per the <A
HREF="https://creativecommons.org/publicdomain/zero/1.0/">Creative
Commons license CC0</A> [external].
</P>

<P>
<B>Exception.</B> Short quotations from copyrighted works, with
attribution, may appear on this page under the "fair use" provision of
Section 107 of the United States Copyright Act (Title 17 of the
<I>United States Code</I>).
</P>
-->

<HR NOSHADE SIZE=1>

<TABLE BORDER=0 WIDTH="100%">
<TR>
<TD ALIGN=LEFT VALIGN=TOP WIDTH="25%"><FONT SIZE=-2 FACE=sans-serif>
&nbsp;</FONT></TD>

<TD NOWRAP ALIGN=CENTER>
<I><FONT SIZE=-1>This page was last updated on 14-Jan-2024.</FONT></I>
<BR>
<FONT FACE="ARIAL" SIZE=-2>Your comments are welcome: Norman Megill
<A HREF="../email.html"><IMG BORDER=0 SRC="_nmemail.gif"
ALT="nm at alum dot mit dot edu"
TITLE="nm at alum dot mit dot edu"
WIDTH=90 HEIGHT=13 STYLE="margin-bottom:-3px"></A>
<BR>

<!--
<A HREF="../copyright.html">Copyright terms and conditions</A><BR>
-->
Copyright terms:
<A HREF="../copyright.html#pd">Public domain</A></FONT></TD>

<TD ALIGN=RIGHT VALIGN=BOTTOM WIDTH="25%">
<FONT FACE="ARIAL" SIZE=-2>
<A HREF="https://validator.w3.org/check?uri=referer">W3C validator</A>&nbsp;
&nbsp;<A HREF="https://www.google.com/webmasters/tools/mobile-friendly/">
Mobile test</A>
</FONT>
</TD>
</TR>
</TABLE>

<!--
<SCRIPT SRC="http://www.google-analytics.com/urchin.js" TYPE="text/javascript">
</SCRIPT>
<SCRIPT TYPE="text/javascript">
_uacct = "UA-1862729-1";
urchinTracker();
</SCRIPT>
-->

</BODY>
</HTML>