% This file, 'metamath.tex', is self-contained with everything needed to % generate the the PDF file 'metamath.pdf' on standard LaTeX installations. % The auxilliary files are embedded as comments. To generate metamath.pdf % file, run these commands under Linux or Cygwin in the directory that % contains 'metamath.tex': % % % grep "^%realref.sty%" metamath.tex | sed -e s/^%realref.sty%// > realref.sty % grep "^%bib%" metamath.tex | sed -e s/^%bib%// > metamath.bib % touch metamath.ind % pdflatex metamath % pdflatex metamath % bibtex metamath % makeindex metamath % pdflatex metamath % pdflatex metamath % % The warnings that occur in the initial runs of pdflatex can be ignored. % The final run should have no warnings (check metamath.log). % --------------------------- Start of realref.sty ----------------------------- %realref.sty%% Save the following as realref.sty (take off comment prefix %realref.sty%% tag on each line). %realref.sty%% You can then use it with \usepackage{realref} %realref.sty%% %realref.sty%% This has \pageref jumping to the page on which the ref appears, %realref.sty%% \ref jumping to the point of the anchor, and \sectionref %realref.sty%% jumping to the start of section. %realref.sty%% %realref.sty%% Author: Anthony Williams %realref.sty%% Software Engineer %realref.sty%% Nortel Networks Optical Components Ltd %realref.sty%% Date: 9 Nov 2001 (posted to comp.text.tex) %realref.sty%% %realref.sty%\ProvidesPackage{realref} %realref.sty%\RequirePackage[plainpages=false,pdfpagelabels=true]{hyperref} %realref.sty%\def\realref@anchorname{} %realref.sty%\AtBeginDocument{% %realref.sty%% ensure every label is a possible hyperlink target %realref.sty%\let\realref@oldrefstepcounter\refstepcounter% %realref.sty%\DeclareRobustCommand{\refstepcounter}[1]{\realref@oldrefstepcounter{#1} %realref.sty%\edef\realref@anchorname{\string #1.\@currentlabel}% %realref.sty%}% %realref.sty%\let\realref@oldlabel\label% %realref.sty%\DeclareRobustCommand{\label}[1]{\realref@oldlabel{#1}\hypertarget{#1}{}% %realref.sty%\@bsphack\protected@write\@auxout{}{% %realref.sty% \string\expandafter\gdef\protect\csname %realref.sty% page@num.#1\string\endcsname{\thepage}% %realref.sty% \string\expandafter\gdef\protect\csname %realref.sty% ref@num.#1\string\endcsname{\@currentlabel}% %realref.sty% \string\expandafter\gdef\protect\csname %realref.sty% sectionref@name.#1\string\endcsname{\realref@anchorname}% %realref.sty%}\@esphack}% %realref.sty%\DeclareRobustCommand\pageref[1]{{\edef\a{\csname %realref.sty% page@num.#1\endcsname}\expandafter\hyperlink{page.\a}{\a}}}% %realref.sty%\DeclareRobustCommand\ref[1]{{\edef\a{\csname %realref.sty% ref@num.#1\endcsname}\hyperlink{#1}{\a}}}% %realref.sty%\DeclareRobustCommand\sectionref[1]{{\edef\a{\csname %realref.sty% ref@num.#1\endcsname}\edef\b{\csname %realref.sty% sectionref@name.#1\endcsname}\hyperlink{\b}{\a}}}% %realref.sty%} % ---------------------------- End of realref.sty ------------------------------ %Book: Metamath %Author: Norman D. Megill Email: nm at alum.mit.edu % A book template example % http://www.stsci.edu/ftp/software/tex/bookstuff/book.template %\documentstyle[leqno]{book} % LaTeX 2.09 - obsolete \documentclass[leqno]{book} % hyperref 2002/05/27 v6.72r (couldn't get pagebackref to work) \usepackage[plainpages=false,pdfpagelabels=true]{hyperref} \usepackage{realref} % Restarting page numbers: try? % \printglossary % \cleardoublepage % \pagenumbering{arabic} % \setcounter{page}{1} ???needed % \include{chap1} % not used: % \def\R2Lurl#1#2{\mbox{\href{#1}\texttt{#2}}} \usepackage{amssymb} \raggedbottom \makeindex \begin{document} %%%%%%% load in AMS fonts %%%%%%% % LaTeX 2.09 - obsolete %\input{amssym.def} %\input{amssym.tex} %\input{c:/texmf/tex/plain/amsfonts/amssym.def} %\input{c:/texmf/tex/plain/amsfonts/amssym.tex} \bibliographystyle{plain} \pagenumbering{roman} \pagestyle{headings} \thispagestyle{empty} \hfill \vfill \begin{center} {\LARGE\bf Metamath} \\ \vspace{1ex} {\large A Computer Language for Pure Mathematics} \\ \vspace{7ex} {\large Norman D. Megill} \end{center} \vfill \hfill \newpage \thispagestyle{empty} \hfill \vfill \begin{center} Copyright (C) 1997, 2002, 2003, 2004 by Norman D. Megill \vspace{1ex} {\small This book is distributed under the terms of the GNU Free Documentation License \url{http://www.gnu.org/licenses/fdl.html}} % \vspace{1ex} % % \vspace{1ex} % {\small Permission is granted to make and distribute verbatim copies of this % book % provided the copyright notice and this % permission notice are preserved on all copies.} % % \vspace{1ex} % {\small Permission is granted to copy and distribute modified versions of this % book under the conditions for verbatim copying, provided that the % entire % resulting derived work is distributed under the terms of a permission % notice % identical to this one.} % % \vspace{1ex} % {\small Permission is granted to copy and distribute translations of this % book into another language, under the above conditions for modified % versions, % except that this permission notice may be stated in a translation % approved by the % author.} % % \vspace{1ex} % %{\small For a copy of the \LaTeX\ source files for this book, contact % %the author.} \\ % \ \\ % \ \\ \hfill \vfill Norman D. Megill\\ 19 Locke Lane, Lexington, MA 02420 \\ E-mail address: \texttt{nm @ alum.mit.edu} \\ See notes added at end of Preface for revision history. \\ For current information on the Metamath software see \\ \url{http://metamath.org}. \end{center} \newpage \thispagestyle{empty} \hfill \vfill \begin{center} {\it To my son Robin Dwight Megill} \end{center} \vfill \hfill \newpage \tableofcontents %\listoftables \chapter*{Preface} \markboth{PREFACE}{PREFACE} \addcontentsline{toc}{section}{Preface} (For current information, see the notes added at the end of this preface on p.~\pageref{note2002}.) \subsubsection{Overview} Metamath\index{Metamath} is a computer language and an associated computer program for archiving, verifying, and studying mathematical proofs at a very detailed level. The Metamath language incorporates no mathematics per se but treats all mathematical statements as mere sequences of symbols. You provide Metamath with certain special sequences (axioms) that tell it what rules of inference are allowed. Metamath is not limited to any specific field of mathematics. The Metamath language is simple and robust, with an almost total absence of hard-wired syntax, and I believe that it provides about the simplest possible framework that allows essentially all of mathematics to be expressed with absolute rigor. % index test %\newcommand{\nn}[1]{#1n} %\index{aaa@bbb} %\index{abc!def} %\index{abd|see{qqq}} %\index{abe|nn} %\index{abf|emph} %\index{abg|(} %\index{abg|)} Using the Metamath language, you can build formal or mathematical systems\index{formal system}\footnote{A formal or mathematical system consists of a collection of symbols (such as $2$, $4$, $+$ and $=$), syntax rules that describe how symbols may be combined to form a legal expression (called a well-formed formula or {\em wff}, pronounced ``whiff''), some starting wffs called axioms, and inference rules that describe how theorems may be derived (proved) from the axioms. A theorem is a mathematical fact such as $2+2=4$. Strictly speaking, even an obvious fact such as this must be proved from axioms to be formally acceptable to a mathematician.}\index{theorem} \index{axiom}\index{rule}\index{well-formed formula (wff)} that involve inferences from axioms. Although a database is provided that includes a recommended set of axioms for standard mathematics, if you wish you can supply your own symbols, syntax, axioms, rules, and definitions. The name ``Metamath'' was chosen to suggest that the language provides a means for {\em describing} mathematics rather than being the mathematics itself. Actually in some sense any mathematical language is metamathematical. Symbols written on paper, or stored in a computer, are not mathematics itself but rather a way of expressing mathematics. For example ``7'' and ``VII'' are symbols for denoting the number seven in Arabic and Roman numerals; neither {\em is} the number seven. If you are able to understand and write computer programs, you should be able to follow abstract mathematics with the aid of Metamath. Used in conjunction with standard textbooks, Metamath can guide you step-by-step towards an understanding of abstract mathematics from a very rigorous viewpoint, even if you have no formal abstract mathematics background. By using a single, consistent notation to express proofs, once you grasp its basic concepts Metamath provides you with the ability to immediately follow and dissect proofs even in totally unfamiliar areas. Of course, just being able follow a proof will not necessarily give you an intuitive familiarity with mathematics. Memorizing the rules of chess does not give you the ability to appreciate the game of a master, and knowing how the notes on a musical score map to piano keys does not give you the ability to hear in your head how it would sound. But each of these can be a first step. Metamath allows you to explore proofs in the sense that you can see the theorem referenced at any step expanded in as much detail as you want, right down to the underlying axioms of logic and set theory (in the case of the set theory database provided). While Metamath will not replace the higher-level understanding that can only be acquired through exercises and hard work, being able to see how gaps in a proof are filled in can give you increased confidence that can speed up the learning process and save you time when you get stuck. The Metamath language breaks down a mathematical proof into its tiniest possible parts. These can be pieced together, like interlocking pieces in a puzzle, only in a way that produces correct and absolutely rigorous mathematics. The nature of Metamath\index{Metamath} enforces very precise mathematical thinking, similar to that involved in writing a computer program. A crucial difference, though, is that once a proof is verified (by the Metamath program) to be correct, it is definitely correct; it can never have a hidden ``bug.''\index{computer program bugs} After getting used to the kind of rigor and accuracy provided by Metamath, you might even be tempted to adopt the attitude that a proof should never be considered correct until it has been verified by a computer, just as you would not completely trust a manual calculation until you have verified it on a calculator. My goal for Metamath was a system for describing and verifying mathematics that is completely universal yet conceptually as simple as possible. In approaching mathematics from an axiomatic, formal viewpoint, I wanted Metamath to be able to handle almost any mathematical system, not necessarily with ease, but at least in principle and hopefully in practice. I wanted it to verify proofs with absolute rigor, and for this reason Metamath is what might be thought of as a ``compile-only'' language rather than an algorithmic or Turing-machine language (Pascal, C, Prolog, Mathematica, etc.). In other words, a ``program'' (database) written in the Metamath language doesn't ``do'' anything; it merely exhibits mathematical knowledge and permits this knowledge to be verified as being correct. A program in an algorithmic language can potentially have hidden bugs\index{computer program bugs} as well as possibly being hard to understand. But each token in a Metamath database must be consistent with the database's earlier contents according to simple, fixed rules, and if a database is syntactically correct,\footnote{Here the notion of verifying correctness of syntax includes verification that a sequential list of proof steps results in the specified theorem.} then the mathematical content is correct with absolute certainty (or at least to the certainty of the verification program, which is relatively simple). The only ``bugs'' that can exist are in the statement of the axioms, for example if the axioms are inconsistent (a famous problem shown to be unsolvable by G\"{o}del's incompleteness theorem\index{G\"{o}del's incompleteness theorem}). Metamath doesn't prove theorems automatically but is designed to verify proofs that you supply to it. Metamath is completely general and has no built-in, preconceived notions about your formal system\index{formal system}, its logic or its syntax, but the price for its generality is that it does not lend itself well to automated proofs in its most general form. (In principle it could accept translated proofs from other, more specific theorem proving programs, although nothing along those lines has been done so far.) For constructing proofs, the Metamath program has a Proof Assistant\index{Proof Assistant} which helps you fill in some of a proof step's details, shows you what choices you have at any step, and verifies the proof as you build it; but you are still expected to provide the proof. Like most computer languages, the Metamath\index{Metamath} language uses the standard ({\sc ascii}) characters on a computer keyboard, so it cannot directly represent many of the special symbols that mathematicians use. A useful feature of the Metamath program is its ability to convert its notation into the \LaTeX\ typesetting language.\index{latex@{\LaTeX}} This feature lets you convert the {\sc ascii} tokens you've defined into standard mathematical symbols, so you end up with symbols and formulas you are familiar with instead of somewhat cryptic {\sc ascii} representations of them. Metamath is probably conceptually different from anything you've seen before and some aspects may take some getting used to. This book will help you decide whether Metamath suits your specific needs. \subsubsection{Setting Your Expectations} It is important for you to understand what Metamath\index{Metamath} is and is not. As mentioned, Metamath is {\em not} an automated theorem prover but rather a proof verifier. Developing a database can be tedious, hard work, especially if you want to make the proofs as short as possible, but it becomes easier as you build up a collection of useful theorems. The purpose of Metamath is simply to document existing mathematics in an absolutely rigorous, computer-verifiable way, not to aid directly in the creation of new mathematics. It also is not a magic solution for learning abstract mathematics, although it may be helpful to be able to actually see the implied rigor behind what you are learning from textbooks, as well as providing hints to work out proofs that you are stumped on. As of this writing, a sizable set theory database has been developed to provide a foundation for many fields of mathematics, but much more work would be required to develop useful databases for specific fields. Metamath\index{Metamath} ``knows no math;'' it just provides a framework in which to express mathematics. Its language is very small. You can define two kinds of symbols, constants\index{constant} and variables\index{variable}. The only thing Metamath knows how to do is to substitute strings of symbols for the variables\index{substitution!variable}\index{variable substitution} in an expression based on instructions you provide it in a proof, subject to certain constraints you specify for the variables. Even the decimal representation of a number is merely a string of certain constants (digits) which together, in a specific context, correspond to whatever mathematical object you choose to define for it; unlike other computer languages, there is no actual number stored inside the computer. In a proof, you in effect instruct Metamath what symbol substitutions to make in previous axioms or theorems and join a sequence of them together to result in the desired theorem. This kind of symbol manipulation captures the essence of mathematics at a preaxiomatic level. \subsubsection{Metamath and Mathematical Literature} In advanced mathematical literature, proofs are usually presented in the form of short outlines that often only an expert can follow. This is partly out of a desire for brevity, but it would also be unwise (even if it were practical) to present proofs in complete formal detail, since the overall picture would be lost.\index{formal proof} A solution I envision\label{envision} that would allow mathematics to remain acceptable to the expert, yet increase its accessibility to non-specialists, consists of a combination of the traditional short, informal proof in print accompanied by a complete formal proof stored in a computer database. In an analogy with a computer program, the informal proof is like a set of comments that describe the overall reasoning and content of the proof, whereas the computer database is like the actual program and provides a means for anyone, even a non-expert, to follow the proof in as much detail as desired, exploring it back through layers of theorems (like subroutines that call other subroutines) all the way back to the axioms of the theory. In addition, the computer database would have the advantage of providing absolute assurance that the proof is correct, since each step can be verified automatically. There are several other approaches besides Metamath to a project such as this. Section~\ref{proofverifiers} discusses some of these. To me, a noble goal would be a {\sc cd rom} with hundreds of thousands of theorems and their computer-verifiable proofs, encompassing a significant fraction of known mathematics and available for instant access. Whether or not Metamath is an appropriate choice remains to be seen, but in principle I believe it is sufficient. \subsubsection{Formalism} Over the past fifty years, a group of French mathematicians working collectively under the pseudonym of Bourbaki\index{Bourbaki, Nicholaus} have co-authored a series of monographs that attempt to rigorously and consistently formalize large bodies of mathematics from foundations. On the one hand, certainly such an effort has its merits; on the other hand, the Bourbaki project has been criticized for its ``scholasticism'' and ``hyperaxiomatics'' that hide the intuitive steps that lead to the results \cite[p.~191]{Barrow}\index{Barrow, John D.}. Metamath unabashedly carries this philosophy to its extreme and no doubt is subject to the same kind of criticism. Nonetheless I think that in conjunction with conventional approaches to mathematics Metamath can serve a useful purpose. The Bourbaki approach is essentially pedagogic, requiring the reader to become intimately familiar with each detail in a very large hierarchy before he or she can proceed to the next step. The difference with Metamath is that the ``reader'' (user) knows that all details are contained in its computer database, available as needed; it does not demand that the user know everything but conveniently makes available those portions that are of interest. As the body of all mathematical knowledge grows larger and larger, no one individual can have a thorough grasp of its entirety. Metamath can finalize and put to rest any questions about the validity of any part of it and can make any part of it accessible, in principle, to a non-specialist. \subsubsection{A Personal Note} Why did I develop Metamath\index{Metamath}? I enjoy abstract mathematics, but I sometimes get lost in a barrage of definitions and start to lose confidence that my proofs are correct. Or I reach a point where I lose sight of how anything I'm doing relates to the axioms that a theory is based on and am sometimes suspicious that there may be some overlooked implicit axiom accidentally introduced along the way (as happened historically with Euclidean geometry\index{Euclidean geometry}, whose omission of Pasch's axiom\index{Pasch's axiom} went unnoticed for 2000 years \cite[p.~160]{Davis}!). I'm also somewhat lazy and wish to avoid the effort involved in re-verifying the gaps in informal proofs ``left to the reader;'' I prefer to figure them out just once and not have to go through the same frustration a year from now when I've forgotten what I did. Metamath provides better recovery of my efforts than scraps of paper that I can't decipher anymore. But mostly I find very appealing the idea of rigorously archiving mathematical knowledge in a computer database, providing precision, certainty, and elimination of human error. \subsubsection{Note on Bibliography and Index} The Bibliography usually includes the Library of Congress classification for a work to make it easier for you to find it in on a university library shelf. The Index has author references to pages where their works are cited, even though the authors' names may not appear on those pages. \subsubsection{Acknowledgments} Acknowledgments are first due to my wife, Deborah, for critiquing the manu\-script but most of all for her patience and support. I also wish to thank Joe Wright, Richard Becker, Clarke Evans, Buddha Buck, and Jeremy Henty for helpful comments. Any errors, omissions, and other shortcomings are of course my responsibility. \subsubsection{Note Added January 6, 2002}\label{note2002} Except for the correction of a few typographical errors, found by Josh Purinton, the text of this book is the same as the original edition written in 1997. Some additional features, such as the ability to produce web pages, have been added to the Metamath program that are not shown in Chapter~\ref{commands}, and some of the commands have slightly different or additional switches or defaults. The examples herein should work as shown, but the built-in help in the command-line interface should be relied upon as the authoritative reference, rather than Chapter~\ref{commands}, which I hope to update at some point in the future. The method of producing \LaTeX\ files has changed; see the \texttt{help latex} in the program. See \texttt{help html} for information on how to produce web pages. Current information can always be obtained at \url{http://metamath.org}. The book has been converted to \LaTeX\ 2$\epsilon$ and PDF with hyperlinks, resulting in a different page numbering than the 1997 edition. My wife Deborah passed away on September 4, 1998. \subsubsection{Note Added May 20, 2003}\label{note2003} Previous editions had an appendix called ``Metamath's Formal System.'' Bob Solovay\index{Solovay, Bob} discovered an error in it. Since that appendix is not important to the rest of the text, I removed it for now, until I can find time to correct it. (For the sufficiently curious, that appendix, preceded by Bob's remarks, is retained as a comment in the \LaTeX\ source file for this book, \texttt{metamath.tex}.) Bob also communicated a new result of A.~R.~D.~Mathias on the system of Bourbaki, and the text has been updated accordingly (p.~\pageref{bourbaki}). Finally, Bob pointed out a clarification of the literature regarding category theory and inaccessible cardinals\index{category theory}\index{cardinal, inaccessible} (p.~\pageref{categoryth}), and a misleading statement was removed from the text. Specifically, contrary to a statement in previous editions, it is possible to express ``There is a proper class of inaccessible cardinals'' in the language of ZFC. This can be done as follows: "For every set $x$ there is an inaccessible cardinal $\kappa$ such that $\kappa$ is not in $x$." Bob writes:\footnote{Private communication, Nov.~30, 2002.} \begin{quotation} This axiom is how Grothendieck presents category theory. To each inaccessible cardinal $\kappa$ one associates a Grothendieck universe \index{Grothendieck, Alexander} $U(\kappa)$. $U(\kappa)$ consists of those sets which lie in a transitive set of cardinality less than $\kappa$. Instead of the ``category of all groups,'' one works relative to a universe [considering the category of groups of cardinality less than $\kappa$]. Now the category whose objects are all categories ``relative'' to the universe $U(\kappa)$'' will be a category not relative to this universe but to the next universe. All of the things category theorists like to do can be done in this framework. The only controversial point is whether the Grothen\-dieck axiom is too strong for the needs of category theorists. Mac Lane \index{Mac Lane, Saunders} argues that ``one universe is enough'' and Feferman\index{Feferman, Solomon} has argued that one can get by with ordinary ZFC. I don't find Feferman's arguments persausive. Mac Lane may be right, but when I think about category theory I do it \`{a} la Grothendieck. By the way Mizar\index{Mizar} adds the axiom ``there is a proper class of inaccessibles'' precisely so as to do category theory. \end{quotation} The Metamath command list in Chapter~\ref{commands}, although for the most part correct, still reflects the 1997 version of the program. % I % hope to update it, to borrow a phrase from Bob Solovay's web site % (originally popularized by Jerry Pournelle's\index{Pournelle, Jerry} % column in {\sc byte} magazine), ``real soon now.'' I hope to update it at some point, but in the meantime the on-line help in the current version of the Metamath program provides the definitive reference. Similar comments apply to that material in Chapter~\ref{fol} taken from the \texttt{set.mm} database as it existed at that time. There are references in the text to software packages and web sites that were current in 1997 but are now out of date. These are constantly subject to change, of course. I do not plan to update these frequently or even in the near future, and they should be viewed from a historical perspective. The interested reader can usually find current references using search engines such as Google. \subsubsection{Note Added November 20, 2003}\label{note2003b} About a dozen minor typos found by One Hand Clapping have been corrected. \subsubsection{Note Added April 2, 2004}\label{note2004} I corrected Appendix~\ref{formalspec} (that was removed on May 20, 2003; see the note above) and added it back in. In addition, the Axiom of Replacement in Section~\ref{mmsettheoryaxioms} was revised to a somewhat more standard version that should be easier to understand. \subsubsection{Note Added May 22, 2004}\label{note2004b} About a half a dozen minor typos found by Josh Purinton have been corrected. A technical change he suggested simplified the definition of the closure of a pre-statement of formal system in Appendix~\ref{formalspec}. \subsubsection{Note Added September 14, 2004}\label{note2004c} In the Metamath specification (Section~\ref{spec}), ``Each variable in a \texttt{\$e}, \texttt{\$d}, \texttt{\$a}, or \texttt{\$p} statement must exist in an active \texttt{\$f} statement'' was changed to ``Each variable in a \texttt{\$e}, \texttt{\$a}, or \texttt{\$p} statement must exist in an active \texttt{\$f} statement.'' The former requirement was unnecessarily restrictive. Thanks to Mr.\ Mel L.\ O'Cat for pointing this out. \chapter{Introduction} \pagenumbering{arabic} \begin{quotation} {\em {\em I.M.:} No, no. There's nothing subjective about it! Everybody knows what a proof is. Just read some books, take courses from a competent mathematician, and you'll catch on. {\em Student:} Are you sure? {\em I.M.:} Well---it is possible that you won't, if you don't have any aptitude for it. That can happen, too. {\em Student:} Then {\em you} decide what a proof is, and if I don't learn to decide in the same way, you decide I don't have any aptitude. {\em I.M.:} If not me, then who?} \flushright\sc ``The Ideal Mathematician'' \index{Davis, Phillip J.} \footnote{\cite{Davis}, p.~40}\\ \end{quotation} In the past century, brilliant mathematicians have discovered almost unimaginably profound results that rank among the crowning intellectual achievements of mankind. However, there is a sense in which modern abstract mathematics is behind the times, stuck in an era before computers existed. While no one disputes the remarkable results that have been achieved, communicating these results in a precise way to the uninitiated is virtually impossible. To describe these results, a terse informal language is used which despite its elegance is very difficult to learn. This informal language is not imprecise, far from it, but rather it often has omitted detail and symbols with hidden context that are implicitly understood by an expert but few others. Extremely complex technical meanings are associated with innocent-sounding English words such as ``compact'' and ``measurable'' that barely hint at what is actually being said. Anyone who does not keep the precise technical meaning constantly in mind is bound to fail, and acquiring the ability to do this can be achieved only through much practice and hard work. Only the few who complete the painful learning experience can join the small in-group of pure mathematicians. The informal language effectively cuts off the true nature of their knowledge from most everyone else. Metamath\index{Metamath} makes abstract mathematics more concrete. It allows a computer to keep track of the complexity associated with each word or symbol with absolute rigor. You can explore this complexity at your leisure, to whatever degree you desire. Whether or not you believe that concepts such as infinity actually ``exist'' outside of the mind, Metamath lets you get to the foundation for what's really being said. Its language is simple enough so that you don't have to rely on the authority of experts but can verify the results yourself, step by step. If you want to attempt to derive your own results, Metamath will not let you make a mistake in reasoning. ``Metamath''\index{Metamath} is the name of a mathematical computer language that describes formal\index{formal system} mathematical systems and expresses proofs of theorems in those systems. Such a language is called a metalanguage\index{metalanguage} by mathematicians. ``Metamath'' is also the name of a computer program that verifies proofs expressed in the language. The Metamath program does not have the built-in ability to make logical inferences; it just makes a series of symbol substitutions according to instructions given to it in a proof and verifies that the result matches the expected theorem. It makes logical inferences based only on rules of logic that are contained in a set of axioms\index{axiom}, or first principles, that you provide to it as the starting point for proofs. The complete specification of the Metamath language is only four pages long (Section~\ref{spec}, p.~\pageref{spec}). Its simplicity may at first make you may wonder how it can do much of anything at all. But in fact the kinds of symbol manipulations it performs are the ones that are implicitly done in all mathematical systems at the lowest level. You can learn it relatively quickly and have complete confidence in any mathematical proof that it verifies. On the other hand, it is powerful and general enough so that virtually any mathematical theory, from the most basic to the deeply abstract, can be described with it. Although in principle Metamath can be used with any kind of mathematics, it is best suited for abstract or ``pure'' mathematics that is mostly concerned with theorems and their proofs, as opposed to the kind of mathematics that deals with the practical manipulation of numbers. Examples of branches of pure mathematics are logic\index{logic},\footnote{Logic is the study of statements that are universally true regardless of the objects being described by the statements. An example is the statement, ``if $P$ implies $Q$, then either $P$ is false or $Q$ is true.''} set theory\index{set theory},\footnote{Set theory is the study of general-purpose mathematical objects called ``sets,'' and from it essentially all of mathematics can be derived. For example, numbers can be defined as specific sets, and their properties can be explored using the tools of set theory.} number theory\index{number theory},\footnote{Number theory deals with the properties of positive and negative integers (whole numbers).} group theory\index{group theory},\footnote{Group theory studies the properties of mathematical objects called groups that obey a simple set of axioms and have properties of symmetry that make them useful in many other fields.} abstract algebra\index{abstract algebra},\footnote{Abstract algebra includes group theory and also studies groups with additional properties that qualify them as ``rings'' and ``fields.'' The set of real numbers is a familiar example of a field.}, analysis\index{analysis} \index{real and complex numbers}\footnote{Analysis is the study of real and complex numbers.} and topology\index{topology}.\footnote{One area studied by topology are properties that remain unchanged when geometrical objects undergo stretching deformations; for example a doughnut and a coffee cup each have one hole (the cup's hole is in its handle) and are thus considered topologically equivalent. In general, though, topology is the study of abstract mathematical objects that obey a certain (surprisingly simple) set of axioms. See, for example, Munkres \cite{Munkres}\index{Munkres, James R.}.} Even in physics, Metamath could be applied to certain branches that make use of abstract mathematics, such as quantum logic\index{quantum logic} (used to study aspects of quantum mechanics\index{quantum mechanics}). On the other hand, Metamath\index{Metamath} is less suited to applications that deal primarily with intensive numeric computations. Metamath does not have any built-in representation of numbers\index{Metamath!representation of numbers}; instead, a specific string of symbols (digits) must be syntactically constructed as part of any proof in which an ordinary number is used. For this reason, numbers in Metamath are best limited to specific constants that arise during the course of a theorem or its proof. Numbers are only a tiny part of the world of abstract mathematics. The exclusion of built-in numbers was a conscious decision to help achieve Metamath's simplicity, and there are other software tools such as the computer algebra programs\index{computer algebra system} {\sc macsyma}\index{macsyma@{\sc macsyma}}, Mathematica\index{Mathematica}, and Maple\index{Maple} specifically suited to handling numbers efficiently. After learning Metamath's basic statement types, any tech\-ni\-cal\-ly ori\-ent\-ed person, mathematician or not, can immediately trace any theorem proved in the language as far back as he or she wants, all the way to the axioms on which the theorem is based. This ability suggests a non-traditional way of learning about pure mathematics. Used in conjunction with traditional methods, Metamath could make pure mathematics accessible to people who are not sufficiently skilled to figure out the implicit detail in ordinary textbook proofs. Once you learn the axioms of a theory, you can have complete confidence that everything you need to understand a proof you are studying is all there, at your beck and call, allowing you to focus in on any proof step you don't understand in as much depth as you need, without worrying about getting stuck on a step you can't figure out.\footnote{On the other hand, writing proofs in the Metamath language is challenging, requiring a degree of rigor far in excess of that normally taught to students. In a classroom setting, I doubt that writing Metamath proofs would ever replace traditional homework exercises involving informal proofs, because the time needed to work out the details would not allow a course to cover much material. For students who have trouble grasping the implied rigor in traditional material, writing a few simple proofs in the Metamath language might help clarify fuzzy thought processes. Although somewhat difficult at first, it eventually becomes fun to do, like solving a puzzle, because of the instant feedback provided by the computer.} Metamath\index{Metamath} is probably unlike anything you have encountered before. In this first chapter we will look at the philosophy and use of computers in mathematics in order to better understand the motivation behind Metamath. The material in this chapter is not required in order to use Metamath. You may skip it if you are impatient, but I hope you will find it educational and enjoyable. If you want to start experimenting with the Metamath program right away, proceed directly to Chapter~\ref{using} (p.~\pageref{using}). To learn the Metamath language, skim Chapter~\ref{using} then proceed to Chapter~\ref{languagespec} (p.~\pageref{languagespec}). \section{Mathematics as a Computer Language} \begin{quote} {\em The study of mathematics is apt to commence in dis\-ap\-point\-ment.\ldots \\ We are told that by its aid the stars are weighted and the billions of molecules in a drop of water are counted. Yet, like the ghost of Hamlet's father, this great science eludes the efforts of our mental weapons to grasp it.} \flushright\sc Alfred North Whitehead\footnote{\cite{Whitehead}, ch.\ 1}\\ \end{quote}\index{Whitehead, Alfred North} \subsection{Is Mathematics ``User-Friendly''?} Suppose you have no formal training in abstract mathematics. But popular books you've read offer tempting glimpses of this world filled with profound ideas that have stirred the human spirit. You are not satisfied with the informal, watered-down descriptions you've read but feel it is important to grasp the underlying mathematics itself to understand its true meaning. It's not practical to go back to school to learn it, though; you don't want to dedicate years of your life to it. There are many important things in life, and you have to set priorities for what's important to you. What would happen if you tried to pursue it on your own, in your spare time? After all, you were able to learn a computer programming language such as Pascal on your own without too much difficulty, even though you had no formal training in computers. You don't claim to be an expert in software design, but you can write a passable program when necessary to suit your needs. Even more important, you know that you can look at anyone else's Pascal program, no matter how complex, and with enough patience figure out exactly how it works, even though you are not a specialist. Pascal allows you do anything that a computer can do, at least in principle. Thus you know you have the ability, in principle, to follow anything that a computer program can do: you just have to break it down into small enough pieces. Here's an imaginary scenario of what might happen if you na\-ive\-ly a\-dopted this same view of abstract mathematics and tried to pick it up on your own, in a period of time comparable to, saying, learning a computer programming language. \subsubsection{A Non-Mathematician's Quest for Truth} \begin{quote} {\em \ldots my daughters have been studying (chemistry) for several se\-mes\-ters, think they have learned differential and integral calculus in school, and yet even today don't know why $x\cdot y=y\cdot x$ is true.} \flushright\sc Edmund Landau\footnote{\cite{Landau}, p.~vi}\\ \end{quote}\index{Landau, Edmund} \begin{quote} {\em Minus times minus is plus,\\ The reason for this we need not discuss.} \flushright\sc W.\ H.\ Auden\footnote{As quoted in \cite{Guillen}, p.~64}\\ \end{quote}\index{Auden, W.\ H.}\index{Guillen, Michael} We'll suppose you are technically oriented professional, perhaps an engineer, a computer programmer, or a physicist, but probably not a mathematician. You consider yourself reasonably intelligent. You did well in school, learning a variety of methods and techniques in practical mathematics such as calculus and differential equations. But rarely did your courses get into anything resembling modern abstract mathematics, and proofs were something that appeared only occasionally in your textbooks, a kind of necessary evil that was supposed to convince you of a certain key result. Most of your homework consisted of exercises that gave you practice in the techniques, and you were hardly ever asked to come up with a proof of your own. You find yourself curious about advanced, abstract mathematics. You are driven by an inner conviction that it is important to understand and appreciate some of the most profound knowledge discovered by mankind. But it seems very hard to learn, something that only certain gifted longhairs can access and understand. You are frustrated that it seems forever cut off from you. Eventually your curiosity drives you to do something about it. You set for yourself a goal of ``really'' understanding mathematics: not just how to manipulate equations in algebra or calculus according to cookbook rules, but rather to gain a deep understanding of where those rules come from. In fact, you're not thinking about this kind of ordinary mathematics at all, but about a much more abstract, ethereal realm of pure mathematics, where famous results such as G\"{o}del's incompleteness theorem\index{G\"{o}del's incompleteness theorem} and Cantor's different kinds of infinities reside. You have probably read a number of popular books, with titles like {\em Infinity and the Mind} \cite{Rucker}\index{Rucker, Rudy}, on topics such as these. You found them inspiring but at the same time somewhat unsatisfactory. They gave you a general idea of what these results are about, but if someone asked you to prove them, you wouldn't have the faintest idea of where to begin. Sure, you could give the same overall outline that you learned from the popular books; and in a general sort of way, you do have an understanding. But deep down inside, you know that there is a rigor that is missing, that probably there are many subtle steps and pitfalls along the way, and ultimately it seems you have to place your trust in the experts in the field. You don't like this; you want to be able to verify these results for yourself. So where do you go next? As a first step, you decide to look up some of the original papers on the theorems you are curious about, or better, obtain some standard textbooks in the field. You look up a theorem you want to understand. Sure enough, it's there, but it's expressed with strange terms and odd symbols that mean absolutely nothing to you. It might as well be written in a foreign language you've never seen before, whose symbols are totally alien. You look at the proof, and you haven't the foggiest notion what each step means, much less how one step follows from another. Well, obviously you have a lot to learn if you want to understand this stuff. You feel that you could probably understand it by going back to college for another three to six years and getting a math degree. But that does not fit in with your career and the other things in your life and would serve no practical purpose. You decide to seek a quicker path. You figure you'll just trace your way back to the beginning, step by step, as you would do with a computer program, until you understand it. But you quickly find that this is not possible, since you can't even understand enough to know what you have to trace back to. Maybe a different approach is in order---maybe you should start at the beginning and work your way up. First, you read the introduction to the book to find out what the prerequisites are. In a similar fashion, you trace your way back through two or three more books, finally arriving at one that seems to start at a beginning: it lists the axioms of arithmetic. ``Aha!'' you naively think, ``This must be the starting point, the source of all mathematical knowledge.'' Or at least the starting point for mathematics dealing with numbers; you have to start somewhere and have no idea what the starting point for other mathematics would be. But the word ``axioms'' looks promising. So you eagerly read along and work through some elementary exercises at the beginning of the book. You feel vaguely bothered: these don't seem like axioms at all, at least not in the sense that you want to think of axioms. Axioms imply a starting point from which everything else can be built up, according to precise rules specified in the axiom system. Even though you can understand first few proofs in an informal way, and are able to do some of the exercises, it's hard to pin down precisely what the rules are. Sure, each step seems to follow logically from the others, but exactly what does that mean? Is the ``logic'' just a matter of common sense, something vague that we all understand but can never quite state precisely? You've spent a number of years, off and on, programming computers, and you know that in the case of computer languages there is no question of what the rules are---they are precise and crystal clear. If you follow them, your program will work, and if you don't, it won't. No matter how complex a program, it can always be broken down into simpler and simpler pieces, until you can ultimately identify the bits that are moved around to perform a specific function. Some programs might require a lot of perseverance to accomplish this, but if you focus on a specific portion of it, you don't even necessarily have to know how the rest of it works. Shouldn't there be an analogy in mathematics? You decide to apply the ultimate test: you ask yourself how a computer could verify or ensure that the steps in these proofs follow from one another. Certainly mathematics must be at least as precisely defined as a computer language, if not more so; after all, computer science itself is based on it. If you can get a computer to verify these proofs, then you should also be able, in principle, to understand them yourself in a very crystal clear, precise way. You're in for a surprise: you can conceive of no way to convert the proofs, which are in English, to a form that the computer can understand. The proofs are filled with phrases such as ``assume there exists a unique $x$\ldots'' and ``given any $y$, let $z$ be the number such that\ldots'' This isn't the kind of logic you are used to in computer programming, where everything, even arithmetic, reduces to Boolean ones and zeroes if you care to break it down sufficiently. Even though you think you understand the proofs, there seems to be some kind of higher reasoning involved rather than precise rules that define how you manipulate the symbols in the axioms. Whatever it is, it just isn't obvious how you would express it to a computer, and the more you think about it, the more puzzled and confused you get, to the point where you even wonder whether {\em you} really understand it. There's a lot more to these axioms of arithmetic than meets the eye. Nobody ever talked about this in school in your applied math and engineering courses. You just learned the rules they gave you, not quite understanding how or why they worked, sometimes vaguely suspicious or uncertain of them, and through homework problems and osmosis learned how to present solutions that satisfied the instructor and earned you an ``A.'' Rarely did you actually ``prove'' anything in a rigorous way, and the math majors who did do stuff like that seemed to be in a different world. Of course, there are computer algebra programs that can do mathematics, and rather impressively. They can instantly solve the integrals that you struggled with in freshman calculus, and do much, much more. But when you look at these programs, what you see is a big collection of algorithms and techniques that evolved and were added to over time, along with some basic software that manipulates symbols. Each algorithm that is built in is the result of someone's theorem whose proof is omitted; you just have to trust the person who proved it and the person who programmed it in and hope there are no bugs.\index{computer program bugs} Somehow this doesn't seem to be the essence of mathematics. Although computer algebra systems can generate theorems with amazing speed, they can't actually prove a single one of them. After some puzzlement, you revisit some popular books on what mathematics is all about. Somewhere you read that all of mathematics is actually derived from something called ``set theory.'' This is a little confusing, because no where in the book that presented the axioms of arithmetic was there any mention of set theory, or if there was, it seemed to be just a tool that helps you describe things better---the set of even numbers, that sort of thing. If set theory is the basis for all mathematics, then why are additional axioms needed for arithmetic? Something is wrong but you're not sure what. One of your friends is a pure mathematician. He knows he is unable to communicate to you what he does for a living and seems to have little interest in trying. You do know that for him, proofs are what mathematics is all about. You ask him what a proof is, and he essentially tells you that, while of course it's based on logic, really it's something you learn by doing it over and over until you pick it up. He refers you to a book, {\em How to Read and Do Proofs} \cite{Solow}.\index{Solow, Daniel} Although this book helps you understand traditional informal proofs, there is still something missing you can't seem to pin down yet. You ask your friend how you would go about having a computer verify a proof. At first he seems puzzled by the question; why would you want to do that? Then he says it's not something that would make any sense to do, but he's heard that you'd have to break the proof down into thousands or even millions of individual steps to do such a thing, because the reasoning involved is at such a high level of abstraction. He says that maybe it's something you could do up to a point, but the computer would be completely impractical once you get into any meaningful mathematics. There, the only way you can verify a proof is by hand, and you can only acquire the ability to do this by specializing in the field for a couple of years in grad school. Anyway, he thinks it all has to do with set theory, although he has never taken a formal course in set theory but just learned what he needed as he went along. You are intrigued and amazed. Apparently a mathematician can grasp as a single concept something that would take a computer a thousand or a million steps to verify, and have complete confidence in it. Each one of these thousand or million steps must be absolutely correct, or else the whole proof is meaningless. If you added a million numbers by hand, would you trust the result? How do you really know that all these steps are correct, that there isn't some subtle pitfall in one of these million steps, like a bug in a computer program?\index{computer program bugs} After all, you've read that famous mathematicians have occasionally made mistakes, and you certainly know you've made your share on your math homework problems in school. You recall the analogy with a computer program. Sure, you can understand what a large computer program such as a word processor does, as a single high-level concept or a small set of such concepts, but your ability to understand it in no way ensures that the program is correct and doesn't have hidden bugs. Even if you wrote the program yourself you can't really know this; most large programs that you've written have had bugs that crop up at some later date, no matter how careful you tried to be while writing them. OK, so now it seems the reason you can't figure out how to make a computer verify proofs is because each step really corresponds to a million small steps. Well, you say, a computer can do a million calculations in a second, so maybe it's still practical to do. Now the puzzle becomes how to figure out what the million steps are that each English-language step corresponds to. Your mathematician friend hasn't a clue, but suggests that maybe you would find the answer by studying set theory. Actually, your friend thinks you're a little off the wall for even wondering such a thing. For him, this is not what mathematics is all about. The subject of set theory keeps popping up, so you decide it's time to look it up. You decide to start off on a careful footing, so you start reading a couple of very elementary books on set theory. A lot of it seems pretty obvious, like intersections, subsets, and Venn diagrams. You thumb through one of the books; nowhere is anything about axioms mentioned. The other book relegates to an appendix a brief discussion that mentions a set of axioms called ``Zermelo-Fraenkel set theory''\index{Zermelo-Fraenkel set theory} and states them in English. You look at them and have no idea what they really mean or what you can do with them. The comments in this appendix say that the purpose of mentioning them is to expose you to the idea, but imply that they are not necessary for basic understanding and that they are really the subject matter of advanced treatments where fine points such as a certain paradox (Russell's paradox\index{Russell's paradox}\footnote{Russell's paradox assumes that there exists a set $S$ that is a collection of all sets that don't contain themselves. Now, either $S$ contains itself or it doesn't. If it contains itself, it contradicts its definition. But if it doesn't contain itself, it also contradicts its definition. Russell's paradox is resolved in ZF set theory by denying that such a set $S$ exists.}) are resolved. Wait a minute---shouldn't the axioms be a starting point, not an ending point? If there are paradoxes that arise without the axioms, how do you know you won't stumble across one accidentally when using the informal approach? And nowhere do these books describe how ``all of mathematics can be derived from set theory'' which by now you've heard a few times. You find a more advanced book on set theory. This one actually lists the axioms of ZF set theory in plain English on page one. {\em Now} you think your quest has ended and you've finally found the source of all mathematical knowledge; you just have to understand what it means. Here, in one place, is the basis for all of mathematics! You stare at the axioms in awe, puzzle over them, memorize them, hoping that if you just meditate on them long enough they will become clear. Of course, you haven't the slightest idea how the rest of mathematics is ``derived'' from them; in particular, if these are the axioms of mathematics, then why do arithmetic, group theory, and so on need their own axioms? You start reading this advanced book carefully, pondering the meaning of every word, because by now you're really determined to get to the bottom of this. The first thing the book does is explain how the axioms came about, which was to resolve Russell's paradox.\index{Russell's paradox} In fact that seems to be the main purpose of their existence; that they supposedly can be used to derive all of mathematics seems irrelevant and is not even mentioned. Well, you go on. You hope the book will explain to you clearly, step by step, how to derive things from the axioms. After all, this is the starting point of mathematics, like a book that explains the basics of a computer programming language. But something is missing. You find you can't even understand the first proof or do the first exercise. Symbols such as $\exists$ and $\forall$ permeate the page without any mention of where they came from or how to manipulate them; the author assumes you are totally familiar with them and doesn't even tell you what they mean. By now you know that $\exists$ means ``there exists'' and $\forall$ means ``for all,'' but shouldn't the rules for manipulating these symbols be part of the axioms? You still have no idea how you could even describe the axioms to a computer. Certainly there is something much different here from the technical literature you're used to reading. A computer language manual almost always explains very clearly what all the symbols mean, precisely what they do, and the rules used for combining them, and you work your way up from there. After glancing at four or five other such books, you come to the realization that there is another whole field of study that you need just to get to the point at which you can understand the axioms of set theory. The field is called ``logic.'' In fact, some of the books did recommend it as a prerequisite, but it just didn't sink in. You assumed logic was, well, just logic, something that a person with common sense intuitively understood. Why waste your time reading boring treatises on symbolic logic, the manipulation of 1's and 0's that computers do, when you already know that? But this is a different kind of logic, quite alien to you. The subject of {\sc nand} and {\sc nor} gates is not even touched upon or in any case has to do with only a very small part of this field. So your quest continues. Skimming through the first couple of introductory books, you get a general idea of what logic is about and what quantifiers (``for all,'' ``there exists'') mean, but you find their examples somewhat trivial and mildly annoying (``all dogs are animals,'' ``some animals are dogs,'' and such). But all you want to know is what the rules are for manipulating the symbols so you can apply them to set theory. Some formulas describing the relationships among quantifiers ($\exists$ and $\forall$) are listed in tables, along with some verbal reasoning to justify them. Presumably, if you want to find out if a formula is correct, you go through this same kind of mental reasoning process, possibly using images of dogs and animals. Intuitively, the formulas seem to make sense. But when you ask yourself, ``What are the rules I need to get a computer to figure out whether this formula is correct?'', you still don't know. Certainly you don't ask the computer to imagine dogs and animals. You look at some more advanced logic books. Many of them have an introductory chapter summarizing set theory, which turns out to be a prerequisite. You need logic to understand set theory, but it seems you also need set theory to understand logic! These books jump right into proving rather advanced theorems about logic, without offering the faintest clue about where the logic came from that allows them to prove these theorems. Luckily, you come across an elementary book of logic that, halfway through, after the usual truth tables and metaphors, presents in a clear, precise way what you've been looking for all along: the axioms! They're divided into propositional calculus (also called sentential logic) and predicate calculus (also called first-order logic),\index{first-order logic} with rules so simple and crystal clear that now you can finally program a computer to understand them. Indeed, they're no harder than learning how to play a game of chess. As far as what you seem to need is concerned, the whole book could have been written in five pages! {\em Now} you think you've found the ultimate source of mathematical truth. So---the axioms of mathematics consist of these axioms of logic, together with the axioms of ZF set theory. (By now you've also been able to figure out how to translate the ZF axioms from English into the actual symbols of logic which you can now manipulate according to precise, easy-to-understand rules.) Of course, you still don't understand how ``all of mathematics can be derived from set theory,'' but maybe this will reveal itself in due course. You eagerly set out to program the axioms and rules into a computer and start to look at the theorems you will have to prove as the logic is developed. All sorts of important theorems start popping up: the deduction theorem,\index{deduction theorem} the substitution theorem,\index{substitution theorem} the completeness theorem of propositional calculus,\index{first-order logic!completeness} the completeness theorem of predicate calculus. Uh-oh, there seems to be trouble. They all get harder and harder, and not one of them can be derived with the axioms and rules of logic you've just been handed. Instead, they all require ``metalogic'' for their proofs, a kind of mixture of logic and set theory that allows you to prove things {\em about} the axioms and theorems of logic rather than {\em with} them. You plow ahead anyway. A month later, you've spent much of your free time getting the computer to verify proofs in propositional calculus. You've programmed in the axioms, but you've also had to program in the deduction theorem, the substitution theorem, and the completeness theorem of propositional calculus, which by now you've resigned yourself to treating as rather complex additional axioms, since they can't be proved from the axioms you were given. You can now get the computer to verify and even generate complete, rigorous, formal proofs\index{formal proof}. Never mind that they may have 100,000 steps---at least now you can have complete, absolute confidence in them. Unfortunately, the only theorems you have proved are pretty trivial and you can easily verify them in a few minutes with truth tables, if not by inspection. It looks like your mathematician friend was right. Getting the computer to do serious mathematics with this kind of rigor seems almost hopeless. Even worse, it seems that the further along you get, the more ``axioms'' you have to add, as each new theorem seems to involve additional ``metamathematical'' reasoning that hasn't been formalized, and none of it can be derived from the axioms of logic. Not only do the proofs keep growing exponentially as you get further along, but the program to verify them keeps getting bigger and bigger as you program in more ``metatheorems.''\index{metatheorem}\footnote{A metatheorem is usually a statement that is too general to be directly provable in a theory. For example, ``if $n_1$, $n_2$, and $n_3$ are integers, then $n_1+n_2+n_3$ is an integer'' is a theorem of number theory. But ``for any integer $k > 1$, if $n_1, \ldots, n_k$ are integers, then $n_1+\ldots +n_k$ is an integer'' is a metatheorem, in other words a family of theorems, one for every $k$. The reason it is not a theorem is that the general sum $n_1+\ldots +n_k$ (as a function of $k$) is not an operation that can be defined directly in number theory.} The bugs\index{computer program bugs} that have cropped up so far have already made you start to lose faith in the rigor you seem to have achieved, and you know it's just going to get worse as your program gets larger. \begin{center} *** \end{center} \subsection{Mathematics and the Non-Specialist} \begin{quote} {\em A real proof is not checkable by a machine, or even by any mathematician not privy to the gestalt, the mode of thought of the particular field of mathematics in which the proof is located.} \flushright\sc Davis and Hersh\index{Davis, Phillip J.} \footnote{\cite{Davis}, p.~354}\\ \end{quote} The bulk of abstract or theoretical mathematics is ordinarily outside the reach of anyone but a few specialists in each field who have completed the necessary difficult internship in order to enter its coterie. The typical intelligent layperson has no reasonable hope of understanding much of it, nor even the specialist mathematician of understanding other fields. It is like a foreign language that has no dictionary to look up the translation; the only way you can learn it is by living in the country for a few years. It is argued that the effort involved in learning a specialty is a necessary process for acquiring a deep understanding. Of course, this is almost certainly true if one is to make significant contributions to a field; in particular, ``doing'' proofs is probably the most important part of a mathematician's training. But is it also necessary to deny outsiders access to it? Is it necessary that abstract mathematics be so hard for a layperson to grasp? A computer normally is of no help whatsoever. Most published proofs are actually just series of hints written in an informal style that requires considerable knowledge of the field to understand. These are the ``real proofs'' referred to by Davis and Hersh.\index{informal proof} There is an implicit understanding that, in principle, such a proof could be converted to a complete formal proof\index{formal proof}. However, it is said that no one would ever attempt such a conversion, even if they could, because that would presumably require millions of steps (Section~\ref{dream}). Unfortunately the informal style automatically excludes the understanding of the proof by anyone who hasn't gone through the necessary apprenticeship. The best that the intelligent layperson can do is to read popular books about deep and famous results; while this can be helpful, it can also be misleading, and the lack of detail usually leaves the reader with no ability whatsoever to explore any aspect of the field being described. The statements of theorems often use sophisticated notation that makes them inaccessible to the non-specialist. For a non-specialist who wants to achieve a deeper understanding of a proof, the process of tracing definitions and lemmas back through their hierarchy\index{hierarchy} quickly becomes confusing and discouraging. Textbooks are usually written to train mathematicians or to communicate to people who are already mathematicians, and large gaps in proofs are often left as exercises to the reader who is left at an impasse if he or she becomes stuck. I believe that eventually computers will enable non-specialists and even intelligent laypersons to follow almost any mathematical proof in any field. Metamath is an attempt in that direction. If all of mathematics were as easily accessible as a computer programming language, I could envision computer programmers and hobbyists who otherwise lack mathematical sophistication exploring and being amazed by the world of theorems and proofs in obscure specialties, perhaps even coming up with results of their own. A tremendous advantage would be that anyone could experiment with conjectures in any field---the computer would offer instant feedback as to whether an inference step was correct. Mathematicians sometimes have to put up with the annoyance of cranks\index{cranks} who lack a fundamental understanding of mathematics but insist that their ``proofs'' of, say, Fermat's Last Theorem\index{Fermat's Last Theorem} be taken seriously. I think part of the problem is that these people are mislead by informal mathematical language, treating it as if they were reading ordinary expository English and failing to appreciate the implicit underlying rigor. Such cranks are rare in the field of computers, because computer languages are much more explicit, and ultimately the proof is in whether a computer program works or not. With easily accessible computer-based abstract mathematics, a mathematician could say to a crank, ``don't bother me until you've demonstrated your claim on the computer!'' % 22-May-04 nm % Attempt to move De Millo quote so it doesn't separate from attribution % CHANGE THIS NUMBER (AND ELIMINATE IF POSSIBLE) WHEN ABOVE TEXT CHANGES \vspace{-0.5em} \subsection{An Impossible Dream?}\label{dream} \begin{quote} {\em Even quite basic theorems would demand almost unbelievably vast books to display their proofs.} \flushright\sc Robert E. Edwards\footnote{\cite{Edwards}, p.~68}\\ \end{quote}\index{Edwards, Robert E.} \begin{quote} {\em Oh, of course no one ever really {\em does} it. It would take forever! You just show that you could do it, that's sufficient.} \flushright\sc ``The Ideal Mathematician'' \index{Davis, Phillip J.}\footnote{\cite{Davis}, p.~40}\\ \end{quote} \begin{quote} {\em There is a theorem in the primitive notation of set theory that corresponds to the arithmetic theorem `$1000+2000=3000$'. The formula would be forbiddingly long\ldots even if [one] knows the definitions and is asked to simplify the long formula according to them, chances are he will make errors and arrive at some incorrect result.} \flushright\sc Hao Wang\footnote{\cite{Wang}, p.~140}\\ \end{quote}\index{Wang, Hao} % 22-May-04 nm % Attempt to move De Millo quote so it doesn't separate from attribution % CHANGE THIS NUMBER (AND ELIMINATE IF POSSIBLE) WHEN ABOVE TEXT CHANGES \vspace{-0.5em} \begin{quote} {\em The {\em Principia Mathematica} was the crowning achievement of the formalists. It was also the deathblow of the formalist view.\ldots\\ {[Rus\-sell]} failed, in three enormous volumes, to get beyond the elementary facts of arithmetic. He showed what can be done in principle and what cannot be done in practice. If the mathematical process were really one of strict, logical progression, we would still be counting our fingers.\ldots\\ One theoretician estimates, for instance, that a demonstration of one of Ramanujan's conjectures assuming set theory and elementary analysis would take about two thousand pages; the length of a deduction from first principles is nearly in\-con\-ceiv\-a\-ble\ldots The probabilists argue that\ldots any very long proof can at best be viewed as only probably correct\ldots} \flushright\sc Richard de Millo et. al.\footnote{\cite{deMillo}, pp.~269, 271}\\ \end{quote}\index{de Millo, Richard} A number of writers have conveyed the impression that the kind of absolute rigor provided by Metamath\index{Metamath} is an impossible dream, suggesting that a complete, formal verification\index{formal proof} of a typical theorem would take millions of steps in untold volumes of books. Even if it could be done, the thinking sometimes goes, all meaning would be lost in such a monstrous, tedious verification.\index{informal proof}\index{proof length} These writers assume, however, that in order to achieve the kind of complete formal verification they desire one must break down a proof into individual primitive steps that make direct reference to the axioms. This is not necessary. There is no reason not to make use of previously proved theorems rather than proving them over and over. Just as important, definitions\index{definition} can be introduced along the way, allowing very complex formulas to be represented with few symbols. Not doing this can lead to absurdly long formulas. For example, G\"{o}del's incompleteness theorem\index{G\"{o}del's incompleteness theorem}, which can be expressed with a small number of defined symbols, would require about 20,000 primitive symbols to express it.\index{Boolos, George S.}\footnote{George S.\ Boolos, lecture at Massachusetts Institute of Technology, spring 1990} An extreme example is Bourbaki's\label{bourbaki} language for set theory, which requires 4,523,659,424,929 symbols plus 1,179,618,517,981 disambiguatory links (lines connecting symbol pairs, usually drawn below or above the formula) to express the number ``one'' \cite{Mathias}.\index{Mathias, Adrian R. D.}\index{Bourbaki, Nicholaus} % http://www.dpmms.cam.ac.uk/~ardm/ A hierarchy\index{hierarchy} of theorems and definitions permits an exponential growth in the formula sizes and primitive proof steps to be described with only a linear growth in the number of symbols used. Of course, this is how ordinary informal mathematics is normally done anyway, but with Metamath\index{Metamath} it can be done with absolute rigor and precision. \subsection{Beauty} \begin{quote} {\em No one shall be able to drive us from the paradise that Cantor has created for us.} \flushright\sc David Hilbert\footnote{As quoted in \cite{Moore}, p.~131}\\ \end{quote}\index{Hilbert, David} \begin{quote} {\em Mathematics possesses not only truth, but some supreme beauty ---a beauty cold and austere, like that of a sculpture.} \flushright\sc Bertrand Russell\footnote{\cite{Russell}}\\ \end{quote}\index{Russell, Bertrand} \begin{quote} {\em Euclid alone has looked on Beauty bare.} \flushright\sc Edna Millay\footnote{As quoted in \cite{Davis}, p.~150}\\ \end{quote}\index{Millay, Edna} For most people, abstract mathematics is distant, strange, and incomprehensible. Many popular books have tried to convey some of the sense of beauty in famous theorems. But even an intelligent layperson is left with only a general idea of what a theorem is about and is hardly given the tools needed to make use of it. Traditionally, it is only after years of arduous study that one can grasp the concepts needed for deep understanding. Metamath\index{Metamath} allows you to approach the proof of the theorem from a quite different perspective, peeling apart the formulas and definitions layer by layer until an entirely different kind of understanding is achieved. Every step of the proof is there, pieced together with absolute precision and instantly available for inspection through a microscope with a magnification as powerful as you desire. A proof in itself can be considered an object of beauty. Constructing an elegant proof is an art. Once a famous theorem has been proved, often considerable effort is made to find simpler and more easily understood proofs. Creating and communicating elegant proofs is a major concern of mathematicians. Metamath is one way of providing a common language for archiving and preserving this information. The length of a proof can, to a certain extent, be considered an objective measure of its ``beauty,'' since shorter proofs are usually considered more elegant. In the set theory database \texttt{set.mm} provided with Metamath, one goal was to make all proofs as short as possible. \subsection{Simplicity} \begin{quote} {\em God made man simple; man's complex problems are of his own devising.} \flushright\sc Eccles. 7:29\footnote{Jerusalem Bible}\\ \end{quote}\index{Bible} \begin{quote} {\em God made integers, all else is the work of man.} \flushright\sc Leopold Kronecker\footnote{{\em Jahresberichte der Deutschen Mathematicker Vereinigung}, bk. 2}\\ \end{quote}\index{Kronecker, Leopold} \begin{quote} {\em For what is clear and easily comprehended attracts; the complicated repels.} \flushright\sc David Hilbert\footnote{As quoted in \cite{deMillo}, p.~273}\\ \end{quote}\index{Hilbert, David} The Metamath\index{Metamath} language is simple and Spartan. Metamath treats all mathematical expressions as simple sequences of symbols, devoid of meaning. The higher-level or ``metamathematical'' notions underlying Metamath are about as simple as they could possibly be. Each individual step in a proof involves a single basic concept, the substitution of an expression for a variable, so that in principle almost anyone, whether mathematician or not, can completely understand how it was arrived at. In one of its most basic applications, Metamath\index{Metamath} can be used to develop the foundations of mathematics\index{foundations of mathematics} from the very beginning. This is done in the set theory database that is provided with the Metamath package and is the subject matter of Chapter~\ref{fol}. Any language (a metalanguage\index{metalanguage}) used to describe mathematics (an object language\index{object language}) must have a mathematical content of its own, but it is desirable to keep this content down to a bare minimum, namely that needed to make use of the inference rules specified by the axioms. With any metalanguage there is a ``chicken and egg'' problem somewhat like circular reasoning: you must assume the validity of the mathematics of the metalanguage in order to prove the validity of the mathematics of the object language. The mathematical content of Metamath itself is quite limited. Like the rules of a game of chess, the essential concepts are simple enough so that virtually anyone should be able to understand them (although that in itself will not let you play like a master). The symbols that Metamath manipulates do not in themselves have any intrinsic meaning. Your interpretation of the axioms that you supply to Metamath is what gives them meaning. Metamath is an attempt to strip down mathematical thought to its bare essence and show you exactly how the symbols are manipulated. Philosophers and logicians, with various motivations, have often thought it important to study ``weak'' fragments of logic\index{weak logic} \cite{Anderson}\index{Anderson, Alan Ross} \cite{MegillBunder}\index{Megill, Norman}\index{Bunder, Martin}, other unconventional systems of logic (such as ``modal'' logic\index{modal logic} \cite[ch.\ 27]{Boolos}\index{Boolos, George S.}), and quantum logic\index{quantum logic} in physics \cite{Pavicic}\index{Pavi{\v{c}}i{\'{c}}, M.}. Metamath\index{Metamath} provides a framework in which such systems can be expressed, with an absolute precision that makes all underlying metamathematical assumptions rigorous and crystal clear. Some schools of philosophical thought, for example intuitionism\index{intuitionism} and constructivism\index{constructivism}, demand that the notions underlying any mathematical system be as simple and concrete as possible. Metamath should meet the requirements of these philosophies. Metamath must be taught the symbols, axioms\index{axiom}, and rules\index{rule} for a specific theory, from the skeptical (such as intuitionism\index{intuitionism}\footnote{Intuitionism does not accept the law of excluded middle (``either something is true or it is not true''). See \cite[p.~xi]{Tymoczko}\index{Tymoczko, Thomas} for discussion and references on this topic. Consider the theorem, ``There exist irrational numbers $a$ and $b$ such that $a^b$ is rational.'' An intuitionist would reject the following proof: If $\sqrt{2}^{\sqrt{2}}$ is rational, we are done. Otherwise, let $a=\sqrt{2}^{\sqrt{2}}$ and $b=\sqrt{2}$. Then $a^b=2$, which is rational.}) to the bold (such as the axiom of choice in set theory\footnote{The axiom of choice\index{Axiom of Choice} asserts that given any collection of pairwise disjoint nonempty sets, there exists a set that has exactly one element in common with each set of the collection. It is used to prove many important theorems in standard mathematics. Some philosophers object to it because it asserts the existence of a set without specifying what the set contains \cite[p.~154]{Enderton}\index{Enderton, Herbert B.}. In one foundation for mathematics due to Quine\index{Quine, Willard Van Orman}, that has not been otherwise shown to be inconsistent, the axiom of choice turns out to be false \cite[p.~23]{Curry}\index{Curry, Haskell B.}. The \texttt{show trace{\char`\_}back} command of the Metamath program allows you to find out whether the axiom of choice, or any other axiom, was assumed by a proof.}\index{\texttt{show trace{\char`\_}back} command}). The simplicity of the Metamath language lets the algorithm (computer program) that verifies the validity of a Metamath proof to be straightforward and robust. You can have confidence that the theorems it verifies really can be derived from your axioms. \subsection{Rigor} \begin{quote} {\em Rigor became a goal with the Greeks\ldots But the efforts to pursue rigor to the utmost have led to an impasse in which there is no longer any agreement on what it really means. Mathematics remains alive and vital, but only on a pragmatic basis.} \flushright\sc Morris Kline\footnote{\cite{Kline}, p.~1209}\\ \end{quote}\index{Kline, Morris} Kline refers to a much deeper kind of rigor than that which we will discuss in this section. G\"{o}del's incompleteness theorem\index{G\"{o}del's incompleteness theorem} showed that it is impossible to achieve absolute rigor in standard mathematics because we can never prove that mathematics is consistent (free from contradictions).\index{consistent theory} If mathematics is consistent, we will never know it, but must rely on faith. If mathematics is inconsistent, the best we can hope for is that some clever future mathematician will discover the inconsistency. In this case, the axioms would probably be revised slightly to eliminate the inconsistency, as was done in the case of Russell's paradox,\index{Russell's paradox} but the bulk of mathematics would probably not be affected by such a discovery. Russell's paradox, for example, did not affect most of the remarkable results achieved by 19th-century and earlier mathematicians. It mainly invalidated some of Gottlob Frege's\index{Frege, Gottlob} work on the foundations of mathematics in the late 1800's; in fact Frege's work inspired Russell's discovery. Despite the paradox, Frege's work contains important concepts that have significantly influenced modern logic. Kline's {\em Mathematics, The Loss of Certainty} \cite{Klinel}\index{Kline, Morris} has an interesting discussion of this topic. What {\em can} be achieved with absolute certainty\index{certainty} is the knowledge that if we assume the axioms are consistent and true, then the results derived from them are true. Part of the beauty of mathematics is that it is the one area of human endeavor where absolute certainty can be achieved in this sense. A mathematical truth will remain such for eternity. However, our actual knowledge of whether a particular statement is a mathematical truth is only as certain as the correctness of the proof that establishes it. If the proof of a statement is questionable or vague, we can't have absolute confidence in the truth that the statement claims. Let us look at some traditional ways of expressing proofs. Except in the field of formal logic\index{formal logic}, almost all traditional proofs in mathematics are really not proofs at all, but rather proof outlines or hints as to how to go about constructing the proof. Many gaps\index{gaps in proofs} are left for the reader to fill in. There are several reasons for this. First, it is usually assumed in mathematical literature that the person reading the proof is a mathematician familiar with the specialty being described, and that the missing steps are obvious to such a reader or at least that the reader is capable of filling them in. This attitude is fine for professional mathematicians in the specialty, but unfortunately it often has the drawback of cutting off the rest of the world, including mathematicians in other specialties, from understanding the proof. We discussed one possible resolution to this on p.~\pageref{envision}. Second, it is often assumed that a complete formal proof\index{formal proof} would require countless millions of symbols (Section~\ref{dream}). This might be true if the proof were to be expressed directly in terms of the axioms of logic and set theory,\index{set theory} but it is usually not true if we allow ourselves a hierarchy\index{hierarchy} of definitions and theorems to build upon, using a notation that allows us to introduce new symbols, definitions, and theorems in a precisely specified way. Even in formal logic,\index{formal logic} formal proofs\index{formal proof} that are considered complete still contain hidden or implicit information. For example, a ``proof'' is usually defined as a sequence of wffs,\index{well-formed formula (wff)}\footnote{A {\em wff} or well-formed formula is a mathematical expression (string of symbols) constructed according to some precise rules. A formal mathematical system\index{formal system} contains (1) the rules for constructing syntactically correct wffs,\index{syntax rules} (2) a list of starting wffs called axioms,\index{axiom} and (3) one or more rules prescribing how to derive new wffs, called theorems\index{theorem}, from the axioms or previously derived theorems. An example of such a system is contained in Metamath's\index{Metamath} set theory database, which defines a formal system\index{formal system} from which all of standard mathematics can be derived. Section~\ref{startf} steps you through a complete example of a formal system, and you may want to skim it now if you are unfamiliar with the concept.} each of which is an axiom or follows from a rule applied to previous wffs in the sequence. The implicit part of the proof is the algorithm by which a sequence of symbols is verified to be a valid wff, given the definition of a wff. The algorithm in this case is rather simple, but for a computer to verify the proof,\index{automated proof verification} it must have the algorithm built into its verification program.\footnote{It is possible, of course, to specify wff construction syntax outside of the program itself with a suitable input language (the Metamath language being an example), but some proof-verification or theorem-proving programs lack the ability extend wff syntax in such a fashion.} If one deals exclusively with axioms and elementary wffs, it is straightforward to implement such an algorithm. But as more and more definitions are added to the theory in order to make the expression of wffs more compact, the algorithm becomes more and more complicated. A computer program that implements the algorithm becomes larger and harder to understand as each definition is introduced, and thus more prone to bugs.\index{computer program bugs} The larger the program, the more suspicious the mathematician may be about the validity of its algorithms. This is especially true because computer programs are inherently hard to follow to begin with, and few people enjoy verifying them manually in detail. Metamath\index{Metamath} takes a different approach. Metamath's ``knowledge'' is limited to the ability to substitute variables for expressions, subject to some simple constraints. Once the basic algorithm of Metamath is assumed to be debugged, and perhaps independently confirmed, it can be trusted once and for all. The information that Metamath needs to ``understand'' mathematics is contained entirely in the body of knowledge presented to Metamath. Any errors in reasoning can only be errors in the axioms or definitions contained in this body of knowledge. As a ``constructive'' language\index{constructive language} Metamath has no conditional branches or loops like the ones that make computer programs hard to decipher; instead, the language can only build new sequences of symbols from earlier sequences of symbols. The simplicity of the rules that underlie Metamath not only makes Metamath easy to learn but also gives Metamath a great deal of flexibility. For example, Metamath is not limited to describing standard first-order logic\index{first-order logic}; higher-order logics\index{higher-order logic} and fragments of logic\index{weak logic} can be described just as easily. Metamath gives you the freedom to define whatever wff notation you prefer; it has no built-in conception of the syntax of a wff.\index{well-formed formula (wff)} With suitable axioms and definitions, Metamath can even describe and prove things about itself.\index{Metamath!self-description} (John Harrison\index{Harrison, John} discusses the ``reflection'' principle\index{reflection principle} involved in self-descriptive systems in \cite{Harrison}.) The flexibility of Metamath requires that its proofs specify a lot of detail, much more than in an ordinary ``formal'' proof.\index{formal proof} For example, in an ordinary formal proof, a single step consists of displaying the wff that constitutes that step. In order for a computer program to verify that the step is acceptable, it first must verify that the symbol sequence being displayed is an acceptable wff.\index{automated proof verification} Most proof verifiers have at least basic wff syntax built into their programs. Metamath has no hard-wired knowledge of what constitutes a wff built into it; instead every wff must be explicitly constructed based on rules defining wffs that are present in a database. Thus a single step in an ordinary formal proof may be correspond to many steps in a Metamath proof. Despite the larger number of steps, though, this does not mean that a Metamath proof must be significantly larger than an ordinary formal proof. The reason is that since we have constructed the wff from scratch, we know what the wff is, so there is no reason to display it. We only need to refer to a sequence of statements that construct it. In a sense, the display of the wff in an ordinary formal proof is an implicit proof of its own validity as a wff; Metamath just makes the proof explicit. (Section~\ref{proof} describes Metamath's proof notation.) \section{Computers and Mathematicians} \begin{quote} {\em The computer is important, but not to mathematics.} \flushright\sc Paul Halmos\footnote{As quoted in \cite{Albers}, p.~121}\\ \end{quote}\index{Halmos, Paul} Pure mathematicians have traditionally been indifferent to computers, even to the point of disdain.\index{computers and pure mathematics} Computer science itself is sometimes considered to fall in the mundane realm of ``applied'' mathematics, perhaps essential for the real world but intellectually unexciting to those who seek the deepest truths in mathematics. Perhaps a reason for this attitude towards computers is that there is little or no computer software that meets their needs, and there may be a general feeling that such software could not even exist. On the one hand, there are the practical computer algebra systems, which can perform amazing symbolic manipulations in algebra and calculus,\index{computer algebra system} yet can't prove the simplest existence theorem, if the idea of a proof is present at all. On the other hand, there are specialized automated theorem provers that technically speaking may generate correct proofs.\index{automated theorem proving} But sometimes their specialized input notation may be cryptic and their output perceived to be long, inelegant, incomprehensible proofs. The output may be viewed with suspicion, since the program that generates it tends to be very large, and its size increases the potential for bugs\index{computer program bugs}. Such a proof may be considered trustworthy only if independently verified and ``understood'' by a human, but no one wants to waste their time on such a boring, unrewarding chore. \subsection{Trusting the Computer} \begin{quote} {\em \ldots I continue to find the quasi-empirical interpretation of computer proofs to be the more plausible.\ldots Since not everything that claims to be a computer proof can be accepted as valid, what are the mathematical criteria for acceptable computer proofs?} \flushright\sc Thomas Tymoczko\footnote{\cite{Tymoczko}, p.~245}\\ \end{quote}\index{Tymoczko, Thomas} In some cases, computers have been essential tools for proving famous theorems. But if a proof is so long and obscure that it can be verified in a practical way only with a computer, it is vaguely felt to be suspicious. For example, proving the famous four-color theorem\index{four-color theorem}\index{proof length} (``a map needs no more than four colors to prevent any two adjacent countries from having the same color'') can presently only be done with the aid of a very complex computer program which originally required 1200 hours of computer time. There has been considerable debate about whether such a proof can be trusted and whether such a proof is ``real'' mathematics \cite{Swart}\index{Swart, E. R.}.\index{trusting computers} However, under normal circumstances even a skeptical mathematician would a have a great deal of confidence in the result of multiplying two numbers on a pocket calculator, even though the precise details of what goes on are hidden from its user. Even the verification on a supercomputer that a huge number is prime is trusted, especially if there is independent verification; no one bothers to debate the philosophical significance of its ``proof,'' even though the actual proof would be so large that it would be completely impractical to ever write it down on paper. It seems that if the algorithm used by the computer is simple enough to be readily understood, then the computer can be trusted. Metamath\index{Metamath} adopts this philosophy. The simplicity of its language makes it easy to learn, and because of its simplicity one can have essentially absolute confidence that a proof is correct. All axioms, rules, and definitions are available for inspection at any time because they are defined by the user; there are no hidden or built-in rules that may be prone to subtle bugs\index{computer program bugs}. The basic algorithm at the heart of Metamath is simple and fixed, and it can be assumed to be bug-free and robust with a degree of confidence approaching certainty. (An independently written implementation of Metamath could pretty much eliminate any residual doubt on the part of a skeptic.) \subsection{Trusting the Mathematician} \begin{quote} {\em There is no Algebraist nor Mathematician so expert in his science, as to place entire confidence in any truth immediately upon his discovery of it, or regard it an any thing, but a mere probability. Every time he runs over his proofs, his confidence encreases; but still more by the approbation of his friends; and is rais'd to its utmost perfection by the universal assent and applauses of the learned world.} \flushright\sc David Hume\footnote{{\em A Treatise of Human Nature}, as quoted in \cite{deMillo}, p.~267}\\ \end{quote}\index{Hume, David} \begin{quote} {\em Stanislaw Ulam estimates that mathematicians publish 200,000 theorems every year. A number of these are subsequently contradicted or otherwise disallowed, others are thrown into doubt, and most are ignored.} \flushright\sc Richard de Millo et. al.\footnote{\cite{deMillo}, p.~269}\\ \end{quote}\index{Ulam, Stanislaw} Whether or not the computer can be trusted, humans of course will occasionally err. Only the most memorable proofs get independently verified, and of these only a handful of truly great ones achieve the status of being ``known'' mathematical truths that are used without giving a second thought to their correctness. There are many famous examples of incorrect theorems and proofs in mathematical literature.\index{errors in proofs} \begin{itemize} \item There have been thousands of purported proofs of Fermat's Last Theorem\index{Fermat's Last Theorem} (``no integer solutions exist to $x^n + y^n = z^n$ for $n > 2$''), by amateurs, cranks, and well-regarded mathematicians \cite[p.~5]{Stark}\index{Stark, Harold M}. Fermat wrote a note in his copy of Bachet's {\em Diophantus} that he found ``a truly marvelous proof of this theorem but this margin is too narrow to contain it'' \cite[p.~507]{Kramer}. A recent, much publicized proof by Yoichi Miyaoka\index{Miyaoka, Yoichi} was shown to be incorrect ({\em Science News}, April 9, 1988, p.~230). The theorem was finally proved by Andrew Wiles\index{Wiles, Andrew} ({\em Science News}, July 3, 1993, p.~5), but it initially had some gaps and took over a year after its announcement to be checked thoroughly by experts. On Oct. 25, 1994, Wiles announced that the last gap found in his proof had been filled in. \item In 1882, M. Pasch discovered that an axiom was omitted from Euclid's formulation of geometry\index{Euclidean geometry}; without it, the proofs of important theorems of Euclid are not valid. Pasch's axiom\index{Pasch's axiom} states that a line that intersects one side of a triangle must also intersect another side, provided that it does not touch any of the triangle's vertices. The omission of Pasch's axiom went unnoticed for 2000 years \cite[p.~160]{Davis}, in spite of (one presumes) the thousands of students, instructors, and mathematicians who studied Euclid. \item The first published proof of the famous Schr\"{o}der-Berstein theorem\index{Schr\"{o}der-Berstein theorem} in set theory was incorrect \cite[p.~148]{Enderton}\index{Enderton, Herbert B.}. This theorem states that if there exists a function\footnote{A {\em set}\index{set} is any collection of objects. A {\em function}\index{function} or {\em mapping}\index{mapping} is a rule that assigns to each element of one set (called the function's {\em domain}\index{domain}) an element from another set.} from set $A$ onto set $B$ and vice-versa, then sets $A$ and $B$ can be put into one-to-one correspondence. Although it sounds simple and obvious, the standard proof is quite long and complex. \item In the early 1900's, Hilbert\index{Hilbert, David} published a purported proof of the continuum hypothesis\index{continuum hypothesis}, which was eventually established as unprovable by Cohen\index{Cohen, Paul} in 1963 \cite[p.~166]{Enderton}. The continuum hypothesis states that no infinity\index{infinity} (``transfinite cardinal number'')\index{cardinal, transfinite} exists whose size (or ``cardinality''\index{cardinality}) is between the size of the set of integers and the size of the set of real numbers. This hypothesis originated with German mathematician Georg Cantor\index{Cantor, Georg} in the late 1800's, and his inability to prove it is said to have contributed to mental illness that afflicted him in his later years. \item An incorrect proof of the four-color theorem\index{four-color theorem} was published by Kempe\index{Kempe, A. B.} in 1879 \cite[p.~582]{Courant}\index{Courant, Richard}; it stood for 11 years before its flaw was discovered. This theorem states that any map can be colored using only four colors, so that no two adjacent countries have the same color. In 1976 the theorem was finally proved by the famous computer-assisted proof of Haken, Appel, and Koch \cite{Swart}\index{Appel, K.}\index{Haken, W.}\index{Koch, K.}. Or at least it seems that way. Mathematician H.~S.~M.~Coxeter\index{Coxeter, H. S. M.} has doubts \cite[p.~58]{Davis}: ``I have a feeling that is an untidy kind of use of the computers, and the more you correspond with Haken and Appel, the more shaky you seem to be.'' \item Many false ``proofs'' of the Poincar\'{e} conjecture\index{Poincar\'{e} conjecture} have been proposed over the years. This conjecture states that any object that mathematically behaves like a three-dimensional sphere is a three-dimensional sphere topologically, regardless of how it is distorted. In March 1986, mathematicians Colin Rourke\index{Rourke, Colin} and Eduardo R\^{e}go\index{R\^{e}go, Eduardo} caused a stir in the mathematical community by announcing that they had found a proof; in November of that year the proof was found to be false \cite[p. 218]{PetersonI}. The conjecture remains unproven. \end{itemize} Some other counterexamples to ``theorems'' in current mathematical literature are given on the Web page \begin{verbatim} http://www.math.hut.fi/~lounesto/counterexamples.htm \end{verbatim} One of the purposes of Metamath\index{Metamath} is to allow proofs to be expressed with absolute precision. Developing a proof in the Metamath language can be challenging, because Metamath will not permit even the tiniest mistake.\index{errors in proofs} But once the proof is created, its correctness can be trusted immediately, without having to depend on the process of peer review for confirmation. \section{The Use of Computers in Mathematics} \subsection{Computer Algebra Systems} For the most part, you will find that Metamath\index{Metamath} is not a practical tool for manipulating numbers. (Even proving that $2 + 2 = 4$, if you start with set theory, can be quite complex!) Several commercial mathematics packages are quite good at arithmetic, algebra, and calculus, and as practical tools they are invaluable.\index{computer algebra system} But they have no notion of proof, and cannot understand statements starting with ``there exists such and such...''. Software packages such as Mathematica \cite{Wolfram}\index{Mathematica} do not concern themselves with proofs but instead work directly with known results. These packages primarily emphasize heuristic rules such as the substitution of equals for equals to achieve simpler expressions or expressions in a different form. Starting with a rich collection of built-in rules and algorithms, users can add to the collection by means of a powerful programming language. However, results such as, say, the existence of a certain abstract object without displaying the actual object cannot be expressed (directly) in their languages. The idea of a proof from a small set of axioms is absent. Instead this software simply assumes that each fact or rule you add to the built-in collection of algorithms is valid. One way to view the software is as a large collection of axioms from which the software, with certain goals, attempts to derive new theorems, for example equating a complex expression with a simpler equivalent. But the terms ``theorem''\index{theorem} and ``proof,''\index{proof} for example, are not even mentioned in the index of the user's manual for Mathematica.\index{Mathematica and proofs} What is also unsatisfactory from a philosophical point of view is that there is no way to ensure the validity of the results other than by trusting the writer of each application module or tediously checking each module by hand, similar to checking a computer program for bugs.\index{computer program bugs}\footnote{Two examples illustrate why the knowledge database of computer algebra systems should sometimes be regarded with a certain caution. If you ask Mathematica (version 3.0) to \texttt{Solve[x\^{ }n + y\^{ }n == z\^{ }n , n]} it will respond with \texttt{\{\{n-\char`\>-2\}, \{n-\char`\>-1\}, \{n-\char`\>1\}, \{n-\char`\>2\}\}}. In other words, Mathematica seems to ``know'' that Fermat's Last Theorem\index{Fermat's Last Theorem} is true! (At the time this version of Mathematica was released this fact was unknown.) If you ask Maple\index{Maple} to \texttt{solve(x\^{ }2 = 2\^{ }x)} then \texttt{simplify(\{"\})}, it returns the solution set \texttt{\{2, 4\}}, apparently unaware that 0.7666647\ldots is also a solution.} While of course extremely valuable in applied mathematics, computer algebra systems tend to be of little interest to the theoretical mathematician except as aids for exploring certain specific problems. Because of possible bugs, trusting the output of a computer algebra system for use as theorems in a proof-verifier would defeat the latter's goal of rigor. On the other hand, a fact such that a certain relatively large number is prime, while easy for a computer algebra system to derive, might have a long, tedious proof that could overwhelm a proof-verifier. One approach for linking computer algebra systems to a proof-verifier while retaining the advantages of both is to add a hypothesis to each such theorem indicating its source. For example, a constant {\sc maple} could indicate the theorem came from the Maple package, and would mean ``assuming Maple is consistent, then\ldots'' This and many other topics concerning the formalization of mathematics are discussed in John Harrison's\index{Harrison, John} very interesting PhD thesis~\cite{Harrison-thesis}, available on the Web. \subsection{Automated Theorem Provers}\label{theoremprovers} A mathematical theory is ``decidable''\index{decidable theory} if a mechanical method or algorithm exists that is guaranteed to determine whether or not a particular formula is a theorem. Among the few theories that are decidable is elementary geometry,\index{Euclidean geometry} as was shown by a classic result of logician Alfred Tarski\index{Tarski, Alfred} in 1948 \cite{Tarski}.\footnote{Tarski's result actually applies to a subset of the geometry discussed in elementary textbooks. This subset includes most of what would be considered elementary geometry but it is not powerful enough to express, among other things, the notions of the circumference and area of a circle. Extending the theory in a way that includes notions such as these makes the theory undecidable, as was also shown by Tarski. Tarski's algorithm is far too inefficient to implement practically on a computer. A practical algorithm for proving a smaller subset of geometry theorems (those not involving concepts of ``order'' or ``continuity'') was discovered by Chinese mathematician Wu Wen-ts\"{u}n in 1977 \cite{Chou}\index{Chou, Shang-Ching}.}\index{Wen-ts{\"{u}}n, Wu} But most theories, including elementary arithmetic, are undecidable. This fact contributes to keeping mathematics alive and well, since mathematicians know that they will never be replaced by computers (providing one believes Roger Penrose's argument that a computer can never replace the brain \cite{Penrose}\index{Penrose, Roger}). In fact, elementary geometry is often considered a ``dead'' field for the simple reason that it is decidable. On the other hand, the undecidability of a theory does not mean that one cannot use a computer to search for proofs, providing one is willing to give up if a proof is not found after a reasonable amount of time. The field of automated theorem proving\index{automated theorem proving} specializes in pursuing such computer searches. Among the more successful results to date are those based on an algorithm known as Robinson's resolution principle \cite{Robinson}\index{Robinson's resolution principle}. Automated theorem provers can be excellent tools for those willing to learn how to use them. But they are not widely used in mainstream pure mathematics, even though they could probably be useful in many areas. There are several reasons for this. Probably most important, the main goal in pure mathematics is to arrive at results that are considered to be deep or important; proving them is essential but secondary. Usually, an automated theorem prover cannot assist in this main goal, and by the time the main goal is achieved, the mathematician may have already figured out the proof as a by-product. There is also a notational problem. Mathematicians are used to using very compact syntax where one or two symbols (heavily dependent on context) can represent very complex concepts; this is part of the hierarchy\index{hierarchy} they have built up to tackle difficult problems. A theorem prover on the other hand might require that a theorem be expressed in ``first-order logic,''\index{first-order logic} which is the logic on which most of mathematics is ultimately based but which is not ordinarily used directly because expressions can become very long. Some automated theorem provers are experimental programs, limited in their use to very specialized areas, and the goal of many is simply research into the nature of automated theorem proving itself. Finally, much research remains to be done to enable them to prove very deep theorems. One significant recent result was a computer proof by Larry Wos\index{Wos, Larry} and colleagues that every Robbins algebra\index{Robbins algebra} is a Boolean algebra\index{Boolean algebra} ({\em New York Times}, Dec. 10, 1996).\footnote{In 1933, E.~V.\ Huntington\index{Huntington, E. V.} presented the following axiom system for Boolean algebra with a unary operation $n$ and a binary operation $+$: \begin{center} $x + y = y + x$ \\ $(x + y) + z = x + (y + z)$ \\ $n(n(x) + y) + n(n(x) + n(y)) = x$ \end{center} Herbert Robbins\index{Robbins, Herbert}, a student of Huntington, conjectured that the last equation can be replaced with a simpler one: \begin{center} $n(n(x + y) + n(x + n(y))) = x$ \end{center} Robbins and Huntington could not find a proof. The problem was later studied unsucessfully by Tarski\index{Tarski, Alfred} and his students, and it remained an unsolved problem until a computer found the proof in 1996. For more information on the Robbins algebra problem see \cite{Wos}.} How does Metamath\index{Metamath} relate to automated theorem provers? A theorem prover is primary concerned with one theorem at a time (perhaps tapping into a small database of known theorems) whereas Metamath is more like a theorem archiving system, storing both the theorem and its proof in a database for access and verification. Metamath is one answer to ``what do you do with the output of a theorem prover?'' and could be viewed as the next step in the process. Automated theorem provers could be useful tools for helping develop its database, although as of this writing there are no software translation tools that do this. Note that very long, automatically generated proofs can make your database fat and ugly and cause Metamath's proof verification to take a long time to run. Unless you have a particularly good program that generates very concise proofs, it might be best to consider the use of automatically generated proofs as a quick-and-dirty approach, to be manually rewritten at some later date. If you are interested in automatic theorem provers, two well-regarded programs are Isabelle\footnote{Isabelle is available on the Internet via anonymous ftp to \texttt{ftp.cl.cam.ac.uk} in the directory \texttt{ml}. Read the instructions in the file \texttt{isabelle.txt}.}\index{Isabelle} and {\sc otter}. {\sc otter}\index{otter@{\sc otter}} is available on a disk included with the book {\em Automated Reasoning: Introduction and Applications} \cite{Wos}\index{Wos, Larry}. This program not only is able to generate relatively efficient proofs, it can even be instructed to search for shorter proofs. The effective use of {\sc otter} does require a certain amount of experience, skill, and patience. The axiom system used in the \texttt{set.mm}\index{set theory database (\texttt{set.mm})} set theory database can be expressed to {\sc otter} using a method described in \cite{Megill}.\index{Megill, Norman}\footnote{To use those axioms with {\sc otter}, they must be restated in a way that eliminates the need for ``dummy variables.''\index{dummy variable!eliminating} See the Comment on p.~\pageref{nodd}.} When successful, this method tends to generate short and clever proofs, but my experiments with it indicate that the method will find proofs within a reasonable time only for relatively easy theorems. It is still fun to experiment with. Reference \cite{Bledsoe}\index{Bledsoe, W. W.} surveys a number of approaches people have explored in the field of automated theorem proving\index{automated theorem proving}. \subsection{Proof Verifiers}\label{proofverifiers} A proof verifier is a program that doesn't generate proofs but instead verifies proofs that you give it. Many proof verifiers have limited built-in automated proof capabilities, such as figuring out simple logical inferences (while still being guided by a person who provides the overall proof). Metamath has no built-in automated proof capability other than the limited capability of its Proof Assisitant. Proof-verification languages are not used as frequently as they might be. Pure mathematicians are more concerned with producing new results, and such detail and rigor would interfere with that goal. The use of computers in pure mathematics is primarily focused on automated theorem provers (not verifiers), again with the ultimate goal of aiding the creation of new mathematics. Automated theorem provers are usually concerned with attacking one theorem at time rather than making a large, organized database easily available to the user. Metamath is one way to help close this gap. Besides Metamath, there are several other on-going projects with the goal of formalizing mathematics into computer-verifiable databases. One such project is {\sc qed},\index{qed project@{\sc qed} project} and several mathematicians are currently working to agree on the requirements for a universal language. Information on this project is available at \url{www.mcs.anl.gov/qed/}. One specific proof-verification language is Mizar,\index{Mizar} which can display its proofs in the informal language that mathematicians are accustomed to. Information on the Mizar language is available \url{http://www.mizar.org}. Other higher-level proof verification languages are {\sc lcf}\index{lcf@{\sc lcf}} and {\sc hol};\index{hol@{\sc hol}} a good overview of these and others is given in \cite{Harrison}. All of these languages are fundamentally different from Metamath in that much of the mathematical foundational knowledge is embedded in the underlying proof-verification program, rather than placed directly in the database that is being verified. For the working mathematician these languages are often more practical to use than Metamath, but they can have a steep learning curve for those without a mathematical background. For example, one usually must have a fair understanding of mathematical logic in order to follow their proofs. For the working mathematician, Mizar is an excellent tool for rigorously documenting proofs. Mizar typesets its proofs in the informal English used by mathematicians (and, while fine for them, are just as inscrutable by laypersons!). A price paid for Mizar is a relatively steep learning curve of a couple of weeks. Several mathematicians are actively formalizing different areas of mathematics using Mizar and publishing the proofs in a dedicated journal. Unfortunately the task of formalizing mathematics is still looked down upon to a certain extent since it doesn't involve the creation of new mathematics. To summarize our discussions of computers and mathematics, computer algebra systems can be viewed as theorem generators focusing on a narrow realm of mathematics (numbers and their properties), automated theorem provers as proof generators for specific theorems in a much broader realm covered by a built-in formal system such as first-order logic, proof verifiers in general as proof documentors usually restricted to first-order logic, and Metamath in particular as a proof documentor whose realm is essentially unlimited. \section{Mathematics and Metamath} \subsection{Standard Mathematics} There are a number of ways that Metamath\index{Metamath} can be used with standard mathematics. The most satisfying way philosophically is the start at the very beginning, and develop the desired mathematics from the axioms of logic and set theory.\index{set theory} This is the approach taken in the \texttt{set.mm}\index{set theory database (\texttt{set.mm})} module provided with the Metamath software. Among other things, this module builds up to the axioms of real and complex numbers\index{analysis}\index{real and complex numbers} (see Section~\ref{real}), and a standard development of analysis, for example, could start at that point, using it as a basis. Besides this philosophical advantage, there are practical advantages to having all of the tools of set theory available in the supporting infrastructure. On the other hand, you may wish to start with the standard axioms of a mathematical theory without going through the set theoretical proofs of those axioms. You will need mathematical logic to make inferences, but if you wish you can simply introduce theorems\index{theorem} of logic as ``axioms''\index{axiom} wherever you need them, with the implicit assumption that in principle they can be proved, if they are obvious to you. If you choose this approach, you will probably want to review the notation used in \texttt{set.mm}\index{set theory database (\texttt{set.mm})} so that your own notation will be consistent with it. \subsection{Other Formal Systems} \index{formal system} Unlike some programs, Metamath\index{Metamath} is not limited to any specific area of mathematics, nor committed to any particular mathematical philosophy such as classical logic versus intuitionism, nor limited, say, to expressions in first-order logic. Although the database \texttt{set.mm} included with the Metamath software package describes standard logic and set theory, Meta\-math is actually a general-purpose language for describing a wide variety of formal systems.\index{formal system} Non-standard systems such as modal logic,\index{modal logic} intuitionist logic\index{intuitionism}, higher-order logic\index{higher-order logic}, quantum logic\index{quantum logic}, and category theory\index{category theory} can all be described with the Metamath language. You define the symbols you prefer and tell Metamath the axioms and rules you want to start from, and Metamath will verify any inferences you make from those axioms and rules. A simple example of a non-standard formal system is Hofstadter's\index{Hofstadter, Douglas R.} MIU system,\index{MIU-system} whose Metamath description is presented in Appendix~\ref{MIU}. Since the days of David Hilbert,\index{Hilbert, David} mathematicians have been concerned with the fact that the metalanguage\index{metalanguage} used to describe mathematics may be stronger than the mathematics being described. Metamath\index{Metamath}'s underlying finitary\index{finitary proof}, constructive nature provides a good philosophical basis for studying even the weakest logics.\index{weak logic} Actually, the usual treatment of many non-standard formal systems\index{formal system} uses model theory\index{model theory} or proof theory\index{proof theory} to describe these systems; these theories, in turn, are based on standard set theory. In other words, a non-standard formal system is defined as a set with certain properties, and standard set theory is used to derive additional properties of this set. The standard set theory database provided with Metamath can be used for this purpose, and the development of a special axiom system for the non-standard formal system becomes unnecessary. The model- or proof-theoretic approach often allows you to prove much deeper results with less effort. %\section{Additional Remarks} \subsection{Metamath and Its Philosophy} Closely related to Metamath\index{Metamath} is a philosophy or way of looking at mathematics. This philosophy is related to the formalist philosophy\index{formalism} of Hilbert\index{Hilbert, David} and his followers \cite[pp.~1203--1208]{Kline}\index{Kline, Morris} \cite[p.~6]{Behnke}\index{Behnke, H.}. In this philosophy, mathematics is viewed as nothing more than a set of rules that manipulate symbols, together with the consequences of those rules. While the mathematics being described may be complex, the rules used to describe it (the ``metamathematics''\index{metamathematics}) should be as simple as possible. In particular, proofs should be restricted to dealing with concrete objects (the symbols we write on paper rather than the abstract concepts they represent) in a constructive manner; these are called ``finitary'' proofs\index{finitary proof} \cite[pp.~2--3]{Shoenfield}\index{Shoenfield, Joseph R.}. Whether or not you find Metamath interesting or useful will in part depend on the appeal you find in its philosophy, and this appeal will probably depend on your particular goals with respect to mathematics. For example, if you are a pure mathematician at the forefront of discovering new mathematical knowledge, you will probably find that the rigid formality of Metamath stifles your creativity. On the other hand, we would argue that once this knowledge is discovered, there are advantages to documenting it in a standard format that will make it accessible to others. Sixty years from now, your field may be dormant, and as Davis and Hersh put it, your ``writings would become less translatable than those of the Maya'' \cite[p.~37]{Davis}\index{Davis, Phillip J.}. \subsection{A History of the Approach Behind Metamath} Probably the one work that has had the most motivating influence on Metamath\index{Metamath} is Whitehead and Russell's monumental {\em Principia Mathematica} \cite{PM}\index{Whitehead, Alfred North}\index{Russell, Bertrand}\index{principia mathematica@{\em Principia Mathematica}}, whose aim was to deduce all of mathematics from a small number of primitive ideas, in a very explicit way that in principle anyone could understand and follow. While this work was tremendously influential in its time, from a modern perspective it suffers from several drawbacks. Both its notation and its underlying axioms are now considered dated and are no longer used. From our point of view, its development is not really as accessible as we would like to see; for practical reasons, proofs become more and more sketchy as its mathematics progresses, and working them out in fine detail requires a degree of mathematical skill and patience that many people don't have. There are numerous small errors, which is understandable given the tedious, technical nature of the proofs and the lack of a computer to verify the details. However, even today {\em Principia Mathematica} stands out as the work closest in spirit to Metamath. It remains a mind-boggling work, and one can't help but be amazed at seeing ``$1+1=2$'' finally appear on page 83 of Volume II (Theorem *110.643). The origin of the proof notation used by Metamath dates back to the 1950's, when the logician C.~A.~Meredith expressed his proofs in a compact notation called ``condensed detachment''\index{condensed detachment} \cite{Hindley}\index{Hindley, J. Roger} \cite{Kalman}\index{Kalman, J. A.} \cite{Meredith}\index{Meredith, C. A.} \cite{Peterson}\index{Peterson, Jeremy George}. This notation allows proofs to be communicated unambiguously by merely referencing the axiom\index{axiom}, rule\index{rule}, or theorem\index{theorem} used at each step, without explicitly indicating the substitutions\index{substitution!variable}\index{variable substitution} that have to be made to the variables in that axiom, rule, or theorem. Ordinarily, condensed detachment is more or less limited to propositional calculus\index{propositional calculus}. The concept has been extended to first-order logic\index{first-order logic} in \cite{Megill}\index{Megill, Norman}, making it is easy to write a small computer program to verify proofs of simple first-order logic theorems.\index{condensed detachment!and first-order logic} A key concept behind the notation of condensed detachment is called ``unification,''\index{unification} which is an algorithm for determining what substitutions\index{substitution!variable}\index{variable substitution} to variables have to be made to make two expressions match each other. Unification was first precisely defined by the logician J.~A.~Robinson, who used it in the development of a powerful theorem-proving technique called the ``resolution principle'' \cite{Robinson}\index{Robinson's resolution principle}. Metamath does not make use of the resolution principle, which is intended for systems of first-order logic.\index{first-order logic} Metamath's use is not restricted to first-order logic, and as we have mentioned it does not automatically discover proofs. However, unification is a key idea behind Metamath's proof notation, and Metamath makes use of a very simple version of it (Section~\ref{unify}). \subsection{Metamath and First-Order Logic} First-order logic\index{first-order logic} is the supporting structure for standard mathematics. On top of it is set theory, which contains the axioms from which virtually all of mathematics can be derived---a remarkable fact.\index{category theory}\index{cardinal, inaccessible}\label{categoryth}\footnote{An exception seems to be category theory. There are several schools of thought on whether category theory is derivable from set theory. At a minimum, it appears that an additional axiom is needed that asserts the existence of an ``inaccessible cardinal'' (a type of infinity so large that standard set theory can't prove or deny that it exists). % %%%% (I took this out that was in previous editions:) % But it is also argued that not just one but a ``proper class'' of them % is needed, and the existence of proper classes is impossible in standard % set theory. (A proper class is a collection of sets so huge that no set % can contain it as an element. Proper classes can lead to % inconsistencies such as ``Russell's paradox.'' The axioms of standard % set theory are devised so as to deny the existence of proper classes.) % For more information, see \cite[pp.~328--331]{Herrlich}\index{Herrlich, Horst} and \cite{Blass}\index{Blass, Andrea}.} One of the things that makes Metamath\index{Metamath} more practical for first-order theories is a set of axioms for first-order logic designed specifically with Metamath's approach in mind. These are included in a standard database called \texttt{set.mm}\index{set theory database (\texttt{set.mm})} which comes with the Metamath software. See Chapter~\ref{fol} for a detailed description; the axioms are shown in Section~\ref{metaaxioms}. While logically equivalent to standard axiom systems, our axiom system breaks up the standard axioms into smaller pieces such that from them, you can directly derive what in other systems can only be derived as higher-level ``metatheorems.''\index{metatheorem} In other words, it is more powerful than the standard axioms from a metalogical point of view. A rigorous justification for this system and its ``metalogical completeness''\index{metalogical completeness} is found in \cite{Megill}\index{Megill, Norman}. The system is closely related to a system developed by Monk\index{Monk, J. Donald} and Tarski\index{Tarski, Alfred} in 1965 \cite{Monks}. For example, the formula $\exists x \, x = y $ (given $y$, there exists some $x$ equal to it) is a theorem of logic,\footnote{Specifically, it is a theorem of those systems of logic that assume non-empty domains. It is not a theorem of more general systems that include the empty domain\index{empty domain}, in which nothing exists, period! Such systems are called ``free logics.''\index{free logic} For a discussion of these systems, see \cite{Leblanc}\index{Leblanc, Hugues}. Since our use for logic is as a basis for set theory, which has a non-empty domain, it is more convenient (and more traditional) to use a less general system. An interesting curiosity is that, using a free logic as a basis for Zermelo-Fraenkel set theory\index{Zermelo-Fraenkel set theory} (with the redundant Axiom of the Null Set omitted),\index{Axiom of the Null Set} we cannot even prove the existence of a single set without assuming the axiom of infinity!\index{Axiom of Infinity}} whether or not $x$ and $y$ are distinct variables\index{distinct variables}. In many systems of logic, we would have to prove two theorems to arrive at this result. First we would prove ``$\exists x \, x = x $,'' then we would separately prove ``$\exists x \, x = y $, where $x$ and $y$ are distinct variables.'' We would then combine these two special cases ``outside of the system'' (i.e.\ in our heads) to be able to claim, ``$\exists x \, x = y $, regardless of whether $x$ and $y$ are distinct.'' In other words, in the combination of the two special cases is a metatheorem. In the system of logic used in Metamath's set theory\index{set theory database (\texttt{set.mm})} database, the axioms of logic are broken down into small pieces that allow them to reassembled in such a way that theorems such as these can be proved directly. Breaking down the axioms in this way makes them look peculiar and not very intuitive at first, but rest assured that they are correct and complete. Their correctness is ensured because they are theorem schemes of standard first-order logic (which you can easily verify if you are a logician). Their completeness follows from the fact that we explicitly derive the standard axioms of first-order logic as theorems. Deriving the standard axioms is somewhat tricky, but once we're there, we have at our disposal a system that is less awkward to work with in formal proofs\index{formal proof}. In technical terms that logicians understand, we eliminate the cumbersome concepts of ``free variable,''\index{free variable} ``bound variable,''\index{bound variable} and ``proper substitution''\index{proper substitution}\index{substitution!proper} as primitive notions. These concepts are present in our system but are defined in terms of concepts expressed by the axioms and can be eliminated in principle. In standard systems, these concepts are really like additional, implicit axioms\index{implicit axiom} that are somewhat complex and cannot be eliminated. The traditional approach to logic, wherein free variables and proper substitution is defined, is also possible to do directly in the Metamath language. However the notation tends to become awkward and there are disadvantages; for example, extending the definition of wffs becomes more complex when definitions are added because the free variable and proper substitution concepts have to have their definitions extended for each new wff introduced by a definition. Our choice of axioms for \texttt{set.mm} is to a certain extent a matter of style, in an attempt to achieve overall simplicity, but you should also be aware that the traditional approach is possible as well if you should choose it. \chapter{Using the Metamath Program} \label{using} \section{Installation} The way that you install Metamath\index{Metamath!installation} on your computer system is different for different computers. A separate set of installation instructions for your specific computer is provided with the Metamath software. In general, the installation is simple. There is one file containing the Metamath program itself. This file is usually called \texttt{metamath} or \texttt{metamath.}{\em xxx} where {\em xxx} is the convention (such as \texttt{exe}) for an executable program on your operating system. There are several additional files containing samples of the Metamath language, all ending with \texttt{.mm}. The file \texttt{set.mm}\index{set theory database (\texttt{set.mm})} contains logic and set theory and can be used as a starting point for other areas of mathematics. You will also need a text editor\index{text editor} capable of editing plain {\sc ascii}\footnote{American Standard for Coded Information Interchange} text in order to prepare your input files.\index{ascii@{\sc ascii}} Most computers have this capability built in. Note that plain text is not necessarily the default for some word processing programs\index{word processor}, especially if they can handle different fonts; for example, with Microsoft Word\index{Word (Microsoft)}, you must save the file in the format ``Text Only With Line Breaks'' to get a plain