\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}{xii}{section*.6}
\contentsline {subsubsection}{A Personal Note}{xiii}{section*.7}
\contentsline {subsubsection}{Note on Bibliography and Index}{xiii}{section*.8}
\contentsline {subsubsection}{Acknowledgments}{xiii}{section*.9}
\contentsline {subsubsection}{Note Added January 6, 2002}{xiii}{section*.10}
\contentsline {subsubsection}{Note Added May 20, 2003}{xiv}{section*.11}
\contentsline {subsubsection}{Note Added November 20, 2003}{xv}{section*.12}
\contentsline {subsubsection}{Note Added April 2, 2004}{xv}{section*.13}
\contentsline {subsubsection}{Note Added May 22, 2004}{xv}{section*.14}
\contentsline {subsubsection}{Note Added September 14, 2004}{xv}{section*.15}
\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}{4}{section*.16}
\contentsline {subsection}{\numberline {1.1.2}Mathematics and the Non-Specialist}{11}{subsection.1.1.2}
\contentsline {subsection}{\numberline {1.1.3}An Impossible Dream?}{13}{subsection.1.1.3}
\contentsline {subsection}{\numberline {1.1.4}Beauty}{14}{subsection.1.1.4}
\contentsline {subsection}{\numberline {1.1.5}Simplicity}{15}{subsection.1.1.5}
\contentsline {subsection}{\numberline {1.1.6}Rigor}{17}{subsection.1.1.6}
\contentsline {section}{\numberline {1.2}Computers and Mathematicians}{19}{section.1.2}
\contentsline {subsection}{\numberline {1.2.1}Trusting the Computer}{20}{subsection.1.2.1}
\contentsline {subsection}{\numberline {1.2.2}Trusting the Mathematician}{21}{subsection.1.2.2}
\contentsline {section}{\numberline {1.3}The Use of Computers in Mathematics}{23}{section.1.3}
\contentsline {subsection}{\numberline {1.3.1}Computer Algebra Systems}{23}{subsection.1.3.1}
\contentsline {subsection}{\numberline {1.3.2}Automated Theorem Provers}{24}{subsection.1.3.2}
\contentsline {subsection}{\numberline {1.3.3}Proof Verifiers}{26}{subsection.1.3.3}
\contentsline {section}{\numberline {1.4}Mathematics and Metamath}{27}{section.1.4}
\contentsline {subsection}{\numberline {1.4.1}Standard Mathematics}{27}{subsection.1.4.1}
\contentsline {subsection}{\numberline {1.4.2}Other Formal Systems}{27}{subsection.1.4.2}
\contentsline {subsection}{\numberline {1.4.3}Metamath and Its Philosophy}{28}{subsection.1.4.3}
\contentsline {subsection}{\numberline {1.4.4}A History of the Approach Behind Metamath}{28}{subsection.1.4.4}
\contentsline {subsection}{\numberline {1.4.5}Metamath and First-Order Logic}{29}{subsection.1.4.5}
\contentsline {chapter}{\numberline {2}Using the Metamath Program}{31}{chapter.2}
\contentsline {section}{\numberline {2.1}Installation}{31}{section.2.1}
\contentsline {section}{\numberline {2.2}Your First Formal System}{32}{section.2.2}
\contentsline {subsection}{\numberline {2.2.1}From Nothing to Zero}{32}{subsection.2.2.1}
\contentsline {subsection}{\numberline {2.2.2}Converting It to Metamath}{34}{subsection.2.2.2}
\contentsline {section}{\numberline {2.3}A Trial Run}{38}{section.2.3}
\contentsline {subsection}{\numberline {2.3.1}Some Hints for Using the Command Line Interface}{43}{subsection.2.3.1}
\contentsline {section}{\numberline {2.4}Your First Proof}{44}{section.2.4}
\contentsline {section}{\numberline {2.5}A Note About Editing a Data\discretionary {-}{}{}base File}{49}{section.2.5}
\contentsline {chapter}{\numberline {3}Abstract Mathematics Revealed}{51}{chapter.3}
\contentsline {section}{\numberline {3.1}Logic and Set Theory}{51}{section.3.1}
\contentsline {section}{\numberline {3.2}The Axioms for All of Mathematics}{53}{section.3.2}
\contentsline {subsection}{\numberline {3.2.1}Propositional Calculus}{54}{subsection.3.2.1}
\contentsline {subsection}{\numberline {3.2.2}Predicate Calculus}{55}{subsection.3.2.2}
\contentsline {subsection}{\numberline {3.2.3}Equality}{56}{subsection.3.2.3}
\contentsline {subsection}{\numberline {3.2.4}Set Theory}{57}{subsection.3.2.4}
\contentsline {section}{\numberline {3.3}The Axioms in the Metamath Language}{58}{section.3.3}
\contentsline {subsection}{\numberline {3.3.1}Propositional Calculus}{59}{subsection.3.3.1}
\contentsline {subsection}{\numberline {3.3.2}Pure Predicate Calculus}{59}{subsection.3.3.2}
\contentsline {subsection}{\numberline {3.3.3}Equality and Substitution}{60}{subsection.3.3.3}
\contentsline {subsection}{\numberline {3.3.4}Set Theory}{60}{subsection.3.3.4}
\contentsline {subsection}{\numberline {3.3.5}That's It}{61}{subsection.3.3.5}
\contentsline {section}{\numberline {3.4}A Hierarchy of Definitions}{61}{section.3.4}
\contentsline {subsection}{\numberline {3.4.1}Definitions for Propositional Calculus}{63}{subsection.3.4.1}
\contentsline {subsection}{\numberline {3.4.2}Definitions for Predicate Calculus}{64}{subsection.3.4.2}
\contentsline {subsection}{\numberline {3.4.3}Definitions for Set Theory}{65}{subsection.3.4.3}
\contentsline {section}{\numberline {3.5}Tricks of the Trade}{71}{section.3.5}
\contentsline {section}{\numberline {3.6}A Theorem Sampler}{72}{section.3.6}
\contentsline {section}{\numberline {3.7}Axioms for Real and Complex Numbers}{75}{section.3.7}
\contentsline {subsubsection}{Complex Number Axioms in Analysis Texts}{77}{section*.17}
\contentsline {section}{\numberline {3.8}Exploring the Set Theory Database}{77}{section.3.8}
\contentsline {subsection}{\numberline {3.8.1}A Note on ``Compact'' Proof Format}{84}{subsection.3.8.1}
\contentsline {chapter}{\numberline {4}The Metamath Language}{87}{chapter.4}
\contentsline {section}{\numberline {4.1}Specification of the Metamath Language}{88}{section.4.1}
\contentsline {subsection}{\numberline {4.1.1}Preliminaries}{88}{subsection.4.1.1}
\contentsline {subsection}{\numberline {4.1.2}Preprocessing}{89}{subsection.4.1.2}
\contentsline {subsection}{\numberline {4.1.3}Basic Syntax}{89}{subsection.4.1.3}
\contentsline {subsection}{\numberline {4.1.4}Proof Verification}{90}{subsection.4.1.4}
\contentsline {subsubsection}{Verifying Disjoint Variable Restrictions}{91}{section*.18}
\contentsline {section}{\numberline {4.2}The Basic Keywords}{91}{section.4.2}
\contentsline {subsection}{\numberline {4.2.1}User-Defined Tokens}{93}{subsection.4.2.1}
\contentsline {subsubsection}{Math Symbol Tokens}{93}{section*.19}
\contentsline {subsubsection}{Label Tokens}{94}{section*.20}
\contentsline {subsection}{\numberline {4.2.2}Constants and Variables}{94}{subsection.4.2.2}
\contentsline {subsection}{\numberline {4.2.3}The \texttt {\$c} and \texttt {\$v} Declaration Statements}{95}{subsection.4.2.3}
\contentsline {subsection}{\numberline {4.2.4}The \texttt {\$d} Statement}{95}{subsection.4.2.4}
\contentsline {subsubsection}{Compound \texttt {\$d} Statements}{97}{section*.21}
\contentsline {subsection}{\numberline {4.2.5}The \texttt {\$f} and \texttt {\$e} Statements}{100}{subsection.4.2.5}
\contentsline {subsection}{\numberline {4.2.6}Assertions (\texttt {\$a} and \texttt {\$p} Statements)}{102}{subsection.4.2.6}
\contentsline {subsubsection}{The \texttt {\$a} Statement}{102}{section*.22}
\contentsline {subsection}{\numberline {4.2.7}Frames}{103}{subsection.4.2.7}
\contentsline {subsection}{\numberline {4.2.8}Scoping Statements (\texttt {\$\{} and \texttt {\$\}})}{107}{subsection.4.2.8}
\contentsline {subsubsection}{Redeclaration of Math Symbols}{108}{section*.23}
\contentsline {subsubsection}{Frames Revisited}{109}{section*.24}
\contentsline {section}{\numberline {4.3}The Anatomy of a Proof}{109}{section.4.3}
\contentsline {subsection}{\numberline {4.3.1}The Concept of Unification}{113}{subsection.4.3.1}
\contentsline {section}{\numberline {4.4}Extensions to the Metamath Language}{113}{section.4.4}
\contentsline {subsection}{\numberline {4.4.1}Comments in the Metamath Language}{113}{subsection.4.4.1}
\contentsline {subsubsection}{Math Symbols and Labels Inside Comments}{114}{section*.25}
\contentsline {subsubsection}{Math Symbols In Comments}{114}{section*.26}
\contentsline {subsubsection}{Label References in Comments}{115}{section*.27}
\contentsline {subsection}{\numberline {4.4.2}Including Other Files in a Metamath Source File}{115}{subsection.4.4.2}
\contentsline {subsection}{\numberline {4.4.3}Compressed Proof Format}{116}{subsection.4.4.3}
\contentsline {subsection}{\numberline {4.4.4}Specifying Unknown Proofs or Subproofs}{117}{subsection.4.4.4}
\contentsline {section}{\numberline {4.5}Appendix: Axioms vs.\ Definitions}{117}{section.4.5}
\contentsline {chapter}{\numberline {5}The Metamath Program}{121}{chapter.5}
\contentsline {section}{\numberline {5.1}Controlling Metamath}{121}{section.5.1}
\contentsline {subsection}{\numberline {5.1.1}\texttt {exit} Command}{121}{subsection.5.1.1}
\contentsline {subsection}{\numberline {5.1.2}\texttt {open log} Command}{121}{subsection.5.1.2}
\contentsline {subsection}{\numberline {5.1.3}\texttt {close log} Command}{121}{subsection.5.1.3}
\contentsline {subsection}{\numberline {5.1.4}\texttt {open tex} Command}{122}{subsection.5.1.4}
\contentsline {subsection}{\numberline {5.1.5}\texttt {close tex} Command}{122}{subsection.5.1.5}
\contentsline {subsection}{\numberline {5.1.6}\texttt {submit} Command}{122}{subsection.5.1.6}
\contentsline {subsection}{\numberline {5.1.7}\texttt {erase} Command}{122}{subsection.5.1.7}
\contentsline {subsection}{\numberline {5.1.8}Operating System Commands}{122}{subsection.5.1.8}
\contentsline {subsection}{\numberline {5.1.9}\texttt {set echo} Command}{123}{subsection.5.1.9}
\contentsline {subsection}{\numberline {5.1.10}\texttt {set scroll} Command}{123}{subsection.5.1.10}
\contentsline {subsection}{\numberline {5.1.11}\texttt {set screen\_width} Command}{123}{subsection.5.1.11}
\contentsline {subsection}{\numberline {5.1.12}\texttt {beep} Command}{123}{subsection.5.1.12}
\contentsline {section}{\numberline {5.2}Reading and Writing Files}{123}{section.5.2}
\contentsline {subsection}{\numberline {5.2.1}\texttt {read} Command}{123}{subsection.5.2.1}
\contentsline {subsection}{\numberline {5.2.2}\texttt {write source} Command}{124}{subsection.5.2.2}
\contentsline {section}{\numberline {5.3}Showing Status and Statements}{124}{section.5.3}
\contentsline {subsection}{\numberline {5.3.1}\texttt {show settings} Command}{124}{subsection.5.3.1}
\contentsline {subsection}{\numberline {5.3.2}\texttt {show memory} Command}{124}{subsection.5.3.2}
\contentsline {subsection}{\numberline {5.3.3}\texttt {show labels} Command}{124}{subsection.5.3.3}
\contentsline {subsection}{\numberline {5.3.4}\texttt {show statement} Command}{124}{subsection.5.3.4}
\contentsline {subsection}{\numberline {5.3.5}\texttt {search} Command}{125}{subsection.5.3.5}
\contentsline {section}{\numberline {5.4}Displaying and Verifying Proofs}{125}{section.5.4}
\contentsline {subsection}{\numberline {5.4.1}\texttt {show proof} Command}{125}{subsection.5.4.1}
\contentsline {subsection}{\numberline {5.4.2}\texttt {show usage} Command}{126}{subsection.5.4.2}
\contentsline {subsection}{\numberline {5.4.3}\texttt {show trace\_back} Command}{126}{subsection.5.4.3}
\contentsline {subsection}{\numberline {5.4.4}\texttt {verify proof} Command}{126}{subsection.5.4.4}
\contentsline {subsection}{\numberline {5.4.5}\texttt {save proof} Command}{127}{subsection.5.4.5}
\contentsline {section}{\numberline {5.5}Changing Label and Symbol Names}{127}{section.5.5}
\contentsline {section}{\numberline {5.6}Creating Proofs}{127}{section.5.6}
\contentsline {subsection}{\numberline {5.6.1}\texttt {prove} Command}{127}{subsection.5.6.1}
\contentsline {subsection}{\numberline {5.6.2}\texttt {set unification\_timeout} Command}{128}{subsection.5.6.2}
\contentsline {subsection}{\numberline {5.6.3}\texttt {set empty\_substitution} Command}{128}{subsection.5.6.3}
\contentsline {subsection}{\numberline {5.6.4}\texttt {set search\_limit} Command}{128}{subsection.5.6.4}
\contentsline {subsection}{\numberline {5.6.5}\texttt {show new\_proof} Command}{128}{subsection.5.6.5}
\contentsline {subsection}{\numberline {5.6.6}\texttt {assign} Command}{129}{subsection.5.6.6}
\contentsline {subsection}{\numberline {5.6.7}\texttt {match} Command}{129}{subsection.5.6.7}
\contentsline {subsection}{\numberline {5.6.8}\texttt {let} Command}{129}{subsection.5.6.8}
\contentsline {subsection}{\numberline {5.6.9}\texttt {unify} Command}{130}{subsection.5.6.9}
\contentsline {subsection}{\numberline {5.6.10}\texttt {initialize} Command}{130}{subsection.5.6.10}
\contentsline {subsection}{\numberline {5.6.11}\texttt {delete} Command}{130}{subsection.5.6.11}
\contentsline {subsection}{\numberline {5.6.12}\texttt {improve} Command}{131}{subsection.5.6.12}
\contentsline {subsection}{\numberline {5.6.13}\texttt {save new\_proof} Command}{131}{subsection.5.6.13}
\contentsline {section}{\numberline {5.7}File Utilities}{132}{section.5.7}
\contentsline {subsection}{\numberline {5.7.1}\texttt {file type} Command}{132}{subsection.5.7.1}
\contentsline {subsection}{\numberline {5.7.2}\texttt {file search} Command}{132}{subsection.5.7.2}
\contentsline {section}{\numberline {5.8}Size Limitations in Metamath}{132}{section.5.8}
\contentsline {chapter}{\numberline {A}Math Symbol Tokens for Set Theory}{133}{appendix.A}
\contentsline {chapter}{\numberline {B}Compressed Proofs}{137}{appendix.B}
\contentsline {chapter}{\numberline {C}Metamath's Formal System}{139}{appendix.C}
\contentsline {section}{\numberline {C.1}Introduction}{139}{section.C.1}
\contentsline {section}{\numberline {C.2}The Formal Description}{140}{section.C.2}
\contentsline {subsection}{\numberline {C.2.1}Preliminaries}{140}{Hfootnote.89}
\contentsline {subsection}{\numberline {C.2.2}Constants, Variables, and Expressions}{140}{subsection.C.2.2}
\contentsline {subsection}{\numberline {C.2.3}Substitution}{141}{subsection.C.2.3}
\contentsline {subsection}{\numberline {C.2.4}Statements}{141}{subsection.C.2.4}
\contentsline {subsection}{\numberline {C.2.5}Formal Systems}{142}{subsection.C.2.5}
\contentsline {section}{\numberline {C.3}Examples of Formal Systems}{143}{section.C.3}
\contentsline {subsection}{\numberline {C.3.1}Example\nobreakspace {}1---Propositional Calculus}{144}{subsection.C.3.1}
\contentsline {subsection}{\numberline {C.3.2}Example\nobreakspace {}2---Predicate Calculus with Equality}{145}{subsection.C.3.2}
\contentsline {subsection}{\numberline {C.3.3}Free Variables and Proper Substitution}{147}{subsection.C.3.3}
\contentsline {subsection}{\numberline {C.3.4}Metalogical Completeness}{148}{subsection.C.3.4}
\contentsline {subsection}{\numberline {C.3.5}Example\nobreakspace {}3---Metalogically Complete Predicate Calculus with Equality}{148}{subsection.C.3.5}
\contentsline {subsection}{\numberline {C.3.6}Example\nobreakspace {}4---Adding Definitions}{150}{subsection.C.3.6}
\contentsline {subsection}{\numberline {C.3.7}Example\nobreakspace {}5---ZFC Set Theory}{150}{subsection.C.3.7}
\contentsline {subsection}{\numberline {C.3.8}Example\nobreakspace {}6---Class Notation in Set Theory}{151}{subsection.C.3.8}
\contentsline {section}{\numberline {C.4}Metamath as a Formal System}{152}{section.C.4}
\contentsline {chapter}{\numberline {D}The MIU System}{155}{appendix.D}
\contentsline {chapter}{\numberline {E}Software Sources}{159}{appendix.E}
\contentsline {chapter}{\numberline {F}Disclaimer and Trademarks}{161}{appendix.F}
\contentsline {chapter}{Bibliography}{163}{section*.28}
\contentsline {chapter}{Index}{169}{section*.30}