\BOOKMARK [1][-]{chapter*.2}{Preface}{}
\BOOKMARK [0][-]{chapter.1}{Introduction}{}
\BOOKMARK [1][-]{section.1.1}{Mathematics as a Computer Language}{chapter.1}
\BOOKMARK [2][-]{subsection.1.1.1}{Is Mathematics ``User-Friendly''?}{section.1.1}
\BOOKMARK [2][-]{subsection.1.1.2}{Mathematics and the Non-Specialist}{section.1.1}
\BOOKMARK [2][-]{subsection.1.1.3}{An Impossible Dream?}{section.1.1}
\BOOKMARK [2][-]{subsection.1.1.4}{Beauty}{section.1.1}
\BOOKMARK [2][-]{subsection.1.1.5}{Simplicity}{section.1.1}
\BOOKMARK [2][-]{subsection.1.1.6}{Rigor}{section.1.1}
\BOOKMARK [1][-]{section.1.2}{Computers and Mathematicians}{chapter.1}
\BOOKMARK [2][-]{subsection.1.2.1}{Trusting the Computer}{section.1.2}
\BOOKMARK [2][-]{subsection.1.2.2}{Trusting the Mathematician}{section.1.2}
\BOOKMARK [1][-]{section.1.3}{The Use of Computers in Mathematics}{chapter.1}
\BOOKMARK [2][-]{subsection.1.3.1}{Computer Algebra Systems}{section.1.3}
\BOOKMARK [2][-]{subsection.1.3.2}{Automated Theorem Provers}{section.1.3}
\BOOKMARK [2][-]{subsection.1.3.3}{Proof Verifiers}{section.1.3}
\BOOKMARK [1][-]{section.1.4}{Mathematics and Metamath}{chapter.1}
\BOOKMARK [2][-]{subsection.1.4.1}{Standard Mathematics}{section.1.4}
\BOOKMARK [2][-]{subsection.1.4.2}{Other Formal Systems}{section.1.4}
\BOOKMARK [2][-]{subsection.1.4.3}{Metamath and Its Philosophy}{section.1.4}
\BOOKMARK [2][-]{subsection.1.4.4}{A History of the Approach Behind Metamath}{section.1.4}
\BOOKMARK [2][-]{subsection.1.4.5}{Metamath and First-Order Logic}{section.1.4}
\BOOKMARK [0][-]{chapter.2}{Using the Metamath Program}{}
\BOOKMARK [1][-]{section.2.1}{Installation}{chapter.2}
\BOOKMARK [1][-]{section.2.2}{Your First Formal System}{chapter.2}
\BOOKMARK [2][-]{subsection.2.2.1}{From Nothing to Zero}{section.2.2}
\BOOKMARK [2][-]{subsection.2.2.2}{Converting It to Metamath}{section.2.2}
\BOOKMARK [1][-]{section.2.3}{A Trial Run}{chapter.2}
\BOOKMARK [2][-]{subsection.2.3.1}{Some Hints for Using the Command Line Interface}{section.2.3}
\BOOKMARK [1][-]{section.2.4}{Your First Proof}{chapter.2}
\BOOKMARK [1][-]{section.2.5}{A Note About Editing a Database File}{chapter.2}
\BOOKMARK [0][-]{chapter.3}{Abstract Mathematics Revealed}{}
\BOOKMARK [1][-]{section.3.1}{Logic and Set Theory}{chapter.3}
\BOOKMARK [1][-]{section.3.2}{The Axioms for All of Mathematics}{chapter.3}
\BOOKMARK [2][-]{subsection.3.2.1}{Propositional Calculus}{section.3.2}
\BOOKMARK [2][-]{subsection.3.2.2}{Predicate Calculus}{section.3.2}
\BOOKMARK [2][-]{subsection.3.2.3}{Equality}{section.3.2}
\BOOKMARK [2][-]{subsection.3.2.4}{Set Theory}{section.3.2}
\BOOKMARK [1][-]{section.3.3}{The Axioms in the Metamath Language}{chapter.3}
\BOOKMARK [2][-]{subsection.3.3.1}{Propositional Calculus}{section.3.3}
\BOOKMARK [2][-]{subsection.3.3.2}{Pure Predicate Calculus}{section.3.3}
\BOOKMARK [2][-]{subsection.3.3.3}{Equality and Substitution}{section.3.3}
\BOOKMARK [2][-]{subsection.3.3.4}{Set Theory}{section.3.3}
\BOOKMARK [2][-]{subsection.3.3.5}{That's It}{section.3.3}
\BOOKMARK [1][-]{section.3.4}{A Hierarchy of Definitions}{chapter.3}
\BOOKMARK [2][-]{subsection.3.4.1}{Definitions for Propositional Calculus}{section.3.4}
\BOOKMARK [2][-]{subsection.3.4.2}{Definitions for Predicate Calculus}{section.3.4}
\BOOKMARK [2][-]{subsection.3.4.3}{Definitions for Set Theory}{section.3.4}
\BOOKMARK [1][-]{section.3.5}{Tricks of the Trade}{chapter.3}
\BOOKMARK [1][-]{section.3.6}{A Theorem Sampler}{chapter.3}
\BOOKMARK [1][-]{section.3.7}{Axioms for Real and Complex Numbers}{chapter.3}
\BOOKMARK [1][-]{section.3.8}{Exploring the Set Theory Database}{chapter.3}
\BOOKMARK [2][-]{subsection.3.8.1}{A Note on ``Compact'' Proof Format}{section.3.8}
\BOOKMARK [0][-]{chapter.4}{The Metamath Language}{}
\BOOKMARK [1][-]{section.4.1}{Specification of the Metamath Language}{chapter.4}
\BOOKMARK [2][-]{subsection.4.1.1}{Preliminaries}{section.4.1}
\BOOKMARK [2][-]{subsection.4.1.2}{Preprocessing}{section.4.1}
\BOOKMARK [2][-]{subsection.4.1.3}{Basic Syntax}{section.4.1}
\BOOKMARK [2][-]{subsection.4.1.4}{Proof Verification}{section.4.1}
\BOOKMARK [1][-]{section.4.2}{The Basic Keywords}{chapter.4}
\BOOKMARK [2][-]{subsection.4.2.1}{User-Defined Tokens}{section.4.2}
\BOOKMARK [2][-]{subsection.4.2.2}{Constants and Variables}{section.4.2}
\BOOKMARK [2][-]{subsection.4.2.3}{The \044c and \044v Declaration Statements}{section.4.2}
\BOOKMARK [2][-]{subsection.4.2.4}{The \044d Statement}{section.4.2}
\BOOKMARK [2][-]{subsection.4.2.5}{The \044f and \044e Statements}{section.4.2}
\BOOKMARK [2][-]{subsection.4.2.6}{Assertions \(\044a and \044p Statements\)}{section.4.2}
\BOOKMARK [2][-]{subsection.4.2.7}{Frames}{section.4.2}
\BOOKMARK [2][-]{subsection.4.2.8}{Scoping Statements \(\044\173 and \044\175\)}{section.4.2}
\BOOKMARK [1][-]{section.4.3}{The Anatomy of a Proof}{chapter.4}
\BOOKMARK [2][-]{subsection.4.3.1}{The Concept of Unification}{section.4.3}
\BOOKMARK [1][-]{section.4.4}{Extensions to the Metamath Language}{chapter.4}
\BOOKMARK [2][-]{subsection.4.4.1}{Comments in the Metamath Language}{section.4.4}
\BOOKMARK [2][-]{subsection.4.4.2}{Including Other Files in a Metamath Source File}{section.4.4}
\BOOKMARK [2][-]{subsection.4.4.3}{Compressed Proof Format}{section.4.4}
\BOOKMARK [2][-]{subsection.4.4.4}{Specifying Unknown Proofs or Subproofs}{section.4.4}
\BOOKMARK [1][-]{section.4.5}{Appendix: Axioms vs. Definitions}{chapter.4}
\BOOKMARK [0][-]{chapter.5}{The Metamath Program}{}
\BOOKMARK [1][-]{section.5.1}{Controlling Metamath}{chapter.5}
\BOOKMARK [2][-]{subsection.5.1.1}{exit Command}{section.5.1}
\BOOKMARK [2][-]{subsection.5.1.2}{open log Command}{section.5.1}
\BOOKMARK [2][-]{subsection.5.1.3}{close log Command}{section.5.1}
\BOOKMARK [2][-]{subsection.5.1.4}{open tex Command}{section.5.1}
\BOOKMARK [2][-]{subsection.5.1.5}{close tex Command}{section.5.1}
\BOOKMARK [2][-]{subsection.5.1.6}{submit Command}{section.5.1}
\BOOKMARK [2][-]{subsection.5.1.7}{erase Command}{section.5.1}
\BOOKMARK [2][-]{subsection.5.1.8}{Operating System Commands}{section.5.1}
\BOOKMARK [2][-]{subsection.5.1.9}{set echo Command}{section.5.1}
\BOOKMARK [2][-]{subsection.5.1.10}{set scroll Command}{section.5.1}
\BOOKMARK [2][-]{subsection.5.1.11}{set screen\137width Command}{section.5.1}
\BOOKMARK [2][-]{subsection.5.1.12}{beep Command}{section.5.1}
\BOOKMARK [1][-]{section.5.2}{Reading and Writing Files}{chapter.5}
\BOOKMARK [2][-]{subsection.5.2.1}{read Command}{section.5.2}
\BOOKMARK [2][-]{subsection.5.2.2}{write source Command}{section.5.2}
\BOOKMARK [1][-]{section.5.3}{Showing Status and Statements}{chapter.5}
\BOOKMARK [2][-]{subsection.5.3.1}{show settings Command}{section.5.3}
\BOOKMARK [2][-]{subsection.5.3.2}{show memory Command}{section.5.3}
\BOOKMARK [2][-]{subsection.5.3.3}{show labels Command}{section.5.3}
\BOOKMARK [2][-]{subsection.5.3.4}{show statement Command}{section.5.3}
\BOOKMARK [2][-]{subsection.5.3.5}{search Command}{section.5.3}
\BOOKMARK [1][-]{section.5.4}{Displaying and Verifying Proofs}{chapter.5}
\BOOKMARK [2][-]{subsection.5.4.1}{show proof Command}{section.5.4}
\BOOKMARK [2][-]{subsection.5.4.2}{show usage Command}{section.5.4}
\BOOKMARK [2][-]{subsection.5.4.3}{show trace\137back Command}{section.5.4}
\BOOKMARK [2][-]{subsection.5.4.4}{verify proof Command}{section.5.4}
\BOOKMARK [2][-]{subsection.5.4.5}{save proof Command}{section.5.4}
\BOOKMARK [1][-]{section.5.5}{Changing Label and Symbol Names}{chapter.5}
\BOOKMARK [1][-]{section.5.6}{Creating Proofs}{chapter.5}
\BOOKMARK [2][-]{subsection.5.6.1}{prove Command}{section.5.6}
\BOOKMARK [2][-]{subsection.5.6.2}{set unification\137timeout Command}{section.5.6}
\BOOKMARK [2][-]{subsection.5.6.3}{set empty\137substitution Command}{section.5.6}
\BOOKMARK [2][-]{subsection.5.6.4}{set search\137limit Command}{section.5.6}
\BOOKMARK [2][-]{subsection.5.6.5}{show new\137proof Command}{section.5.6}
\BOOKMARK [2][-]{subsection.5.6.6}{assign Command}{section.5.6}
\BOOKMARK [2][-]{subsection.5.6.7}{match Command}{section.5.6}
\BOOKMARK [2][-]{subsection.5.6.8}{let Command}{section.5.6}
\BOOKMARK [2][-]{subsection.5.6.9}{unify Command}{section.5.6}
\BOOKMARK [2][-]{subsection.5.6.10}{initialize Command}{section.5.6}
\BOOKMARK [2][-]{subsection.5.6.11}{delete Command}{section.5.6}
\BOOKMARK [2][-]{subsection.5.6.12}{improve Command}{section.5.6}
\BOOKMARK [2][-]{subsection.5.6.13}{save new\137proof Command}{section.5.6}
\BOOKMARK [1][-]{section.5.7}{File Utilities}{chapter.5}
\BOOKMARK [2][-]{subsection.5.7.1}{file type Command}{section.5.7}
\BOOKMARK [2][-]{subsection.5.7.2}{file search Command}{section.5.7}
\BOOKMARK [1][-]{section.5.8}{Size Limitations in Metamath}{chapter.5}
\BOOKMARK [0][-]{appendix.A}{Math Symbol Tokens for Set Theory}{}
\BOOKMARK [0][-]{appendix.B}{Compressed Proofs}{}
\BOOKMARK [0][-]{appendix.C}{Metamath's Formal System}{}
\BOOKMARK [1][-]{section.C.1}{Introduction}{appendix.C}
\BOOKMARK [1][-]{section.C.2}{The Formal Description}{appendix.C}
\BOOKMARK [2][-]{Hfootnote.89}{Preliminaries}{section.C.2}
\BOOKMARK [2][-]{subsection.C.2.2}{Constants, Variables, and Expressions}{section.C.2}
\BOOKMARK [2][-]{subsection.C.2.3}{Substitution}{section.C.2}
\BOOKMARK [2][-]{subsection.C.2.4}{Statements}{section.C.2}
\BOOKMARK [2][-]{subsection.C.2.5}{Formal Systems}{section.C.2}
\BOOKMARK [1][-]{section.C.3}{Examples of Formal Systems}{appendix.C}
\BOOKMARK [2][-]{subsection.C.3.1}{Example 1---Propositional Calculus}{section.C.3}
\BOOKMARK [2][-]{subsection.C.3.2}{Example 2---Predicate Calculus with Equality}{section.C.3}
\BOOKMARK [2][-]{subsection.C.3.3}{Free Variables and Proper Substitution}{section.C.3}
\BOOKMARK [2][-]{subsection.C.3.4}{Metalogical Completeness}{section.C.3}
\BOOKMARK [2][-]{subsection.C.3.5}{Example 3---Metalogically Complete Predicate Calculus with Equality}{section.C.3}
\BOOKMARK [2][-]{subsection.C.3.6}{Example 4---Adding Definitions}{section.C.3}
\BOOKMARK [2][-]{subsection.C.3.7}{Example 5---ZFC Set Theory}{section.C.3}
\BOOKMARK [2][-]{subsection.C.3.8}{Example 6---Class Notation in Set Theory}{section.C.3}
\BOOKMARK [1][-]{section.C.4}{Metamath as a Formal System}{appendix.C}
\BOOKMARK [0][-]{appendix.D}{The MIU System}{}
\BOOKMARK [0][-]{appendix.E}{Software Sources}{}
\BOOKMARK [0][-]{appendix.F}{Disclaimer and Trademarks}{}
\BOOKMARK [0][-]{section*.28}{Bibliography}{}
\BOOKMARK [0][-]{section*.30}{Index}{}