\begin{theindex}

  \item \texttt{\$(} and \texttt{\$)} auxiliary keywords, 
		\hyperpage{38}, \hyperpage{93}, \hyperpage{97}, 
		\hyperpage{119}
  \item \texttt{\$.}\ keyword, \hyperpage{38, 39}, \hyperpage{46}, 
		\hyperpage{96}, \hyperpage{98}
  \item \texttt{\$=} keyword, \hyperpage{39}, \hyperpage{46}, 
		\hyperpage{96}, \hyperpage{98}, \hyperpage{107}, 
		\hyperpage{114}, \hyperpage{124}
  \item \texttt{\$[} and \texttt{\$]} auxiliary keywords, 
		\hyperpage{93}, \hyperpage{97}, \hyperpage{122}, 
		\hyperpage{135}
  \item \texttt{\$\char`\{} and \texttt{\$\char`\}} keywords, 
		\hyperpage{39}, \hyperpage{96}, \hyperpage{111, 112}
  \item \texttt{\$a} statement, \hyperpage{38, 39}, \hyperpage{89}, 
		\hyperpage{94}, \hyperpage{96}, \hyperpage{98}, 
		\hyperpage{104}, \hyperpage{106--108}, 
		\hyperpage{113--115}, \hyperpage{125}, \hyperpage{135}
  \item \texttt{\$c} statement, \hyperpage{38, 39}, \hyperpage{93}, 
		\hyperpage{96}, \hyperpage{99, 100}, \hyperpage{113}
  \item \texttt{\$d} statement, \hyperpage{63}, \hyperpage{65}, 
		\hyperpage{95, 96}, \hyperpage{100--102}, 
		\hyperpage{104, 105}, \hyperpage{113}, \hyperpage{118}, 
		\hyperpage{141}, \hyperpage{146}
    \subitem compound, \hyperpage{94}
    \subitem simple, \hyperpage{94}
  \item \texttt{\$e} statement, \hyperpage{38, 39}, \hyperpage{94}, 
		\hyperpage{96}, \hyperpage{98}, \hyperpage{105, 106}, 
		\hyperpage{113, 114}, \hyperpage{135}, \hyperpage{138}, 
		\hyperpage{143}, \hyperpage{146}
  \item \texttt{\$f} statement, \hyperpage{38, 39}, \hyperpage{45}, 
		\hyperpage{83}, \hyperpage{94}, \hyperpage{96}, 
		\hyperpage{98}, \hyperpage{105, 106}, 
		\hyperpage{113--115}, \hyperpage{135}, \hyperpage{137}, 
		\hyperpage{145, 146}
  \item \texttt{\$p} statement, \hyperpage{38, 39}, \hyperpage{94}, 
		\hyperpage{96}, \hyperpage{98}, \hyperpage{106, 107}, 
		\hyperpage{113--115}, \hyperpage{117}, \hyperpage{124}, 
		\hyperpage{135, 136}, \hyperpage{138}
  \item \texttt{\$t} comment, \hyperpage{98}, \hyperpage{119--121}, 
		\hyperpage{148}, \hyperpage{155}
  \item \texttt{\$v} statement, \hyperpage{38, 39}, \hyperpage{93}, 
		\hyperpage{96}, \hyperpage{99, 100}, \hyperpage{113}
  \item \texttt{\char`\[}\ldots\texttt{]} inside comments, 
		\hyperpage{121}, \hyperpage{149}
  \item \texttt{\char`\_} inside comments, \hyperpage{121}
  \item \texttt{\char`\~} inside comments, \hyperpage{119}, 
		\hyperpage{121}
  \item \texttt{?}\ in command lines, \hyperpage{46}
  \item \texttt{?}\ inside proofs, \hyperpage{46}, \hyperpage{124}
  \item \texttt{`} inside comments, \hyperpage{119}, \hyperpage{121}
  \item \texttt{althtmldef} statement, \hyperpage{149}, \hyperpage{156}
  \item \texttt{althtmldir} statement, \hyperpage{149}
  \item \texttt{assign} command, \hyperpage{48}, \hyperpage{143}
  \item \texttt{beep} command, \hyperpage{133}
  \item \texttt{close log} command, \hyperpage{132}
  \item \texttt{close tex} command, \hyperpage{147}
  \item \texttt{delete} command, \hyperpage{145}
  \item \texttt{erase} command, \hyperpage{132}
  \item \texttt{exit} command, \hyperpage{45}, \hyperpage{131}
  \item \texttt{exthtmlbibliography} statement, \hyperpage{150}
  \item \texttt{exthtmlhome} statement, \hyperpage{150}
  \item \texttt{exthtmllabel} statement, \hyperpage{150}
  \item \texttt{exthtmltitle} statement, \hyperpage{150}
  \item \texttt{help} command, \hyperpage{45}
  \item \texttt{htmlbibliography} statement, \hyperpage{149}
  \item \texttt{htmldef} statement, \hyperpage{148}, \hyperpage{156}
  \item \texttt{htmldir} statement, \hyperpage{149}
  \item \texttt{htmlhome} statement, \hyperpage{149}
  \item \texttt{htmltitle} statement, \hyperpage{149}
  \item \texttt{htmlvarcolors} statement, \hyperpage{149}
  \item \texttt{improve} command, \hyperpage{145}
  \item \texttt{initialize} command, \hyperpage{145}
  \item \texttt{latexdef} statement, \hyperpage{155}
  \item \texttt{let} command, \hyperpage{143}
  \item \texttt{match} command, \hyperpage{143}
  \item \texttt{minimize{\char`\_}with} command, \hyperpage{53}, 
		\hyperpage{141}
  \item \texttt{more} command, \hyperpage{133}
  \item \texttt{open log} command, \hyperpage{131}
  \item \texttt{open tex} command, \hyperpage{98}, \hyperpage{147}
  \item \texttt{prove} command, \hyperpage{47}, \hyperpage{141}
  \item \texttt{read} command, \hyperpage{41}, \hyperpage{45, 46}, 
		\hyperpage{83}, \hyperpage{134}
  \item \texttt{save new{\char`\_}proof} command, \hyperpage{52}, 
		\hyperpage{124}, \hyperpage{146}
  \item \texttt{save proof} command, \hyperpage{90}, \hyperpage{124}, 
		\hyperpage{138}
  \item \texttt{search} command, \hyperpage{84}, \hyperpage{88}, 
		\hyperpage{136}
  \item \texttt{set echo} command, \hyperpage{132}
  \item \texttt{set empty{\char`\_}substitution} command, 
		\hyperpage{49}, \hyperpage{142}
  \item \texttt{set height} command, \hyperpage{133}
  \item \texttt{set scroll} command, \hyperpage{132}
  \item \texttt{set search{\char`\_}limit} command, \hyperpage{142}
  \item \texttt{set unification{\char`\_}timeout} command, 
		\hyperpage{141}
  \item \texttt{set width} command, \hyperpage{132}
  \item \texttt{show        trace{\char`\_}back} command, 
		\hyperpage{138}
  \item \texttt{show labels} command, \hyperpage{42}, \hyperpage{135}
  \item \texttt{show memory} command, \hyperpage{135}
  \item \texttt{show new{\char`\_}proof} command, \hyperpage{47}, 
		\hyperpage{142}
  \item \texttt{show proof} command, \hyperpage{37}, \hyperpage{42}, 
		\hyperpage{45, 46}, \hyperpage{52}, \hyperpage{85, 86}, 
		\hyperpage{117, 118}, \hyperpage{136}
  \item \texttt{show settings} command, \hyperpage{135}
  \item \texttt{show statement} command, \hyperpage{39}, \hyperpage{42}, 
		\hyperpage{53}, \hyperpage{63}, \hyperpage{68}, 
		\hyperpage{84, 85}, \hyperpage{135}
  \item \texttt{show trace{\char`\_}back} command, \hyperpage{17}, 
		\hyperpage{88}
  \item \texttt{show usage} command, \hyperpage{89}, \hyperpage{137}
  \item \texttt{submit} command, \hyperpage{45}, \hyperpage{132}
  \item \texttt{tools} command, \hyperpage{135}, \hyperpage{151}
  \item \texttt{unify} command, \hyperpage{144}
  \item \texttt{verify proof} command, \hyperpage{41}, \hyperpage{114}, 
		\hyperpage{124}, \hyperpage{138}
  \item \texttt{write bibliography} command, \hyperpage{151}
  \item \texttt{write recent{\char`\_}additions} command, 
		\hyperpage{151}
  \item \texttt{write source} command, \hyperpage{46}, \hyperpage{134}
  \item \texttt{write theorem{\char`\_}list} command, \hyperpage{150}

  \indexspace

  \item abstract algebra, \hyperpage{3}
  \item abstraction class, \hyperpage{56}, \hyperpage{70}, 
		\hyperpage{174}
    \subitem of nested ordered pairs, \hyperpage{127}
    \subitem of ordered pairs, \hyperpage{73}
  \item active math symbol, \hyperpage{93}, \hyperpage{100}, 
		\hyperpage{113}
  \item active statement, \hyperpage{94}, \hyperpage{113}
  \item addition, \hyperpage{127}
    \subitem of ordinals, \hyperpage{127}
  \item ambiguous unification, \hyperpage{49}, \hyperpage{119}, 
		\hyperpage{142}, \hyperpage{146}
  \item analysis, \hyperpage{3}, \hyperpage{29}
  \item Anderson, Alan Ross, \hyperpage{17}
  \item Andr{\'{e}}ka, H., \hyperpage{105}, \hyperpage{164}
  \item Appel, K., \hyperpage{23}
  \item {\sc ascii}, \hyperpage{33}, \hyperpage{92}, \hyperpage{96}
  \item assertion, \hyperpage{39, 40}, \hyperpage{94}, \hyperpage{106}, 
		\hyperpage{114}
    \subitem in a formal system, \hyperpage{164}
  \item assertion label, \hyperpage{40}, \hyperpage{115}, 
		\hyperpage{118}
  \item Auden, W.\ H., \hyperpage{5}
  \item Aussonderung, \hyperpage{78}
  \item automated proof verification, \hyperpage{19, 20}
  \item automated theorem proving, \hyperpage{21}, \hyperpage{26, 27}, 
		\hyperpage{61}
  \item auxiliary keyword, \hyperpage{92}, \hyperpage{96}
  \item axiom, \hyperpage{vii}, \hyperpage{2}, \hyperpage{17}, 
		\hyperpage{19}, \hyperpage{29}, \hyperpage{31}, 
		\hyperpage{34--38}, \hyperpage{55}, \hyperpage{57}, 
		\hyperpage{88}, \hyperpage{98}, \hyperpage{107, 108}, 
		\hyperpage{125, 126}
  \item Axiom of Choice, \hyperpage{17}, \hyperpage{62}, \hyperpage{66}, 
		\hyperpage{174}
  \item Axiom of Extensionality, \hyperpage{62}, \hyperpage{65}, 
		\hyperpage{67}, \hyperpage{71}, \hyperpage{174}
  \item Axiom of Infinity, \hyperpage{32}, \hyperpage{62}, 
		\hyperpage{66}, \hyperpage{80}, \hyperpage{174}
  \item Axiom of Pairing, \hyperpage{62}, \hyperpage{78}
  \item Axiom of Power Sets, \hyperpage{62}, \hyperpage{65}, 
		\hyperpage{174}
  \item Axiom of Regularity, \hyperpage{62}, \hyperpage{65}, 
		\hyperpage{174}
  \item Axiom of Replacement, \hyperpage{62}, \hyperpage{65}, 
		\hyperpage{174}
  \item Axiom of Separation, \hyperpage{62}, \hyperpage{78}
  \item Axiom of the Null Set, \hyperpage{32}, \hyperpage{62}, 
		\hyperpage{78}
  \item Axiom of Union, \hyperpage{62}, \hyperpage{65}, \hyperpage{174}
  \item axiom scheme, \hyperpage{35}, \hyperpage{59}, \hyperpage{63}
  \item axiom vs.\ definition, \hyperpage{88}, \hyperpage{107}, 
		\hyperpage{125, 126}
  \item axiomatic assertion, \hyperpage{39}, \hyperpage{106}
  \item axiomatic statement
    \subitem in a formal system, \hyperpage{165}
  \item axioms for mathematics, \hyperpage{58}
  \item axioms in \texttt{set.mm}, \hyperpage{64}
  \item axioms of equality, \hyperpage{61}, \hyperpage{64}
  \item axioms of logic, \hyperpage{56}
  \item axioms of predicate calculus, \hyperpage{60}, \hyperpage{64}
  \item axioms of propositional calculus, \hyperpage{58}, 
		\hyperpage{64}
  \item axioms of set theory, \hyperpage{62}, \hyperpage{65}

  \indexspace

  \item Barrow, John D., \hyperpage{xi}
  \item basic keyword, \hyperpage{96}
  \item basic language, \hyperpage{96}, \hyperpage{99}, \hyperpage{114}, 
		\hyperpage{138}, \hyperpage{146}
  \item Behnke, H., \hyperpage{30}, \hyperpage{125}
  \item Bell, J. L., \hyperpage{68}
  \item Bible, \hyperpage{16}
  \item biconditional ($\leftrightarrow$), \hyperpage{65}, 
		\hyperpage{67, 68}, \hyperpage{173}
  \item binary relation, \hyperpage{73}, \hyperpage{80}
  \item Blass, Andrea, \hyperpage{31}
  \item Bledsoe, W. W., \hyperpage{27}
  \item block, \hyperpage{39}, \hyperpage{93}, \hyperpage{112}
    \subitem outermost, \hyperpage{93}
  \item Boolean algebra, \hyperpage{26}
  \item Boolos, George S., \hyperpage{15}, \hyperpage{17}
  \item bound variable, \hyperpage{32}, \hyperpage{100}
  \item Bourbaki, Nicholaus, \hyperpage{xi}, \hyperpage{15}
  \item brace notation, \hyperpage{56}
  \item Bunder, Martin, \hyperpage{17}
  \item Burali-Forti paradox, \hyperpage{79}

  \indexspace

  \item Cantor's theorem, \hyperpage{79}
  \item Cantor, Georg, \hyperpage{23}
  \item cardinal, inaccessible, \hyperpage{xii}, \hyperpage{31}
  \item cardinal, transfinite, \hyperpage{23}
  \item cardinality, \hyperpage{23}
  \item category theory, \hyperpage{xii}, \hyperpage{29}, 
		\hyperpage{31}
  \item certainty, \hyperpage{18}
  \item Chou, Shang-Ching, \hyperpage{25}
  \item class, \hyperpage{67}, \hyperpage{70}
    \subitem proper, \hyperpage{70}, \hyperpage{174}
  \item class abstraction, \hyperpage{56}, \hyperpage{70}, 
		\hyperpage{174}
  \item class difference, \hyperpage{72}
  \item class equality, \hyperpage{71}
  \item class membership, \hyperpage{71}
  \item class variable, \hyperpage{174}
  \item Clifford algebras, \hyperpage{24}
  \item closure, \hyperpage{165}
  \item Cohen, Paul, \hyperpage{23}
  \item collection, \hyperpage{61}
  \item command keyword, \hyperpage{41}, \hyperpage{45}, \hyperpage{83}
  \item command line interface (CLI), \hyperpage{40}, \hyperpage{45}
  \item command qualifier, \hyperpage{42}
  \item comment, \hyperpage{93}, \hyperpage{119}
  \item comments
    \subitem markup notation, \hyperpage{119}, \hyperpage{121}
  \item compact proof, \hyperpage{89}
  \item composition, \hyperpage{75}
  \item compound declaration, \hyperpage{100}
  \item compressed proof, \hyperpage{40}, \hyperpage{52}, 
		\hyperpage{95}, \hyperpage{123, 124}, \hyperpage{159}
  \item computer algebra system, \hyperpage{3}, \hyperpage{21}, 
		\hyperpage{24}
  \item computer program bugs, \hyperpage{viii}, \hyperpage{8}, 
		\hyperpage{12}, \hyperpage{19}, \hyperpage{21, 22}, 
		\hyperpage{25}
  \item computers and pure mathematics, \hyperpage{21}
  \item concatenation, \hyperpage{162}
  \item condensed detachment, \hyperpage{31}
    \subitem and first-order logic, \hyperpage{31}
  \item conjunction ($\wedge$), \hyperpage{65}, \hyperpage{69}, 
		\hyperpage{87}, \hyperpage{173}
  \item connective, \hyperpage{68}
  \item consistent theory, \hyperpage{18}
  \item constant, \hyperpage{x}, \hyperpage{38}, \hyperpage{40}, 
		\hyperpage{68}, \hyperpage{93}, \hyperpage{99}, 
		\hyperpage{113}
    \subitem in a formal system, \hyperpage{162}
    \subitem in predicate calculus, \hyperpage{63}
  \item constant declaration, \hyperpage{38, 39}, \hyperpage{99}
  \item constant-prefixed expression, \hyperpage{163}
  \item constant-variable pair, \hyperpage{163}
  \item constructive language, \hyperpage{20}
  \item constructivism, \hyperpage{17}
  \item continuum hypothesis, \hyperpage{23}
  \item Courant, Richard, \hyperpage{23}
  \item Courier font, \hyperpage{33}
  \item Coxeter, H. S. M., \hyperpage{24}
  \item cranks, \hyperpage{13}
  \item creative definition, \hyperpage{67}, \hyperpage{125}
  \item cross product, \hyperpage{74}
  \item Curry, Haskell B., \hyperpage{18}

  \indexspace

  \item database, \hyperpage{38}, \hyperpage{92}, \hyperpage{96}, 
		\hyperpage{134}
  \item Davis, Phillip J., \hyperpage{1}, \hyperpage{12}, 
		\hyperpage{14}, \hyperpage{30}
  \item de Millo, Richard, \hyperpage{15}
  \item de Saint-Exupery, Antoine, \hyperpage{161}
  \item decidable theory, \hyperpage{25}
  \item decision procedure, \hyperpage{61}
  \item declaration, \hyperpage{93}
  \item deduction theorem, \hyperpage{11}
  \item definiendum, \hyperpage{67}
  \item definiens, \hyperpage{67}
  \item definition, \hyperpage{15}, \hyperpage{66}, \hyperpage{88}, 
		\hyperpage{98}, \hyperpage{107}, \hyperpage{125, 126}, 
		\hyperpage{172}
    \subitem creative, \hyperpage{67}, \hyperpage{125}
    \subitem eliminability, \hyperpage{67}
    \subitem proper, \hyperpage{108}, \hyperpage{125}
  \item disjoint sets, \hyperpage{62}
  \item disjoint variables, \hyperpage{63}, \hyperpage{101}
  \item disjoint-variable restriction, \hyperpage{94}
    \subitem in a formal system, \hyperpage{164}
  \item disjunction ($\vee$), \hyperpage{69}, \hyperpage{125}, 
		\hyperpage{173}
  \item distinct variables, \hyperpage{32}, \hyperpage{63}, 
		\hyperpage{65}, \hyperpage{100}, \hyperpage{103}
  \item domain, \hyperpage{23}, \hyperpage{74}
  \item dummy variable, \hyperpage{85}, \hyperpage{110}
    \subitem eliminating, \hyperpage{27}, \hyperpage{105}
    \subitem in definitions, \hyperpage{67}

  \indexspace

  \item Edwards, Robert E., \hyperpage{14}
  \item effectively bound variable, \hyperpage{67}
  \item effectively not free, \hyperpage{76}, \hyperpage{170}
  \item element, \hyperpage{61}
  \item empty domain, \hyperpage{32}
  \item empty set, \hyperpage{56}, \hyperpage{72}, \hyperpage{175}
  \item empty substitution, \hyperpage{101}, \hyperpage{142}
  \item Enderton, Herbert B., \hyperpage{17}, \hyperpage{23}, 
		\hyperpage{68}, \hyperpage{84}
  \item epsilon relation, \hyperpage{73}
  \item equality ($=$), \hyperpage{60, 61}, \hyperpage{67}
  \item error checking, \hyperpage{122}, \hyperpage{148}
  \item errors in proofs, \hyperpage{22}, \hyperpage{24}
  \item essential hypothesis, \hyperpage{39}, \hyperpage{105}
  \item Euclidean geometry, \hyperpage{xi}, \hyperpage{23}, 
		\hyperpage{25}
  \item existential quantifier ($\exists$), \hyperpage{65}, 
		\hyperpage{69}, \hyperpage{173}
    \subitem restricted, \hyperpage{71}
  \item existential uniqueness quantifier ($\exists !$), \hyperpage{70}
  \item expression, \hyperpage{95}, \hyperpage{99}
    \subitem in a formal system, \hyperpage{163}
  \item extended frame, \hyperpage{110}
  \item extended language, \hyperpage{97}, \hyperpage{119}

  \indexspace

  \item family, \hyperpage{61}
  \item Feferman, Solomon, \hyperpage{xii}
  \item Fermat's Last Theorem, \hyperpage{13}, \hyperpage{23}, 
		\hyperpage{25}
  \item file inclusion, \hyperpage{93}, \hyperpage{122}
  \item file names
    \subitem Macintosh, \hyperpage{41}, \hyperpage{123}
    \subitem Unix, \hyperpage{41}, \hyperpage{129}, \hyperpage{134}
  \item finitary proof, \hyperpage{29, 30}
  \item finite $n$-termed sequence, \hyperpage{162}
  \item finite induction, \hyperpage{79}
  \item first-order logic, \hyperpage{11}, \hyperpage{20}, 
		\hyperpage{26}, \hyperpage{31}, \hyperpage{56}
    \subitem completeness, \hyperpage{11}
  \item floating hypothesis, \hyperpage{39}, \hyperpage{105}
  \item formal logic, \hyperpage{19}, \hyperpage{107}
  \item formal proof, \hyperpage{x}, \hyperpage{12, 13}, \hyperpage{15}, 
		\hyperpage{19, 20}, \hyperpage{32}, \hyperpage{34}, 
		\hyperpage{36, 37}, \hyperpage{42}, \hyperpage{44}, 
		\hyperpage{46}, \hyperpage{48}
  \item formal system, \hyperpage{vii}, \hyperpage{ix}, \hyperpage{2}, 
		\hyperpage{19}, \hyperpage{29}, \hyperpage{142}, 
		\hyperpage{165}, \hyperpage{177}
  \item formalism, \hyperpage{30}
  \item foundations of mathematics, \hyperpage{17}
  \item founded relation, \hyperpage{73}
  \item four-color theorem, \hyperpage{21}, \hyperpage{23}
  \item frame, \hyperpage{108}
  \item frames and scoping statements, \hyperpage{114}
  \item free logic, \hyperpage{32}
  \item free variable, \hyperpage{32}, \hyperpage{60, 61}, 
		\hyperpage{63}, \hyperpage{100}, \hyperpage{106}, 
		\hyperpage{170}
  \item free vs.\ bound variable, \hyperpage{100}
  \item Frege, Gottlob, \hyperpage{18}
  \item function, \hyperpage{23}, \hyperpage{75}
    \subitem in predicate calculus, \hyperpage{63}
  \item function value, \hyperpage{76}

  \indexspace

  \item G\"{o}del's incompleteness theorem, \hyperpage{ix}, 
		\hyperpage{5}, \hyperpage{15}, \hyperpage{18}
  \item gaps in proofs, \hyperpage{19}
  \item Ghilbert, \hyperpage{xii}
  \item global statement, \hyperpage{113}
  \item Goodstein, R. L., \hyperpage{126}
  \item grave accent (\texttt{`}), \hyperpage{119, 120}
  \item Grothendieck, Alexander, \hyperpage{xii}
  \item group theory, \hyperpage{3}
  \item Guillen, Michael, \hyperpage{5}

  \indexspace

  \item Haken, W., \hyperpage{23}
  \item Halmos, Paul, \hyperpage{21}
  \item Hamilton, Alan G., \hyperpage{60}, \hyperpage{86}
  \item Hardy, G. H., \hyperpage{92}
  \item Harrison, John, \hyperpage{20}, \hyperpage{25}
  \item Herrlich, Horst, \hyperpage{31}
  \item hierarchy, \hyperpage{13}, \hyperpage{15}, \hyperpage{19}, 
		\hyperpage{26}, \hyperpage{88}
  \item higher-order logic, \hyperpage{20}, \hyperpage{29}
  \item Hilbert, David, \hyperpage{15, 16}, \hyperpage{23}, 
		\hyperpage{29, 30}
  \item Hindley, J. Roger, \hyperpage{31}
  \item Hofstadter, Douglas R., \hyperpage{29}, \hyperpage{36}, 
		\hyperpage{179}
  \item {\sc hol}, \hyperpage{27, 28}
  \item {\sc html} generation, \hyperpage{121}, \hyperpage{136}, 
		\hyperpage{156}
  \item Hume, David, \hyperpage{22}
  \item Huntington, E. V., \hyperpage{26}
  \item hypothesis, \hyperpage{39}, \hyperpage{94}, \hyperpage{105}
  \item hypothesis association, \hyperpage{118}
  \item hypothesis label, \hyperpage{40}, \hyperpage{115}

  \indexspace

  \item iff, \hyperpage{73}
  \item image, \hyperpage{75}
  \item implication ($\rightarrow$), \hyperpage{34}, \hyperpage{58}
  \item implicit axiom, \hyperpage{32}
  \item included file, \hyperpage{93}, \hyperpage{122}
  \item individual metavariable, \hyperpage{168}
  \item individual variable, \hyperpage{59}
  \item inference, \hyperpage{106}, \hyperpage{167}
  \item inference rule, \hyperpage{35}
  \item infinite set, \hyperpage{56}
  \item infinity, \hyperpage{23}
  \item infix connective, \hyperpage{69}
  \item informal proof, \hyperpage{13}, \hyperpage{15}
  \item integer, \hyperpage{56, 57}
  \item intersection, \hyperpage{72, 73}
  \item intuitionism, \hyperpage{17}, \hyperpage{29}, \hyperpage{126}
  \item Isabelle, \hyperpage{27}

  \indexspace

  \item Kalman, J. A., \hyperpage{31}
  \item Kempe, A. B., \hyperpage{23}
  \item keyword, \hyperpage{38}, \hyperpage{92}, \hyperpage{96, 97}
  \item Kline, Morris, \hyperpage{18}, \hyperpage{30}
  \item Koch, K., \hyperpage{23}
  \item Kronecker, Leopold, \hyperpage{16}
  \item Kuratowski, Kazimierz, \hyperpage{72}

  \indexspace

  \item label, \hyperpage{39}, \hyperpage{42}, \hyperpage{45}, 
		\hyperpage{93}, \hyperpage{96}, \hyperpage{98}, 
		\hyperpage{103}, \hyperpage{105}, \hyperpage{107, 108}, 
		\hyperpage{115}, \hyperpage{118}
  \item label declaration, \hyperpage{98}
  \item label mode, \hyperpage{120, 121}
  \item label reference, \hyperpage{98}, \hyperpage{114}
  \item label sequence, \hyperpage{98}, \hyperpage{114}
  \item labels in \texttt{set.mm}, \hyperpage{88}
  \item Landau, Edmund, \hyperpage{5}
  \item {\LaTeX}, \hyperpage{ix}, \hyperpage{34}, \hyperpage{85}, 
		\hyperpage{98}, \hyperpage{119}, \hyperpage{137}, 
		\hyperpage{147, 148}
    \subitem characters per line, \hyperpage{133}
  \item \LaTeX\ definitions, \hyperpage{155}
  \item {\sc lcf}, \hyperpage{28}
  \item Le\'{s}niewski, S., \hyperpage{125}
  \item Leblanc, Hugues, \hyperpage{32}
  \item Lejewski, Czeslaw, \hyperpage{125}
  \item Lemmon-style proof, \hyperpage{43}
  \item length of a sequence ({$|\ |$}), \hyperpage{162}
  \item Levien, Raph, \hyperpage{xii}
  \item limit ordinal, \hyperpage{74}
  \item local label, \hyperpage{90}
  \item local variable, \hyperpage{113}
  \item logic, \hyperpage{2}
  \item logical equivalence ($\leftrightarrow$), \hyperpage{65}, 
		\hyperpage{67, 68}, \hyperpage{173}
  \item logical hypothesis, \hyperpage{39}, \hyperpage{105}
    \subitem in a formal system, \hyperpage{164}
  \item logical {\sc and} ($\wedge$), \hyperpage{65}, \hyperpage{69}, 
		\hyperpage{87}
  \item logical {\sc or} ($\vee$), \hyperpage{69}
  \item Lounesto, Pertti, \hyperpage{24}

  \indexspace

  \item Mac Lane, Saunders, \hyperpage{xii}
  \item Macintosh file names, \hyperpage{41}, \hyperpage{123}
  \item {\sc macsyma}, \hyperpage{3}
  \item mandatory \texttt{\$d} statement, \hyperpage{118}
  \item mandatory disjoint-variable restriction, \hyperpage{94}
    \subitem in a formal system, \hyperpage{164}
  \item mandatory hypothesis, \hyperpage{39}, \hyperpage{42}, 
		\hyperpage{53}, \hyperpage{94}, \hyperpage{110}, 
		\hyperpage{115}, \hyperpage{117, 118}, \hyperpage{124}
    \subitem in a formal system, \hyperpage{164}
  \item mandatory variable, \hyperpage{94}, \hyperpage{109}
  \item mandatory variable-type hypothesis
    \subitem in a formal system, \hyperpage{164}
  \item Maple, \hyperpage{3}, \hyperpage{25}
  \item mapping, \hyperpage{23}
  \item markup notation, \hyperpage{119}, \hyperpage{121}
  \item math mode, \hyperpage{119, 120}
  \item math symbol, \hyperpage{38, 39}, \hyperpage{44, 45}, 
		\hyperpage{60}, \hyperpage{93}, \hyperpage{96--99}, 
		\hyperpage{113}, \hyperpage{120}
  \item Mathematica, \hyperpage{3}, \hyperpage{24}
  \item Mathematica and proofs, \hyperpage{25}
  \item mathematical induction, \hyperpage{79}
  \item Mathias, Adrian R. D., \hyperpage{15}
  \item Megill, Norman, \hyperpage{17}, \hyperpage{27}, 
		\hyperpage{31, 32}, \hyperpage{64}, \hyperpage{105}, 
		\hyperpage{171}
  \item member, \hyperpage{61}
  \item Mendelson, Elliot, \hyperpage{34}, \hyperpage{36}
  \item Meredith, C. A., \hyperpage{31}, \hyperpage{58}
  \item metalanguage, \hyperpage{2}, \hyperpage{17}, \hyperpage{29}
  \item metalogic, \hyperpage{64}, \hyperpage{126}
  \item metalogical completeness, \hyperpage{32}, \hyperpage{170, 171}
  \item Metamath, \hyperpage{vii--xi}, \hyperpage{2--4}, 
		\hyperpage{15--17}, \hyperpage{19, 20}, \hyperpage{22}, 
		\hyperpage{24}, \hyperpage{26}, \hyperpage{29--31}, 
		\hyperpage{34, 35}, \hyperpage{37, 38}, 
		\hyperpage{40, 41}, \hyperpage{45, 46}, \hyperpage{55}, 
		\hyperpage{58--61}, \hyperpage{63}, \hyperpage{83}, 
		\hyperpage{91}, \hyperpage{96--99}, \hyperpage{103}, 
		\hyperpage{106, 107}, \hyperpage{118}, 
		\hyperpage{120--123}, \hyperpage{125}
    \subitem as a formal system, \hyperpage{161}
    \subitem bugs, \hyperpage{131}
    \subitem commands, \hyperpage{129}
    \subitem installation, \hyperpage{33}
    \subitem limitations of version 0.07.30, \hyperpage{89}, 
		\hyperpage{92}, \hyperpage{119}, \hyperpage{134}, 
		\hyperpage{141}, \hyperpage{148}, \hyperpage{150}, 
		\hyperpage{155}
    \subitem memory limits, \hyperpage{134}
    \subitem memory usage, \hyperpage{135}
    \subitem representation of numbers, \hyperpage{3}
    \subitem self-description, \hyperpage{20}
    \subitem specification, \hyperpage{92}
    \subitem using as a math editor, \hyperpage{120}
  \item metamathematics, \hyperpage{30}
  \item metatheorem, \hyperpage{12}, \hyperpage{32}
  \item metavariable, \hyperpage{34}, \hyperpage{37--39}, 
		\hyperpage{60}, \hyperpage{99}, \hyperpage{101}
  \item Millay, Edna, \hyperpage{16}
  \item MIU-system, \hyperpage{29}, \hyperpage{49}, \hyperpage{142}, 
		\hyperpage{177}
  \item Miyaoka, Yoichi, \hyperpage{23}
  \item Mizar, \hyperpage{xiii}, \hyperpage{28}
  \item modal logic, \hyperpage{17}, \hyperpage{29}
  \item model theory, \hyperpage{29}
  \item modus ponens, \hyperpage{35, 36}, \hyperpage{59}, 
		\hyperpage{64}
  \item Monaco font, \hyperpage{33}
  \item Monk, J. Donald, \hyperpage{32}
  \item monospaced font, \hyperpage{33}
  \item Munkres, James R., \hyperpage{3}, \hyperpage{161}

  \indexspace

  \item natural number, \hyperpage{56}, \hyperpage{66}, \hyperpage{74}, 
		\hyperpage{80}, \hyperpage{127}
  \item negation ($\lnot$), \hyperpage{58}
  \item Nemesszeghy, E. Z., \hyperpage{125}
  \item nested block, \hyperpage{112}
  \item nesting level, \hyperpage{112}
  \item non-scoping statement, \hyperpage{112}
  \item non-trivial theory, \hyperpage{100}
  \item normal proof, \hyperpage{40}, \hyperpage{52}, \hyperpage{123}
  \item null set, \hyperpage{72}
  \item number theory, \hyperpage{2}, \hyperpage{34}

  \indexspace

  \item object, \hyperpage{61}
  \item object language, \hyperpage{17}
  \item omega ($\omega$), \hyperpage{57}, \hyperpage{66}, 
		\hyperpage{74}, \hyperpage{80}
  \item one-to-one function, \hyperpage{75}
  \item onto function, \hyperpage{75}
  \item operating system command, \hyperpage{133}
  \item operation, \hyperpage{76}, \hyperpage{80}
  \item operator precedence, \hyperpage{35}
  \item optional disjoint-variable restriction, \hyperpage{110}
  \item optional hypothesis, \hyperpage{85}, \hyperpage{110}
  \item optional variable, \hyperpage{85}, \hyperpage{110}
  \item ordered pair, \hyperpage{72}
  \item ordinal addition, \hyperpage{127}
  \item ordinal number, \hyperpage{74}
  \item ordinal predicate, \hyperpage{74}
  \item {\sc otter}, \hyperpage{27}
  \item outermost block, \hyperpage{112, 113}, \hyperpage{123}

  \indexspace

  \item pair, \hyperpage{72}
  \item parsing Metamath, \hyperpage{92}
  \item Pasch's axiom, \hyperpage{xi}, \hyperpage{23}
  \item Pavi{\v{c}}i{\'{c}}, M., \hyperpage{17}
  \item Peano's postulates, \hyperpage{66}, \hyperpage{79}
  \item Penrose, Roger, \hyperpage{26}
  \item Peterson, Jeremy George, \hyperpage{31}
  \item Pierce's axiom, \hyperpage{120}
  \item plain text, \hyperpage{33}
  \item Poincar\'{e} conjecture, \hyperpage{24}
  \item Polish notation, \hyperpage{70}
  \item pop, \hyperpage{40}, \hyperpage{115}
  \item postfix connective, \hyperpage{69}
  \item power class, \hyperpage{72}
  \item power set, \hyperpage{72}
  \item pre-statement
    \subitem in a formal system, \hyperpage{164}
  \item predicate calculus, \hyperpage{56}, \hyperpage{59}, 
		\hyperpage{168}
  \item prefix connective, \hyperpage{70}
  \item {\em Principia Mathematica}, \hyperpage{30}
  \item printable character, \hyperpage{96}
  \item printers, \hyperpage{33}
  \item proof, \hyperpage{25}, \hyperpage{35}, \hyperpage{98}, 
		\hyperpage{114}
    \subitem compressed, \hyperpage{40}, \hyperpage{52}, \hyperpage{95}, 
		\hyperpage{123, 124}, \hyperpage{159}
    \subitem Lemmon-style, \hyperpage{43}
    \subitem Metamath, \hyperpage{95}
    \subitem Metamath, description of, \hyperpage{114}
    \subitem normal, \hyperpage{40}, \hyperpage{52}, \hyperpage{123}
    \subitem tree-style, \hyperpage{43}, \hyperpage{117}
  \item Proof Assistant, \hyperpage{ix}, \hyperpage{46--48}, 
		\hyperpage{51, 52}, \hyperpage{119}, \hyperpage{124}, 
		\hyperpage{131}, \hyperpage{139}, \hyperpage{141, 142}, 
		\hyperpage{144--146}
  \item proof length, \hyperpage{15}, \hyperpage{21}, \hyperpage{89}
  \item proof scheme, \hyperpage{35}
  \item proof step, \hyperpage{37}
  \item proof theory, \hyperpage{29}
  \item proper class, \hyperpage{70}, \hyperpage{174}
  \item proper definition, \hyperpage{108}, \hyperpage{125}
  \item proper substitution, \hyperpage{32}, \hyperpage{60}, 
		\hyperpage{63}, \hyperpage{69}, \hyperpage{100}, 
		\hyperpage{170}
  \item propositional calculus, \hyperpage{31}, \hyperpage{56}, 
		\hyperpage{58}, \hyperpage{166}
  \item provable assertion, \hyperpage{39}, \hyperpage{106}
  \item provable statement
    \subitem in a formal system, \hyperpage{165}
  \item Purinton, Josh, \hyperpage{xii}, \hyperpage{165}
  \item push, \hyperpage{40}, \hyperpage{115}

  \indexspace

  \item {\sc qed} project, \hyperpage{28}
  \item qualifying expression, \hyperpage{67}
  \item quantifier theory, \hyperpage{56}
  \item quantum logic, \hyperpage{3}, \hyperpage{17}, \hyperpage{29}
  \item quantum mechanics, \hyperpage{3}
  \item Quine, Willard Van Orman, \hyperpage{17}, \hyperpage{68}, 
		\hyperpage{126}, \hyperpage{174}

  \indexspace

  \item R\^{e}go, Eduardo, \hyperpage{24}
  \item range, \hyperpage{74}
  \item rational number, \hyperpage{57}
  \item real and complex numbers, \hyperpage{3}, \hyperpage{29}
    \subitem axioms for, \hyperpage{80}
  \item real number, \hyperpage{57}
  \item recursion operator, \hyperpage{127}
  \item recursive definition, \hyperpage{112}, \hyperpage{126, 127}
  \item redeclaration of symbols, \hyperpage{39}, \hyperpage{94}, 
		\hyperpage{113}
  \item reduct
    \subitem in a formal system, \hyperpage{164}
  \item reflection principle, \hyperpage{20}
  \item relation, \hyperpage{75}
  \item restriction, \hyperpage{75}
  \item reverse Polish notation (RPN), \hyperpage{35}, \hyperpage{115}
  \item Robbins algebra, \hyperpage{26}
  \item Robbins, Herbert, \hyperpage{26}
  \item Robinson's resolution principle, \hyperpage{26}, \hyperpage{31}
  \item Robinson, T. Thacher, \hyperpage{126}
  \item Rourke, Colin, \hyperpage{24}
  \item RPN order, \hyperpage{42}, \hyperpage{110}, \hyperpage{160}
  \item RPN stack, \hyperpage{40}, \hyperpage{95}, \hyperpage{115}, 
		\hyperpage{118}
  \item Rucker, Rudy, \hyperpage{6}, \hyperpage{36}, \hyperpage{55}
  \item rule, \hyperpage{vii}, \hyperpage{17}, \hyperpage{31}, 
		\hyperpage{36}, \hyperpage{59}, \hyperpage{108}
  \item rule of generalization, \hyperpage{61}, \hyperpage{64}
  \item Russell's paradox, \hyperpage{9, 10}, \hyperpage{18}, 
		\hyperpage{78}
  \item Russell, Bertrand, \hyperpage{15}, \hyperpage{30}, 
		\hyperpage{91}

  \indexspace

  \item Schr\"{o}der-Berstein theorem, \hyperpage{23}
  \item scope, \hyperpage{85}, \hyperpage{100}, \hyperpage{113}
  \item scoping statement, \hyperpage{93}, \hyperpage{112}
  \item sentential logic, \hyperpage{56}
  \item set, \hyperpage{23}, \hyperpage{61}
  \item set difference, \hyperpage{72}
  \item set intersection, \hyperpage{56}
  \item set theory, \hyperpage{2}, \hyperpage{19}, \hyperpage{29}, 
		\hyperpage{56}, \hyperpage{61}
  \item set theory database (\texttt{set.mm}), \hyperpage{16}, 
		\hyperpage{27}, \hyperpage{29}, \hyperpage{31--33}, 
		\hyperpage{58--61}, \hyperpage{63}, \hyperpage{76}, 
		\hyperpage{83}, \hyperpage{126}, \hyperpage{148}, 
		\hyperpage{150}, \hyperpage{155}, \hyperpage{174}, 
		\hyperpage{176}
  \item set union, \hyperpage{56}
  \item Shoenfield, Joseph R., \hyperpage{30}
  \item simple declaration, \hyperpage{99}
  \item simple infinite sequence, \hyperpage{162}
  \item simple metatheorem, \hyperpage{171}
  \item singleton, \hyperpage{72}
  \item Solovay, Robert, \hyperpage{xii}
  \item Solow, Daniel, \hyperpage{8}
  \item source buffer, \hyperpage{46}, \hyperpage{138}, \hyperpage{146}
  \item source file, \hyperpage{96, 97}, \hyperpage{122}, 
		\hyperpage{134}
  \item special characters, \hyperpage{92}
  \item stack, \hyperpage{40}, \hyperpage{95}, \hyperpage{115}, 
		\hyperpage{118}
  \item Stark, Harold M, \hyperpage{23}
  \item statement
    \subitem in a formal system, \hyperpage{164}
  \item stylized epsilon ($\in$), \hyperpage{57}, \hyperpage{60}
  \item subclass, \hyperpage{72}
  \item subset, \hyperpage{62}, \hyperpage{72}
  \item substitution
    \subitem implicit, \hyperpage{77}
    \subitem proper, \hyperpage{32}, \hyperpage{60}, \hyperpage{63}, 
		\hyperpage{69}, \hyperpage{100}, \hyperpage{170}
    \subitem variable, \hyperpage{x}, \hyperpage{31}, \hyperpage{37}, 
		\hyperpage{39, 40}, \hyperpage{47}, \hyperpage{49}, 
		\hyperpage{63}, \hyperpage{86, 87}, \hyperpage{95}, 
		\hyperpage{99}, \hyperpage{115}, \hyperpage{118}, 
		\hyperpage{142}, \hyperpage{163}
  \item substitution map, \hyperpage{95}, \hyperpage{163}
  \item substitution theorem, \hyperpage{11}
  \item successor, \hyperpage{74}, \hyperpage{79}, \hyperpage{126}
  \item Swart, E. R., \hyperpage{21}
  \item symbol, \hyperpage{96}
    \subitem in a formal system, \hyperpage{162}
  \item syntax rules, \hyperpage{19}, \hyperpage{34}

  \indexspace

  \item Takeuti, Gaisi, \hyperpage{68}, \hyperpage{174}
  \item Tarski, Alfred, \hyperpage{25, 26}, \hyperpage{32}, 
		\hyperpage{162}
  \item tautology, \hyperpage{59}
  \item temporary variable, \hyperpage{48}, \hyperpage{141}, 
		\hyperpage{144}
  \item term, \hyperpage{34}, \hyperpage{37}, \hyperpage{162}
  \item text editor, \hyperpage{33}
  \item theorem, \hyperpage{vii}, \hyperpage{19}, \hyperpage{25}, 
		\hyperpage{29}, \hyperpage{31}, \hyperpage{34--36}, 
		\hyperpage{38}, \hyperpage{47}, \hyperpage{55}, 
		\hyperpage{57}, \hyperpage{59}, \hyperpage{61}, 
		\hyperpage{106}, \hyperpage{125}
  \item theorem scheme, \hyperpage{35}
  \item tilde (\texttt{\char`\~}), \hyperpage{119}, \hyperpage{121}
  \item token, \hyperpage{38}, \hyperpage{45, 46}, \hyperpage{92}, 
		\hyperpage{96--99}, \hyperpage{119--122}, 
		\hyperpage{134}
  \item topology, \hyperpage{3}
  \item transfinite recursion, \hyperpage{79}
  \item transitive class, \hyperpage{73}
  \item transitive set, \hyperpage{73}
  \item tree-style proof, \hyperpage{43}, \hyperpage{117}
  \item trusting computers, \hyperpage{21}
  \item truth table, \hyperpage{59}
  \item turnstile ({$\,\vdash$}), \hyperpage{38}, \hyperpage{76}, 
		\hyperpage{98}, \hyperpage{106}
  \item Tymoczko, Thomas, \hyperpage{17}, \hyperpage{21}
  \item type, \hyperpage{99}, \hyperpage{105}
  \item typesetting comment, \hyperpage{98}, \hyperpage{119--121}, 
		\hyperpage{148}, \hyperpage{155}

  \indexspace

  \item Ulam, Stanislaw, \hyperpage{22}
  \item unification, \hyperpage{31}, \hyperpage{47}, \hyperpage{118}
    \subitem ambiguous, \hyperpage{49}, \hyperpage{119}, 
		\hyperpage{142}, \hyperpage{146}
  \item union, \hyperpage{72, 73}, \hyperpage{175}
  \item universal class ($V$), \hyperpage{71}
  \item universal quantifier ($\forall$), \hyperpage{60}
    \subitem restricted, \hyperpage{71}
  \item universe of a formal system, \hyperpage{165}
  \item Unix file names, \hyperpage{41}, \hyperpage{129}, 
		\hyperpage{134}
  \item unordered pair, \hyperpage{72}, \hyperpage{175}
  \item unordered triple, \hyperpage{72}

  \indexspace

  \item variable, \hyperpage{x}, \hyperpage{39, 40}, \hyperpage{99}, 
		\hyperpage{101}, \hyperpage{113}
    \subitem in a formal system, \hyperpage{162}
    \subitem in ordinary mathematics, \hyperpage{101}
    \subitem in predicate calculus, \hyperpage{56}, \hyperpage{59}
    \subitem in set theory, \hyperpage{57}, \hyperpage{61}
    \subitem Metamath, \hyperpage{93}
  \item variable declaration, \hyperpage{38, 39}, \hyperpage{99}
  \item variable substitution, \hyperpage{x}, \hyperpage{31}, 
		\hyperpage{37}, \hyperpage{39, 40}, \hyperpage{47}, 
		\hyperpage{49}, \hyperpage{63}, \hyperpage{86, 87}, 
		\hyperpage{95}, \hyperpage{99}, \hyperpage{115}, 
		\hyperpage{118}, \hyperpage{142}, \hyperpage{163}
  \item variable type, \hyperpage{99}, \hyperpage{105}
  \item variable-type hypothesis, \hyperpage{39}, \hyperpage{105}
    \subitem in a formal system, \hyperpage{164}
  \item Venn diagram, \hyperpage{62}

  \indexspace

  \item Wang, Hao, \hyperpage{14}
  \item weak logic, \hyperpage{17}, \hyperpage{20}, \hyperpage{29}
  \item well-formed formula (wff), \hyperpage{vii}, \hyperpage{19, 20}, 
		\hyperpage{34}, \hyperpage{37}, \hyperpage{58}, 
		\hyperpage{60}, \hyperpage{63}, \hyperpage{83}, 
		\hyperpage{116}, \hyperpage{125}, \hyperpage{179}
  \item well-ordering, \hyperpage{73}
  \item Wen-ts{\"{u}}n, Wu, \hyperpage{25}
  \item white space, \hyperpage{92}, \hyperpage{96}, 
		\hyperpage{119--121}, \hyperpage{124}
  \item Whitehead, Alfred North, \hyperpage{4}, \hyperpage{30}
  \item Wiles, Andrew, \hyperpage{23}
  \item Williams, Anthony, \hyperpage{xiii}
  \item Word (Microsoft), \hyperpage{33}
  \item word processor, \hyperpage{33}
  \item Wos, Larry, \hyperpage{26, 27}

  \indexspace

  \item Zermelo-Fraenkel set theory, \hyperpage{9}, \hyperpage{32}, 
		\hyperpage{56}, \hyperpage{61}
  \item ZFC set theory, \hyperpage{63}, \hyperpage{173}

\end{theindex}