\contentsline {section}{Preface}{ix}{chapter*.2}
\contentsline {subsubsection}{Overview}{ix}{section*.3}
\contentsline {subsubsection}{Setting Your Expectations}{xi}{section*.4}
\contentsline {subsubsection}{Metamath and Mathematical Literature}{xii}{section*.5}
\contentsline {subsubsection}{Formalism}{xiii}{section*.6}
\contentsline {subsubsection}{A Personal Note}{xiii}{section*.7}
\contentsline {subsubsection}{Note on Bibliography and Index}{xiii}{section*.8}
\contentsline {subsubsection}{Acknowledgments}{xiv}{section*.9}
\contentsline {subsubsection}{Note Added June 22, 2005}{xiv}{section*.10}
\contentsline {subsubsection}{Note Added June 24, 2006}{xv}{section*.11}
\contentsline {subsubsection}{Note Added March 10, 2007}{xv}{section*.12}
\contentsline {chapter}{\numberline {1}Introduction}{1}{chapter.1}
\contentsline {section}{\numberline {1.1}Mathematics as a Computer Language}{4}{section.1.1}
\contentsline {subsection}{\numberline {1.1.1}Is Mathematics ``User-Friendly''?}{4}{subsection.1.1.1}
\contentsline {subsubsection}{A Non-Mathematician's Quest for Truth}{5}{section*.13}
\contentsline {subsection}{\numberline {1.1.2}Mathematics and the Non-Specialist}{12}{subsection.1.1.2}
\contentsline {subsection}{\numberline {1.1.3}An Impossible Dream?}{14}{subsection.1.1.3}
\contentsline {subsection}{\numberline {1.1.4}Beauty}{15}{subsection.1.1.4}
\contentsline {subsection}{\numberline {1.1.5}Simplicity}{16}{subsection.1.1.5}
\contentsline {subsection}{\numberline {1.1.6}Rigor}{18}{subsection.1.1.6}
\contentsline {section}{\numberline {1.2}Computers and Mathematicians}{20}{section.1.2}
\contentsline {subsection}{\numberline {1.2.1}Trusting the Computer}{21}{subsection.1.2.1}
\contentsline {subsection}{\numberline {1.2.2}Trusting the Mathematician}{22}{subsection.1.2.2}
\contentsline {section}{\numberline {1.3}The Use of Computers in Mathematics}{24}{section.1.3}
\contentsline {subsection}{\numberline {1.3.1}Computer Algebra Systems}{24}{subsection.1.3.1}
\contentsline {subsection}{\numberline {1.3.2}Automated Theorem Provers}{25}{subsection.1.3.2}
\contentsline {subsection}{\numberline {1.3.3}Proof Verifiers}{27}{subsection.1.3.3}
\contentsline {section}{\numberline {1.4}Mathematics and Metamath}{29}{section.1.4}
\contentsline {subsection}{\numberline {1.4.1}Standard Mathematics}{29}{subsection.1.4.1}
\contentsline {subsection}{\numberline {1.4.2}Other Formal Systems}{29}{subsection.1.4.2}
\contentsline {subsection}{\numberline {1.4.3}Metamath and Its Philosophy}{30}{subsection.1.4.3}
\contentsline {subsection}{\numberline {1.4.4}A History of the Approach Behind Metamath}{30}{subsection.1.4.4}
\contentsline {subsection}{\numberline {1.4.5}Metamath and First-Order Logic}{31}{subsection.1.4.5}
\contentsline {chapter}{\numberline {2}Using the Metamath Program}{33}{chapter.2}
\contentsline {section}{\numberline {2.1}Installation}{33}{section.2.1}
\contentsline {section}{\numberline {2.2}Your First Formal System}{34}{section.2.2}
\contentsline {subsection}{\numberline {2.2.1}From Nothing to Zero}{34}{subsection.2.2.1}
\contentsline {subsection}{\numberline {2.2.2}Converting It to Metamath}{36}{subsection.2.2.2}
\contentsline {section}{\numberline {2.3}A Trial Run}{40}{section.2.3}
\contentsline {subsection}{\numberline {2.3.1}Some Hints for Using the Command Line Interface}{45}{subsection.2.3.1}
\contentsline {section}{\numberline {2.4}Your First Proof}{46}{section.2.4}
\contentsline {section}{\numberline {2.5}A Note About Editing a Data\discretionary {-}{}{}base File}{53}{section.2.5}
\contentsline {chapter}{\numberline {3}Abstract Mathematics Revealed}{55}{chapter.3}
\contentsline {section}{\numberline {3.1}Logic and Set Theory}{55}{section.3.1}
\contentsline {section}{\numberline {3.2}The Axioms for All of Mathematics}{58}{section.3.2}
\contentsline {subsection}{\numberline {3.2.1}Propositional Calculus}{58}{subsection.3.2.1}
\contentsline {subsection}{\numberline {3.2.2}Predicate Calculus}{59}{subsection.3.2.2}
\contentsline {subsection}{\numberline {3.2.3}Equality}{61}{subsection.3.2.3}
\contentsline {subsection}{\numberline {3.2.4}Set Theory}{61}{subsection.3.2.4}
\contentsline {section}{\numberline {3.3}The Axioms in the Metamath Language}{63}{section.3.3}
\contentsline {subsection}{\numberline {3.3.1}Propositional Calculus}{64}{subsection.3.3.1}
\contentsline {subsection}{\numberline {3.3.2}Pure Predicate Calculus}{64}{subsection.3.3.2}
\contentsline {subsection}{\numberline {3.3.3}Equality and Substitution}{64}{subsection.3.3.3}
\contentsline {subsection}{\numberline {3.3.4}Set Theory}{65}{subsection.3.3.4}
\contentsline {subsection}{\numberline {3.3.5}That's It}{66}{subsection.3.3.5}
\contentsline {section}{\numberline {3.4}A Hierarchy of Definitions}{66}{section.3.4}
\contentsline {subsection}{\numberline {3.4.1}Definitions for Propositional Calculus}{68}{subsection.3.4.1}
\contentsline {subsection}{\numberline {3.4.2}Definitions for Predicate Calculus}{69}{subsection.3.4.2}
\contentsline {subsection}{\numberline {3.4.3}Definitions for Set Theory}{70}{subsection.3.4.3}
\contentsline {section}{\numberline {3.5}Tricks of the Trade}{76}{section.3.5}
\contentsline {section}{\numberline {3.6}A Theorem Sampler}{78}{section.3.6}
\contentsline {section}{\numberline {3.7}Axioms for Real and Complex Numbers}{80}{section.3.7}
\contentsline {subsubsection}{Complex Number Axioms in Analysis Texts}{82}{section*.14}
\contentsline {section}{\numberline {3.8}Exploring the Set Theory Database}{83}{section.3.8}
\contentsline {subsection}{\numberline {3.8.1}A Note on ``Compact'' Proof Format}{89}{subsection.3.8.1}
\contentsline {chapter}{\numberline {4}The Metamath Language}{91}{chapter.4}
\contentsline {section}{\numberline {4.1}Specification of the Metamath Language}{92}{section.4.1}
\contentsline {subsection}{\numberline {4.1.1}Preliminaries}{92}{subsection.4.1.1}
\contentsline {subsection}{\numberline {4.1.2}Preprocessing}{93}{subsection.4.1.2}
\contentsline {subsection}{\numberline {4.1.3}Basic Syntax}{93}{subsection.4.1.3}
\contentsline {subsection}{\numberline {4.1.4}Proof Verification}{95}{subsection.4.1.4}
\contentsline {subsubsection}{Verifying Disjoint Variable Restrictions}{95}{section*.15}
\contentsline {section}{\numberline {4.2}The Basic Keywords}{96}{section.4.2}
\contentsline {subsection}{\numberline {4.2.1}User-Defined Tokens}{97}{subsection.4.2.1}
\contentsline {subsubsection}{Math Symbol Tokens}{97}{section*.16}
\contentsline {subsubsection}{Label Tokens}{98}{section*.17}
\contentsline {subsection}{\numberline {4.2.2}Constants and Variables}{99}{subsection.4.2.2}
\contentsline {subsection}{\numberline {4.2.3}The \texttt {\$c} and \texttt {\$v} Declaration Statements}{99}{subsection.4.2.3}
\contentsline {subsection}{\numberline {4.2.4}The \texttt {\$d} Statement}{100}{subsection.4.2.4}
\contentsline {subsubsection}{Compound \texttt {\$d} Statements}{102}{section*.18}
\contentsline {subsection}{\numberline {4.2.5}The \texttt {\$f} and \texttt {\$e} Statements}{105}{subsection.4.2.5}
\contentsline {subsection}{\numberline {4.2.6}Assertions (\texttt {\$a} and \texttt {\$p} Statements)}{106}{subsection.4.2.6}
\contentsline {subsubsection}{The \texttt {\$a} Statement}{107}{section*.19}
\contentsline {subsection}{\numberline {4.2.7}Frames}{108}{subsection.4.2.7}
\contentsline {subsection}{\numberline {4.2.8}Scoping Statements (\texttt {\$\{} and \texttt {\$\}})}{112}{subsection.4.2.8}
\contentsline {subsubsection}{Redeclaration of Math Symbols}{113}{section*.20}
\contentsline {subsubsection}{Frames Revisited}{114}{section*.21}
\contentsline {section}{\numberline {4.3}The Anatomy of a Proof}{114}{section.4.3}
\contentsline {subsection}{\numberline {4.3.1}The Concept of Unification}{118}{subsection.4.3.1}
\contentsline {section}{\numberline {4.4}Extensions to the Metamath Language}{119}{section.4.4}
\contentsline {subsection}{\numberline {4.4.1}Comments in the Metamath Language}{119}{subsection.4.4.1}
\contentsline {subsubsection}{Math Symbols and Labels Inside Comments}{119}{section*.22}
\contentsline {subsubsection}{Math Symbols In Comments}{120}{section*.23}
\contentsline {subsubsection}{Label References in Comments}{121}{section*.24}
\contentsline {subsection}{\numberline {4.4.2}Comment Markup Notation for HTML}{121}{subsection.4.4.2}
\contentsline {subsection}{\numberline {4.4.3}Including Other Files in a Metamath Source File}{122}{subsection.4.4.3}
\contentsline {subsection}{\numberline {4.4.4}Compressed Proof Format}{123}{subsection.4.4.4}
\contentsline {subsection}{\numberline {4.4.5}Specifying Unknown Proofs or Subproofs}{124}{subsection.4.4.5}
\contentsline {section}{\numberline {4.5}Appendix: Axioms vs.\ Definitions}{125}{section.4.5}
\contentsline {chapter}{\numberline {5}The Metamath Program}{129}{chapter.5}
\contentsline {section}{\numberline {5.1}Invoking Metamath}{129}{section.5.1}
\contentsline {section}{\numberline {5.2}Controlling Metamath}{130}{section.5.2}
\contentsline {subsection}{\numberline {5.2.1}\texttt {exit} Command}{131}{subsection.5.2.1}
\contentsline {subsection}{\numberline {5.2.2}\texttt {open log} Command}{131}{subsection.5.2.2}
\contentsline {subsection}{\numberline {5.2.3}\texttt {close log} Command}{132}{subsection.5.2.3}
\contentsline {subsection}{\numberline {5.2.4}\texttt {submit} Command}{132}{subsection.5.2.4}
\contentsline {subsection}{\numberline {5.2.5}\texttt {erase} Command}{132}{subsection.5.2.5}
\contentsline {subsection}{\numberline {5.2.6}\texttt {set echo} Command}{132}{subsection.5.2.6}
\contentsline {subsection}{\numberline {5.2.7}\texttt {set scroll} Command}{132}{subsection.5.2.7}
\contentsline {subsection}{\numberline {5.2.8}\texttt {set width} Command}{132}{subsection.5.2.8}
\contentsline {subsection}{\numberline {5.2.9}\texttt {set height} Command}{133}{subsection.5.2.9}
\contentsline {subsection}{\numberline {5.2.10}\texttt {beep} Command}{133}{subsection.5.2.10}
\contentsline {subsection}{\numberline {5.2.11}\texttt {more} Command}{133}{subsection.5.2.11}
\contentsline {subsection}{\numberline {5.2.12}Operating System Commands}{133}{subsection.5.2.12}
\contentsline {subsection}{\numberline {5.2.13}Size Limitations in Metamath}{134}{subsection.5.2.13}
\contentsline {section}{\numberline {5.3}Reading and Writing Files}{134}{section.5.3}
\contentsline {subsection}{\numberline {5.3.1}\texttt {read} Command}{134}{subsection.5.3.1}
\contentsline {subsection}{\numberline {5.3.2}\texttt {write source} Command}{134}{subsection.5.3.2}
\contentsline {section}{\numberline {5.4}Showing Status and Statements}{135}{section.5.4}
\contentsline {subsection}{\numberline {5.4.1}\texttt {show settings} Command}{135}{subsection.5.4.1}
\contentsline {subsection}{\numberline {5.4.2}\texttt {show memory} Command}{135}{subsection.5.4.2}
\contentsline {subsection}{\numberline {5.4.3}\texttt {show labels} Command}{135}{subsection.5.4.3}
\contentsline {subsection}{\numberline {5.4.4}\texttt {show statement} Command}{135}{subsection.5.4.4}
\contentsline {subsection}{\numberline {5.4.5}\texttt {search} Command}{136}{subsection.5.4.5}
\contentsline {section}{\numberline {5.5}Displaying and Verifying Proofs}{136}{section.5.5}
\contentsline {subsection}{\numberline {5.5.1}\texttt {show proof} Command}{136}{subsection.5.5.1}
\contentsline {subsection}{\numberline {5.5.2}\texttt {show usage} Command}{137}{subsection.5.5.2}
\contentsline {subsection}{\numberline {5.5.3}\texttt {show trace\_back} Command}{138}{subsection.5.5.3}
\contentsline {subsection}{\numberline {5.5.4}\texttt {verify proof} Command}{138}{subsection.5.5.4}
\contentsline {subsection}{\numberline {5.5.5}\texttt {save proof} Command}{138}{subsection.5.5.5}
\contentsline {section}{\numberline {5.6}Creating Proofs}{139}{section.5.6}
\contentsline {subsection}{\numberline {5.6.1}\texttt {prove} Command}{141}{subsection.5.6.1}
\contentsline {subsection}{\numberline {5.6.2}\texttt {set unification\_timeout} Command}{141}{subsection.5.6.2}
\contentsline {subsection}{\numberline {5.6.3}\texttt {set empty\_substitution} Command}{142}{subsection.5.6.3}
\contentsline {subsection}{\numberline {5.6.4}\texttt {set search\_limit} Command}{142}{subsection.5.6.4}
\contentsline {subsection}{\numberline {5.6.5}\texttt {show new\_proof} Command}{142}{subsection.5.6.5}
\contentsline {subsection}{\numberline {5.6.6}\texttt {assign} Command}{143}{subsection.5.6.6}
\contentsline {subsection}{\numberline {5.6.7}\texttt {match} Command}{143}{subsection.5.6.7}
\contentsline {subsection}{\numberline {5.6.8}\texttt {let} Command}{143}{subsection.5.6.8}
\contentsline {subsection}{\numberline {5.6.9}\texttt {unify} Command}{144}{subsection.5.6.9}
\contentsline {subsection}{\numberline {5.6.10}\texttt {initialize} Command}{145}{subsection.5.6.10}
\contentsline {subsection}{\numberline {5.6.11}\texttt {delete} Command}{145}{subsection.5.6.11}
\contentsline {subsection}{\numberline {5.6.12}\texttt {improve} Command}{145}{subsection.5.6.12}
\contentsline {subsection}{\numberline {5.6.13}\texttt {save new\_proof} Command}{146}{subsection.5.6.13}
\contentsline {section}{\numberline {5.7}Creating \LaTeX \ Output}{147}{section.5.7}
\contentsline {subsection}{\numberline {5.7.1}\texttt {open tex} Command}{147}{subsection.5.7.1}
\contentsline {subsection}{\numberline {5.7.2}\texttt {close tex} Command}{147}{subsection.5.7.2}
\contentsline {section}{\numberline {5.8}Creating HTML Output}{148}{section.5.8}
\contentsline {subsection}{\numberline {5.8.1}The Typesetting Comment (\texttt {\$t})}{148}{subsection.5.8.1}
\contentsline {subsection}{\numberline {5.8.2}\texttt {write theorem\_list} Command}{150}{subsection.5.8.2}
\contentsline {subsection}{\numberline {5.8.3}\texttt {write bibliography} Command}{151}{subsection.5.8.3}
\contentsline {subsection}{\numberline {5.8.4}\texttt {write recent\_additions} Command}{151}{subsection.5.8.4}
\contentsline {section}{\numberline {5.9}Text File Utilities}{151}{section.5.9}
\contentsline {subsection}{\numberline {5.9.1}\texttt {tools} Command}{151}{subsection.5.9.1}
\contentsline {subsection}{\numberline {5.9.2}\texttt {help} Command (in \texttt {tools})}{152}{subsection.5.9.2}
\contentsline {subsection}{\numberline {5.9.3}Using \texttt {tools} to Build Metamath \texttt {submit} Scripts}{152}{subsection.5.9.3}
\contentsline {subsection}{\numberline {5.9.4}Example of a \texttt {tools} Session}{153}{subsection.5.9.4}
\contentsline {chapter}{\numberline {A}Math Symbol Tokens for Set Theory}{155}{appendix.A}
\contentsline {chapter}{\numberline {B}Compressed Proofs}{159}{appendix.B}
\contentsline {chapter}{\numberline {C}Metamath's Formal System}{161}{appendix.C}
\contentsline {section}{\numberline {C.1}Introduction}{161}{section.C.1}
\contentsline {section}{\numberline {C.2}The Formal Description}{162}{section.C.2}
\contentsline {subsection}{\numberline {C.2.1}Preliminaries}{162}{Hfootnote.86}
\contentsline {subsection}{\numberline {C.2.2}Constants, Variables, and Expressions}{162}{subsection.C.2.2}
\contentsline {subsection}{\numberline {C.2.3}Substitution}{163}{subsection.C.2.3}
\contentsline {subsection}{\numberline {C.2.4}Statements}{163}{subsection.C.2.4}
\contentsline {subsection}{\numberline {C.2.5}Formal Systems}{165}{subsection.C.2.5}
\contentsline {section}{\numberline {C.3}Examples of Formal Systems}{166}{section.C.3}
\contentsline {subsection}{\numberline {C.3.1}Example\nobreakspace {}1---Propositional Calculus}{166}{subsection.C.3.1}
\contentsline {subsection}{\numberline {C.3.2}Example\nobreakspace {}2---Predicate Calculus with Equality}{168}{subsection.C.3.2}
\contentsline {subsection}{\numberline {C.3.3}Free Variables and Proper Substitution}{170}{subsection.C.3.3}
\contentsline {subsection}{\numberline {C.3.4}Metalogical Completeness}{170}{subsection.C.3.4}
\contentsline {subsection}{\numberline {C.3.5}Example\nobreakspace {}3---Metalogically Complete Predicate Calculus with Equality}{171}{subsection.C.3.5}
\contentsline {subsection}{\numberline {C.3.6}Example\nobreakspace {}4---Adding Definitions}{172}{subsection.C.3.6}
\contentsline {subsection}{\numberline {C.3.7}Example\nobreakspace {}5---ZFC Set Theory}{173}{subsection.C.3.7}
\contentsline {subsection}{\numberline {C.3.8}Example\nobreakspace {}6---Class Notation in Set Theory}{174}{subsection.C.3.8}
\contentsline {section}{\numberline {C.4}Metamath as a Formal System}{175}{section.C.4}
\contentsline {chapter}{\numberline {D}The MIU System}{177}{appendix.D}
\contentsline {chapter}{Bibliography}{181}{section*.25}
\contentsline {chapter}{Index}{187}{section*.27}