\begin{theindex}

  \item \texttt{\$(} and \texttt{\$)} auxiliary keywords, 
		\hyperpage{36}, \hyperpage{89}, \hyperpage{92}, 
		\hyperpage{113}
  \item \texttt{\$.}\ keyword, \hyperpage{36, 37}, \hyperpage{44}, 
		\hyperpage{91}, \hyperpage{94}
  \item \texttt{\$=} keyword, \hyperpage{37}, \hyperpage{44}, 
		\hyperpage{91}, \hyperpage{94}, \hyperpage{102}, 
		\hyperpage{109}, \hyperpage{116, 117}
  \item \texttt{\$[} and \texttt{\$]} auxiliary keywords, 
		\hyperpage{89}, \hyperpage{92}, \hyperpage{115}, 
		\hyperpage{124}
  \item \texttt{\$\char`\{} and \texttt{\$\char`\}} keywords, 
		\hyperpage{37}, \hyperpage{91}, \hyperpage{106, 107}
  \item \texttt{\$a} statement, \hyperpage{36, 37}, \hyperpage{83}, 
		\hyperpage{90, 91}, \hyperpage{93, 94}, 
		\hyperpage{100}, \hyperpage{102, 103}, 
		\hyperpage{108, 109}, \hyperpage{117}, \hyperpage{124}
  \item \texttt{\$c} statement, \hyperpage{36}, \hyperpage{89}, 
		\hyperpage{91}, \hyperpage{95}, \hyperpage{108}
  \item \texttt{\$d} statement, \hyperpage{59, 60}, \hyperpage{91}, 
		\hyperpage{95--97}, \hyperpage{100}, \hyperpage{108}, 
		\hyperpage{113}
    \subitem compound, \hyperpage{90}
    \subitem simple, \hyperpage{90}
  \item \texttt{\$e} statement, \hyperpage{36, 37}, \hyperpage{89}, 
		\hyperpage{91}, \hyperpage{94}, \hyperpage{100, 101}, 
		\hyperpage{108, 109}, \hyperpage{124}, \hyperpage{126}, 
		\hyperpage{129}, \hyperpage{131}
  \item \texttt{\$f} statement, \hyperpage{36, 37}, \hyperpage{42}, 
		\hyperpage{77}, \hyperpage{89}, \hyperpage{91}, 
		\hyperpage{94}, \hyperpage{100, 101}, 
		\hyperpage{108, 109}, \hyperpage{124, 125}, 
		\hyperpage{130, 131}
  \item \texttt{\$p} statement, \hyperpage{36, 37}, \hyperpage{90, 91}, 
		\hyperpage{94}, \hyperpage{101, 102}, 
		\hyperpage{108, 109}, \hyperpage{112}, \hyperpage{117}, 
		\hyperpage{124--126}
  \item \texttt{\$v} statement, \hyperpage{36}, \hyperpage{89}, 
		\hyperpage{91}, \hyperpage{95}, \hyperpage{108}
  \item \texttt{\char`\~} inside comments, \hyperpage{114}
  \item \texttt{?}\ in command lines, \hyperpage{43}
  \item \texttt{?}\ inside proofs, \hyperpage{44}, \hyperpage{117}, 
		\hyperpage{129}
  \item \texttt{`} inside comments, \hyperpage{114}
  \item \texttt{assign} command, \hyperpage{45}, \hyperpage{129}
  \item \texttt{beep} command, \hyperpage{123}
  \item \texttt{close log} command, \hyperpage{121}
  \item \texttt{close tex} command, \hyperpage{122}
  \item \texttt{delete} command, \hyperpage{130}
  \item \texttt{erase} command, \hyperpage{122}
  \item \texttt{exit} command, \hyperpage{42}, \hyperpage{121}
  \item \texttt{file type} command, \hyperpage{132}
  \item \texttt{help} command, \hyperpage{43}
  \item \texttt{improve} command, \hyperpage{131}
  \item \texttt{initialize} command, \hyperpage{130}
  \item \texttt{let} command, \hyperpage{129}
  \item \texttt{match} command, \hyperpage{129}
  \item \texttt{open log} command, \hyperpage{121}
  \item \texttt{open tex} command, \hyperpage{93}, \hyperpage{122}
  \item \texttt{prove} command, \hyperpage{45}, \hyperpage{127}
  \item \texttt{read} command, \hyperpage{39}, \hyperpage{43, 44}, 
		\hyperpage{78}, \hyperpage{123}
  \item \texttt{save new{\char`\_}proof} command, \hyperpage{48}, 
		\hyperpage{117}, \hyperpage{131}
  \item \texttt{save proof} command, \hyperpage{84}, \hyperpage{117}, 
		\hyperpage{127}
  \item \texttt{search} command, \hyperpage{78, 79}, \hyperpage{82}, 
		\hyperpage{125}
  \item \texttt{set echo} command, \hyperpage{123}
  \item \texttt{set empty{\char`\_}substitution} command, 
		\hyperpage{45}, \hyperpage{128}
  \item \texttt{set screen{\char`\_}width} command, \hyperpage{123}
  \item \texttt{set scroll} command, \hyperpage{123}
  \item \texttt{set search{\char`\_}limit} command, \hyperpage{128}
  \item \texttt{set unification{\char`\_}timeout} command, 
		\hyperpage{128}
  \item \texttt{show        trace{\char`\_}back} command, 
		\hyperpage{126}
  \item \texttt{show labels} command, \hyperpage{40}, \hyperpage{124}
  \item \texttt{show memory} command, \hyperpage{124}, \hyperpage{127}
  \item \texttt{show new{\char`\_}proof} command, \hyperpage{45}, 
		\hyperpage{128}
  \item \texttt{show proof} command, \hyperpage{35}, \hyperpage{40}, 
		\hyperpage{42}, \hyperpage{44}, \hyperpage{48}, 
		\hyperpage{80}, \hyperpage{112}, \hyperpage{125}
  \item \texttt{show settings} command, \hyperpage{124}
  \item \texttt{show statement} command, \hyperpage{37}, \hyperpage{40}, 
		\hyperpage{49}, \hyperpage{58}, \hyperpage{63}, 
		\hyperpage{79}, \hyperpage{124}
  \item \texttt{show trace{\char`\_}back} command, \hyperpage{16}, 
		\hyperpage{83}
  \item \texttt{show usage} command, \hyperpage{84}, \hyperpage{126}
  \item \texttt{submit} command, \hyperpage{43}, \hyperpage{122}
  \item \texttt{substitute label} command, \hyperpage{114, 115}
  \item \texttt{substitute symbol} command, \hyperpage{114}
  \item \texttt{unify} command, \hyperpage{130}
  \item \texttt{verify proofs} command, \hyperpage{78}
  \item \texttt{verify proof} command, \hyperpage{39}, \hyperpage{109}, 
		\hyperpage{117}, \hyperpage{126}
  \item \texttt{write source} command, \hyperpage{124}
  \item \texttt{write} command, \hyperpage{44}

  \indexspace

  \item abstract algebra, \hyperpage{3}
  \item abstraction class, \hyperpage{52}, \hyperpage{65}, 
		\hyperpage{151}
    \subitem of nested ordered pairs, \hyperpage{119}
    \subitem of ordered pairs, \hyperpage{68}
  \item active math symbol, \hyperpage{89}, \hyperpage{96}, 
		\hyperpage{108}
  \item active statement, \hyperpage{90}, \hyperpage{107}
  \item addition, \hyperpage{119}
    \subitem of ordinals, \hyperpage{119}
  \item ambiguous unification, \hyperpage{45}, \hyperpage{113}, 
		\hyperpage{128}, \hyperpage{131}
  \item AMSFonts, \hyperpage{32}, \hyperpage{159}
  \item analysis, \hyperpage{3}, \hyperpage{27}
  \item Anderson, Alan Ross, \hyperpage{16}
  \item Andr{\'{e}}ka, H., \hyperpage{100}, \hyperpage{142}
  \item Appel, K., \hyperpage{22}
  \item {\sc ascii}, \hyperpage{31}, \hyperpage{88}, \hyperpage{91}
  \item assertion, \hyperpage{37, 38}, \hyperpage{90}, 
		\hyperpage{101, 102}, \hyperpage{109}
    \subitem in a formal system, \hyperpage{142}
  \item assertion label, \hyperpage{38}, \hyperpage{109}, 
		\hyperpage{113}
  \item Auden, W.\ H., \hyperpage{5}
  \item Aussonderung, \hyperpage{73}
  \item automated proof verification, \hyperpage{18, 19}
  \item automated theorem proving, \hyperpage{19}, \hyperpage{24, 25}, 
		\hyperpage{56}
  \item auxiliary keyword, \hyperpage{88}, \hyperpage{92}
  \item axiom, \hyperpage{ix}, \hyperpage{2}, \hyperpage{16}, 
		\hyperpage{18}, \hyperpage{27}, \hyperpage{29}, 
		\hyperpage{32--36}, \hyperpage{51}, \hyperpage{53}, 
		\hyperpage{83}, \hyperpage{93}, \hyperpage{102, 103}, 
		\hyperpage{117, 118}
  \item Axiom of Choice, \hyperpage{16}, \hyperpage{58}, \hyperpage{61}, 
		\hyperpage{151}
  \item Axiom of Extensionality, \hyperpage{57}, \hyperpage{61, 62}, 
		\hyperpage{66}, \hyperpage{151}
  \item Axiom of Infinity, \hyperpage{30}, \hyperpage{57}, 
		\hyperpage{61}, \hyperpage{75}, \hyperpage{151}
  \item Axiom of Pairing, \hyperpage{57}, \hyperpage{73}
  \item Axiom of Power Sets, \hyperpage{57}, \hyperpage{61}, 
		\hyperpage{151}
  \item Axiom of Regularity, \hyperpage{57}, \hyperpage{61}, 
		\hyperpage{151}
  \item Axiom of Replacement, \hyperpage{58}, \hyperpage{61}, 
		\hyperpage{151}
  \item Axiom of Separation, \hyperpage{58}, \hyperpage{73}
  \item Axiom of the Null Set, \hyperpage{30}, \hyperpage{57}, 
		\hyperpage{73}
  \item Axiom of Union, \hyperpage{57}, \hyperpage{61}, \hyperpage{151}
  \item axiom scheme, \hyperpage{33}, \hyperpage{54}, \hyperpage{58}
  \item axiom vs.\ definition, \hyperpage{83}, \hyperpage{102}, 
		\hyperpage{117, 118}
  \item axiomatic assertion, \hyperpage{37}, \hyperpage{102}
  \item axiomatic statement
    \subitem in a formal system, \hyperpage{142}
  \item axioms for mathematics, \hyperpage{53}
  \item axioms in \texttt{set.mm}, \hyperpage{59}
  \item axioms of equality, \hyperpage{56}, \hyperpage{60}
  \item axioms of logic, \hyperpage{52}
  \item axioms of predicate calculus, \hyperpage{55}, \hyperpage{59}
  \item axioms of propositional calculus, \hyperpage{54}, 
		\hyperpage{59}
  \item axioms of set theory, \hyperpage{57}, \hyperpage{60}

  \indexspace

  \item Barrow, John D., \hyperpage{xii}
  \item basic keyword, \hyperpage{91}
  \item basic language, \hyperpage{91}, \hyperpage{94}, \hyperpage{109}, 
		\hyperpage{127}, \hyperpage{131}
  \item Behnke, H., \hyperpage{28}, \hyperpage{117}
  \item Bell, J. L., \hyperpage{63}
  \item Bible, \hyperpage{15}
  \item biconditional ($\leftrightarrow$), \hyperpage{60}, 
		\hyperpage{62, 63}, \hyperpage{150}
  \item binary relation, \hyperpage{68}, \hyperpage{75}
  \item Blass, Andrea, \hyperpage{29}
  \item Bledsoe, W. W., \hyperpage{25}
  \item block, \hyperpage{37}, \hyperpage{89}, \hyperpage{107}
    \subitem outermost, \hyperpage{89}
  \item Boolean algebra, \hyperpage{25}
  \item Boolos, George S., \hyperpage{14}, \hyperpage{16}
  \item bound variable, \hyperpage{30}, \hyperpage{96}
  \item Bourbaki, Nicholaus, \hyperpage{xii}, \hyperpage{14}
  \item brace notation, \hyperpage{52}
  \item Bunder, Martin, \hyperpage{16}
  \item Burali-Forti paradox, \hyperpage{73}

  \indexspace

  \item Cantor's theorem, \hyperpage{73}
  \item Cantor, Georg, \hyperpage{22}
  \item cardinal, inaccessible, \hyperpage{xiv}, \hyperpage{29}
  \item cardinal, transfinite, \hyperpage{22}
  \item cardinality, \hyperpage{22}
  \item category theory, \hyperpage{xiv}, \hyperpage{27}, 
		\hyperpage{29}
  \item certainty, \hyperpage{17}
  \item Chou, Shang-Ching, \hyperpage{24}
  \item class, \hyperpage{62}, \hyperpage{65}
    \subitem proper, \hyperpage{65}, \hyperpage{151}
  \item class abstraction, \hyperpage{52}, \hyperpage{65}, 
		\hyperpage{151}
  \item class difference, \hyperpage{67}
  \item class equality, \hyperpage{66}
  \item class membership, \hyperpage{66}
  \item class variable, \hyperpage{151}
  \item closure, \hyperpage{142}
  \item Cohen, Paul, \hyperpage{22}
  \item collection, \hyperpage{57}
  \item command keyword, \hyperpage{39}, \hyperpage{43}, \hyperpage{78}
  \item command line interface (CLI), \hyperpage{38}, \hyperpage{43}
  \item command qualifier, \hyperpage{40}
  \item comment, \hyperpage{89}, \hyperpage{113}
  \item compact proof, \hyperpage{84}
  \item composition, \hyperpage{70}
  \item compound declaration, \hyperpage{95}
  \item compressed proof, \hyperpage{37}, \hyperpage{48}, 
		\hyperpage{91}, \hyperpage{116, 117}, \hyperpage{137}
  \item computer algebra system, \hyperpage{3}, \hyperpage{19}, 
		\hyperpage{23}
  \item computer program bugs, \hyperpage{x}, \hyperpage{7, 8}, 
		\hyperpage{11}, \hyperpage{18}, \hyperpage{20}, 
		\hyperpage{23}
  \item computers and pure mathematics, \hyperpage{19}
  \item concatenation, \hyperpage{140}
  \item condensed detachment, \hyperpage{29}
    \subitem and first-order logic, \hyperpage{29}
  \item conjunction ($\wedge$), \hyperpage{60}, \hyperpage{64}, 
		\hyperpage{81}, \hyperpage{150}
  \item connective, \hyperpage{63}
  \item consistent theory, \hyperpage{17}
  \item constant, \hyperpage{xi}, \hyperpage{36}, \hyperpage{38}, 
		\hyperpage{63}, \hyperpage{89}, \hyperpage{94}, 
		\hyperpage{108}
    \subitem in a formal system, \hyperpage{140}
    \subitem in predicate calculus, \hyperpage{59}
  \item constant declaration, \hyperpage{36}, \hyperpage{95}
  \item constant-prefixed expression, \hyperpage{141}
  \item constant-variable pair, \hyperpage{141}
  \item constructive language, \hyperpage{18}
  \item constructivism, \hyperpage{16}
  \item continuum hypothesis, \hyperpage{22}
  \item Courant, Richard, \hyperpage{22}
  \item Courier font, \hyperpage{31}
  \item Coxeter, H. S. M., \hyperpage{22}
  \item cranks, \hyperpage{12}
  \item creative definition, \hyperpage{62}, \hyperpage{118}
  \item cross product, \hyperpage{69}
  \item Curry, Haskell B., \hyperpage{16}

  \indexspace

  \item database, \hyperpage{36}, \hyperpage{88}, \hyperpage{91}, 
		\hyperpage{123, 124}
  \item Davis, Phillip J., \hyperpage{1}, \hyperpage{11}, 
		\hyperpage{13}, \hyperpage{28}
  \item de Millo, Richard, \hyperpage{14}
  \item de Saint-Exupery, Antoine, \hyperpage{139}
  \item decidable theory, \hyperpage{24}
  \item decision procedure, \hyperpage{56}
  \item declaration, \hyperpage{89}
  \item deduction theorem, \hyperpage{10}
  \item definiendum, \hyperpage{62}
  \item definiens, \hyperpage{62}
  \item definition, \hyperpage{14}, \hyperpage{61}, \hyperpage{83}, 
		\hyperpage{93}, \hyperpage{102}, \hyperpage{117, 118}, 
		\hyperpage{150}
    \subitem creative, \hyperpage{62}, \hyperpage{118}
    \subitem eliminability, \hyperpage{62}
    \subitem proper, \hyperpage{103}, \hyperpage{117}
  \item disjoint sets, \hyperpage{58}
  \item disjoint variables, \hyperpage{59}, \hyperpage{96}
  \item disjoint-variable restriction, \hyperpage{90}
    \subitem in a formal system, \hyperpage{142}
  \item disjunction ($\vee$), \hyperpage{64}, \hyperpage{118}, 
		\hyperpage{150}
  \item distinct variables, \hyperpage{30}, \hyperpage{59, 60}, 
		\hyperpage{96}, \hyperpage{98}
  \item domain, \hyperpage{22}, \hyperpage{69}
  \item dummy variable, \hyperpage{80}, \hyperpage{105}
    \subitem eliminating, \hyperpage{25}, \hyperpage{100}
    \subitem in definitions, \hyperpage{62}

  \indexspace

  \item Edwards, Robert E., \hyperpage{13}
  \item effectively bound variable, \hyperpage{62}
  \item effectively not free, \hyperpage{71}, \hyperpage{147}
  \item element, \hyperpage{57}
  \item empty domain, \hyperpage{30}
  \item empty set, \hyperpage{52}, \hyperpage{67}, \hyperpage{152}
  \item empty substitution, \hyperpage{45}, \hyperpage{97}, 
		\hyperpage{128}
  \item Enderton, Herbert B., \hyperpage{16}, \hyperpage{22}, 
		\hyperpage{63}, \hyperpage{78}
  \item epsilon relation, \hyperpage{68}
  \item equality ($=$), \hyperpage{55, 56}, \hyperpage{62}
  \item errors in proofs, \hyperpage{21, 22}
  \item essential hypothesis, \hyperpage{37}, \hyperpage{100}
  \item Euclidean geometry, \hyperpage{xiii}, \hyperpage{21}, 
		\hyperpage{24}
  \item existential quantifier ($\exists$), \hyperpage{60}, 
		\hyperpage{64}, \hyperpage{150}
    \subitem restricted, \hyperpage{66}
  \item existential uniqueness quantifier ($\exists !$), \hyperpage{65}
  \item expression, \hyperpage{90}, \hyperpage{94}
    \subitem in a formal system, \hyperpage{141}
  \item extended frame, \hyperpage{105}
  \item extended language, \hyperpage{92}, \hyperpage{113}

  \indexspace

  \item family, \hyperpage{57}
  \item Feferman, Solomon, \hyperpage{xiv}
  \item Fermat's Last Theorem, \hyperpage{12}, \hyperpage{21}, 
		\hyperpage{23}
  \item file inclusion, \hyperpage{89}, \hyperpage{115}
  \item file names
    \subitem Macintosh, \hyperpage{39}, \hyperpage{116}, 
		\hyperpage{123}
    \subitem Unix, \hyperpage{39}, \hyperpage{121}
  \item finitary proof, \hyperpage{27, 28}
  \item finite $n$-termed sequence, \hyperpage{140}
  \item finite induction, \hyperpage{74}
  \item first-order logic, \hyperpage{10}, \hyperpage{19}, 
		\hyperpage{24}, \hyperpage{29}, \hyperpage{52}
    \subitem completeness, \hyperpage{11}
  \item floating hypothesis, \hyperpage{37}, \hyperpage{100}
  \item formal logic, \hyperpage{17, 18}, \hyperpage{102}
  \item formal proof, \hyperpage{xii}, \hyperpage{11, 12}, 
		\hyperpage{14}, \hyperpage{18, 19}, \hyperpage{30}, 
		\hyperpage{32}, \hyperpage{34, 35}, \hyperpage{40}, 
		\hyperpage{42}, \hyperpage{44}, \hyperpage{46}
  \item formal system, \hyperpage{ix}, \hyperpage{xi}, \hyperpage{2}, 
		\hyperpage{18}, \hyperpage{27}, \hyperpage{45}, 
		\hyperpage{128}, \hyperpage{142}, \hyperpage{155}
  \item formalism, \hyperpage{28}
  \item foundations of mathematics, \hyperpage{16}
  \item founded relation, \hyperpage{68}
  \item four-color theorem, \hyperpage{20}, \hyperpage{22}
  \item frame, \hyperpage{103}
  \item frames and scoping statements, \hyperpage{109}
  \item free logic, \hyperpage{30}
  \item free variable, \hyperpage{30}, \hyperpage{56--58}, 
		\hyperpage{96}, \hyperpage{101}, \hyperpage{147}
  \item free vs.\ bound variable, \hyperpage{96}
  \item Frege, Gottlob, \hyperpage{17}
  \item function, \hyperpage{22}, \hyperpage{70}
    \subitem in predicate calculus, \hyperpage{59}
  \item function value, \hyperpage{70}

  \indexspace

  \item G\"{o}del's incompleteness theorem, \hyperpage{xi}, 
		\hyperpage{5}, \hyperpage{14}, \hyperpage{17}
  \item gaps in proofs, \hyperpage{17}
  \item global statement, \hyperpage{108}
  \item Goodstein, R. L., \hyperpage{118}
  \item graphical user interface (GUI), \hyperpage{38}
  \item grave accent (\texttt{`}), \hyperpage{114}
  \item Grothendieck, Alexander, \hyperpage{xiv}
  \item group theory, \hyperpage{2}
  \item Guillen, Michael, \hyperpage{5}

  \indexspace

  \item Haken, W., \hyperpage{22}
  \item Halmos, Paul, \hyperpage{19}
  \item Hamilton, Alan G., \hyperpage{56}, \hyperpage{80}
  \item Hardy, G. H., \hyperpage{88}
  \item Harrison, John, \hyperpage{19}, \hyperpage{24}
  \item Herrlich, Horst, \hyperpage{29}
  \item hierarchy, \hyperpage{12}, \hyperpage{14}, \hyperpage{18}, 
		\hyperpage{24}, \hyperpage{83}
  \item higher-order logic, \hyperpage{19}, \hyperpage{27}
  \item Hilbert, David, \hyperpage{14, 15}, \hyperpage{22}, 
		\hyperpage{27, 28}
  \item Hindley, J. Roger, \hyperpage{29}
  \item Hofstadter, Douglas R., \hyperpage{27}, \hyperpage{34}, 
		\hyperpage{157}
  \item {\sc hol}, \hyperpage{26}
  \item Hume, David, \hyperpage{21}
  \item Huntington, E. V., \hyperpage{25}
  \item hypothesis, \hyperpage{37}, \hyperpage{89}, \hyperpage{100}
  \item hypothesis association, \hyperpage{112}
  \item hypothesis label, \hyperpage{37}, \hyperpage{109}

  \indexspace

  \item iff, \hyperpage{68}
  \item image, \hyperpage{70}
  \item implication ($\rightarrow$), \hyperpage{32}, \hyperpage{54}
  \item implicit axiom, \hyperpage{30}
  \item included file, \hyperpage{89}, \hyperpage{115}
  \item individual metavariable, \hyperpage{145}
  \item individual variable, \hyperpage{55}
  \item inference, \hyperpage{101}, \hyperpage{145}
  \item inference rule, \hyperpage{33}
  \item infinite set, \hyperpage{52}
  \item infinity, \hyperpage{22}
  \item infix connective, \hyperpage{65}
  \item informal proof, \hyperpage{12}, \hyperpage{14}
  \item integer, \hyperpage{52, 53}
  \item intersection, \hyperpage{67, 68}
  \item intuitionism, \hyperpage{16}, \hyperpage{27}, \hyperpage{118}
  \item Isabelle, \hyperpage{25}

  \indexspace

  \item Kalman, J. A., \hyperpage{29}
  \item Kempe, A. B., \hyperpage{22}
  \item keyword, \hyperpage{36}, \hyperpage{88}, \hyperpage{91--93}
  \item Kline, Morris, \hyperpage{17}, \hyperpage{28}
  \item Koch, K., \hyperpage{22}
  \item Kronecker, Leopold, \hyperpage{15}
  \item Kuratowski, Kazimierz, \hyperpage{67}

  \indexspace

  \item label, \hyperpage{37}, \hyperpage{40}, \hyperpage{43}, 
		\hyperpage{88}, \hyperpage{91}, \hyperpage{94}, 
		\hyperpage{98}, \hyperpage{101--103}, \hyperpage{109}, 
		\hyperpage{112}
  \item label declaration, \hyperpage{94}
  \item label mode, \hyperpage{114, 115}
  \item label reference, \hyperpage{94}, \hyperpage{109}
  \item label sequence, \hyperpage{94}, \hyperpage{109}
  \item labels in \texttt{set.mm}, \hyperpage{83}
  \item Landau, Edmund, \hyperpage{5}
  \item {\LaTeX}, \hyperpage{xi}, \hyperpage{32}, \hyperpage{75}, 
		\hyperpage{79}, \hyperpage{93}, \hyperpage{114, 115}, 
		\hyperpage{122}, \hyperpage{124, 125}, \hyperpage{159}
    \subitem characters per line, \hyperpage{123}
  \item \LaTeX\ definitions, \hyperpage{133}
  \item {\sc lcf}, \hyperpage{26}
  \item Le\'{s}niewski, S., \hyperpage{118}
  \item Leblanc, Hugues, \hyperpage{30}
  \item Lejewski, Czeslaw, \hyperpage{118}
  \item Lemmon-style proof, \hyperpage{41}
  \item length of a sequence ({$|\ |$}), \hyperpage{140}
  \item limit ordinal, \hyperpage{69}
  \item local label, \hyperpage{84}
  \item local variable, \hyperpage{108}
  \item logic, \hyperpage{2}
  \item logical equivalence ($\leftrightarrow$), \hyperpage{60}, 
		\hyperpage{62, 63}, \hyperpage{150}
  \item logical hypothesis, \hyperpage{37}, \hyperpage{100}
    \subitem in a formal system, \hyperpage{142}
  \item logical {\sc and} ($\wedge$), \hyperpage{60}, \hyperpage{64}, 
		\hyperpage{81}
  \item logical {\sc or} ($\vee$), \hyperpage{64}

  \indexspace

  \item Mac Lane, Saunders, \hyperpage{xiv}
  \item Macintosh file names, \hyperpage{39}, \hyperpage{116}, 
		\hyperpage{123}
  \item {\sc macsyma}, \hyperpage{3}
  \item mandatory \texttt{\$d} statement, \hyperpage{113}
  \item mandatory disjoint-variable restriction, \hyperpage{90}
    \subitem in a formal system, \hyperpage{142}
  \item mandatory hypothesis, \hyperpage{37}, \hyperpage{40}, 
		\hyperpage{49}, \hyperpage{90}, \hyperpage{105}, 
		\hyperpage{109, 110}, \hyperpage{112, 113}, 
		\hyperpage{116}
    \subitem in a formal system, \hyperpage{142}
  \item mandatory variable, \hyperpage{90}, \hyperpage{104}
  \item mandatory variable-type hypothesis
    \subitem in a formal system, \hyperpage{142}
  \item Maple, \hyperpage{3}, \hyperpage{23}
  \item mapping, \hyperpage{22}
  \item math mode, \hyperpage{114}
  \item math symbol, \hyperpage{36, 37}, \hyperpage{41}, \hyperpage{43}, 
		\hyperpage{55}, \hyperpage{88}, \hyperpage{91}, 
		\hyperpage{93--95}, \hyperpage{108}, \hyperpage{114}
  \item Mathematica, \hyperpage{3}, \hyperpage{23}
  \item Mathematica and proofs, \hyperpage{23}
  \item mathematical induction, \hyperpage{74}
  \item Mathias, Adrian R. D., \hyperpage{14}
  \item Megill, Norman, \hyperpage{16}, \hyperpage{25}, \hyperpage{29}, 
		\hyperpage{59}, \hyperpage{100}, \hyperpage{148}
  \item member, \hyperpage{57}
  \item Mendelson, Elliot, \hyperpage{32}, \hyperpage{34}
  \item Meredith, C. A., \hyperpage{29}, \hyperpage{54}
  \item metalanguage, \hyperpage{2}, \hyperpage{16}, \hyperpage{27}
  \item metalogic, \hyperpage{59}, \hyperpage{119}
  \item metalogical completeness, \hyperpage{29}, \hyperpage{148}
  \item Metamath, \hyperpage{ix--xi}, \hyperpage{xiii}, 
		\hyperpage{2, 3}, \hyperpage{14--16}, \hyperpage{18}, 
		\hyperpage{20}, \hyperpage{22, 23}, \hyperpage{25}, 
		\hyperpage{27--29}, \hyperpage{32, 33}, 
		\hyperpage{35, 36}, \hyperpage{38, 39}, 
		\hyperpage{43, 44}, \hyperpage{51}, \hyperpage{54--58}, 
		\hyperpage{78}, \hyperpage{87}, \hyperpage{91--94}, 
		\hyperpage{98}, \hyperpage{101, 102}, 
		\hyperpage{113--117}
    \subitem as a formal system, \hyperpage{139}
    \subitem bugs, \hyperpage{121}
    \subitem commands, \hyperpage{121}
    \subitem installation, \hyperpage{31}
    \subitem limitations of version 0.06, \hyperpage{38, 39}, 
		\hyperpage{47}, \hyperpage{78}, \hyperpage{84}, 
		\hyperpage{88}, \hyperpage{114, 115}, \hyperpage{124}, 
		\hyperpage{127}, \hyperpage{133}
    \subitem memory limits, \hyperpage{132}
    \subitem memory usage, \hyperpage{124}, \hyperpage{127}
    \subitem representation of numbers, \hyperpage{3}
    \subitem self-description, \hyperpage{19}
    \subitem specification, \hyperpage{88}
    \subitem using as a math editor, \hyperpage{115}
  \item metamathematics, \hyperpage{28}
  \item metatheorem, \hyperpage{11}, \hyperpage{29}
  \item metavariable, \hyperpage{32}, \hyperpage{35, 36}, 
		\hyperpage{55}, \hyperpage{94}, \hyperpage{97}
  \item Millay, Edna, \hyperpage{15}
  \item MIU-system, \hyperpage{27}, \hyperpage{128}, \hyperpage{155}
  \item Miyaoka, Yoichi, \hyperpage{21}
  \item Mizar, \hyperpage{xiv}, \hyperpage{26}
  \item modal logic, \hyperpage{16}, \hyperpage{27}
  \item model theory, \hyperpage{28}
  \item modus ponens, \hyperpage{33, 34}, \hyperpage{54}, 
		\hyperpage{59}
  \item Monaco font, \hyperpage{31}
  \item Monk, J. Donald, \hyperpage{29}
  \item monospaced font, \hyperpage{31}
  \item mouse, \hyperpage{38}
  \item Munkres, James R., \hyperpage{3}, \hyperpage{139}

  \indexspace

  \item natural number, \hyperpage{52}, \hyperpage{61}, \hyperpage{69}, 
		\hyperpage{75}, \hyperpage{119}
  \item negation ($\lnot$), \hyperpage{54}
  \item Nemesszeghy, E. Z., \hyperpage{118}
  \item nested block, \hyperpage{107}
  \item nesting level, \hyperpage{107}
  \item non-scoping statement, \hyperpage{107}
  \item non-trivial theory, \hyperpage{96}
  \item normal proof, \hyperpage{37}, \hyperpage{48}, \hyperpage{116}
  \item null set, \hyperpage{67}
  \item number theory, \hyperpage{2}, \hyperpage{32}

  \indexspace

  \item object, \hyperpage{57}
  \item object language, \hyperpage{16}
  \item omega ($\omega$), \hyperpage{52}, \hyperpage{61}, 
		\hyperpage{69}, \hyperpage{75}
  \item one-to-one function, \hyperpage{70}
  \item onto function, \hyperpage{70}
  \item operating system command, \hyperpage{122}
  \item operation, \hyperpage{71}, \hyperpage{75}
  \item operator precedence, \hyperpage{32}
  \item optional disjoint-variable restriction, \hyperpage{105}
  \item optional hypothesis, \hyperpage{80}, \hyperpage{105}
  \item optional variable, \hyperpage{80}, \hyperpage{105}
  \item ordered pair, \hyperpage{67}
  \item ordinal addition, \hyperpage{119}
  \item ordinal number, \hyperpage{69}
  \item ordinal predicate, \hyperpage{69}
  \item {\sc otter}, \hyperpage{25}
  \item outermost block, \hyperpage{107, 108}, \hyperpage{116}

  \indexspace

  \item pair, \hyperpage{67}
  \item parsing Metamath, \hyperpage{88}
  \item Pasch's axiom, \hyperpage{xiii}, \hyperpage{21}
  \item Pavi{\v{c}}i{\'{c}}, M., \hyperpage{16}
  \item Peano's postulates, \hyperpage{61}, \hyperpage{74}
  \item Penrose, Roger, \hyperpage{24}
  \item Peterson, Jeremy George, \hyperpage{29}
  \item Pierce's axiom, \hyperpage{114}
  \item plain text, \hyperpage{31}
  \item Poincar\'{e} conjecture, \hyperpage{22}
  \item Polish notation, \hyperpage{65}
  \item pop, \hyperpage{38}, \hyperpage{110}
  \item postfix connective, \hyperpage{65}
  \item power class, \hyperpage{67}
  \item power set, \hyperpage{67}
  \item pre-statement
    \subitem in a formal system, \hyperpage{141}
  \item predicate calculus, \hyperpage{52}, \hyperpage{55}, 
		\hyperpage{145}
  \item prefix connective, \hyperpage{65}
  \item {\em Principia Mathematica}, \hyperpage{28}
  \item printable character, \hyperpage{91}
  \item printers, \hyperpage{31}
  \item proof, \hyperpage{23}, \hyperpage{33}, \hyperpage{94}, 
		\hyperpage{109}
    \subitem compressed, \hyperpage{37}, \hyperpage{48}, \hyperpage{91}, 
		\hyperpage{116, 117}, \hyperpage{137}
    \subitem Lemmon-style, \hyperpage{41}
    \subitem Metamath, \hyperpage{90}
    \subitem Metamath, description of, \hyperpage{109}
    \subitem normal, \hyperpage{37}, \hyperpage{48}, \hyperpage{116}
    \subitem tree-style, \hyperpage{41}, \hyperpage{112}
  \item Proof Assistant, \hyperpage{xi}, \hyperpage{44--49}, 
		\hyperpage{113}, \hyperpage{117}, \hyperpage{121}, 
		\hyperpage{127--132}
  \item proof length, \hyperpage{14}, \hyperpage{20}, \hyperpage{83}
  \item proof scheme, \hyperpage{33}
  \item proof step, \hyperpage{35}
  \item proof theory, \hyperpage{28}
  \item proper class, \hyperpage{65}, \hyperpage{151}
  \item proper definition, \hyperpage{103}, \hyperpage{117}
  \item proper substitution, \hyperpage{30}, \hyperpage{56}, 
		\hyperpage{58}, \hyperpage{64}, \hyperpage{96}, 
		\hyperpage{147}
  \item propositional calculus, \hyperpage{29}, \hyperpage{51, 52}, 
		\hyperpage{54}, \hyperpage{144}
  \item provable assertion, \hyperpage{37}, \hyperpage{102}
  \item provable statement
    \subitem in a formal system, \hyperpage{143}
  \item push, \hyperpage{37}, \hyperpage{110}

  \indexspace

  \item {\sc qed} project, \hyperpage{26}
  \item qualifying expression, \hyperpage{62}
  \item quantifier theory, \hyperpage{52}
  \item quantum logic, \hyperpage{3}, \hyperpage{16}, \hyperpage{27}
  \item quantum mechanics, \hyperpage{3}
  \item Quine, Willard Van Orman, \hyperpage{16}, \hyperpage{63}, 
		\hyperpage{119}, \hyperpage{151}

  \indexspace

  \item R\^{e}go, Eduardo, \hyperpage{22}
  \item range, \hyperpage{69}
  \item rational number, \hyperpage{53}
  \item real and complex numbers, \hyperpage{3}, \hyperpage{27}
    \subitem axioms for, \hyperpage{75}
  \item real number, \hyperpage{53}
  \item recursion operator, \hyperpage{119}
  \item recursive definition, \hyperpage{107}, \hyperpage{119}
  \item redeclaration of symbols, \hyperpage{36}, \hyperpage{89}, 
		\hyperpage{108}
  \item reduct
    \subitem in a formal system, \hyperpage{142}
  \item reflection principle, \hyperpage{19}
  \item relation, \hyperpage{70}
  \item restriction, \hyperpage{69}
  \item reverse Polish notation (RPN), \hyperpage{33}, \hyperpage{109}
  \item Robbins algebra, \hyperpage{25}
  \item Robbins, Herbert, \hyperpage{25}
  \item Robinson's resolution principle, \hyperpage{24}, \hyperpage{29}
  \item Robinson, T. Thacher, \hyperpage{119}
  \item Rourke, Colin, \hyperpage{22}
  \item RPN order, \hyperpage{40}, \hyperpage{105}, \hyperpage{138}
  \item RPN stack, \hyperpage{37}, \hyperpage{90}, \hyperpage{110}, 
		\hyperpage{113}
  \item Rucker, Rudy, \hyperpage{5}, \hyperpage{34}, \hyperpage{51}
  \item rule, \hyperpage{ix}, \hyperpage{16}, \hyperpage{29}, 
		\hyperpage{34}, \hyperpage{54}, \hyperpage{103}
  \item rule of generalization, \hyperpage{56}, \hyperpage{60}
  \item Russell's paradox, \hyperpage{9}, \hyperpage{17}, 
		\hyperpage{73}
  \item Russell, Bertrand, \hyperpage{14}, \hyperpage{28}, 
		\hyperpage{87}

  \indexspace

  \item Schr\"{o}der-Berstein theorem, \hyperpage{22}
  \item scope, \hyperpage{80}, \hyperpage{96}, \hyperpage{108}
  \item scoping statement, \hyperpage{89}, \hyperpage{107}
  \item sentential logic, \hyperpage{51}
  \item set, \hyperpage{22}, \hyperpage{57}
  \item set difference, \hyperpage{67}
  \item set intersection, \hyperpage{52}
  \item set theory, \hyperpage{2}, \hyperpage{18}, \hyperpage{27}, 
		\hyperpage{52}, \hyperpage{57}
  \item set theory database (\texttt{set.mm}), \hyperpage{25}, 
		\hyperpage{27}, \hyperpage{29--31}, \hyperpage{54--58}, 
		\hyperpage{71}, \hyperpage{77, 78}, \hyperpage{118}
  \item set union, \hyperpage{52}
  \item Shoenfield, Joseph R., \hyperpage{28}
  \item simple declaration, \hyperpage{95}
  \item simple infinite sequence, \hyperpage{140}
  \item simple metatheorem, \hyperpage{148}
  \item singleton, \hyperpage{67}
  \item Solovay, Bob, \hyperpage{xiv}
  \item Solow, Daniel, \hyperpage{8}
  \item source buffer, \hyperpage{44}, \hyperpage{127}, \hyperpage{131}
  \item source file, \hyperpage{91, 92}, \hyperpage{115}, 
		\hyperpage{124}
  \item special characters, \hyperpage{88}
  \item stack, \hyperpage{37}, \hyperpage{90}, \hyperpage{110}, 
		\hyperpage{113}
  \item Stark, Harold M, \hyperpage{21}
  \item statement
    \subitem in a formal system, \hyperpage{142}
  \item stylized epsilon ($\in$), \hyperpage{52}, \hyperpage{55}
  \item subclass, \hyperpage{67}
  \item subset, \hyperpage{57}, \hyperpage{67}
  \item substitution
    \subitem implicit, \hyperpage{72}
    \subitem proper, \hyperpage{30}, \hyperpage{56}, \hyperpage{58}, 
		\hyperpage{64}, \hyperpage{96}, \hyperpage{147}
    \subitem variable, \hyperpage{xi}, \hyperpage{29}, 
		\hyperpage{35, 36}, \hyperpage{38}, \hyperpage{44, 45}, 
		\hyperpage{58, 59}, \hyperpage{80, 81}, \hyperpage{90}, 
		\hyperpage{94}, \hyperpage{110}, \hyperpage{113}, 
		\hyperpage{128}, \hyperpage{141}
  \item substitution map, \hyperpage{90}, \hyperpage{141}
  \item substitution theorem, \hyperpage{11}
  \item successor, \hyperpage{69}, \hyperpage{74}, \hyperpage{119}
  \item Swart, E. R., \hyperpage{20}
  \item symbol, \hyperpage{91}
    \subitem in a formal system, \hyperpage{140}
  \item syntax rules, \hyperpage{18}, \hyperpage{32}

  \indexspace

  \item Takeuti, Gaisi, \hyperpage{63}, \hyperpage{151}
  \item Tarski, Alfred, \hyperpage{24, 25}, \hyperpage{29}, 
		\hyperpage{140}
  \item tautology, \hyperpage{55}
  \item temporary variable, \hyperpage{46}, \hyperpage{128, 129}
  \item term, \hyperpage{32}, \hyperpage{35}, \hyperpage{140}
  \item text editor, \hyperpage{31}
  \item theorem, \hyperpage{ix}, \hyperpage{18}, \hyperpage{23}, 
		\hyperpage{27}, \hyperpage{29}, \hyperpage{32--34}, 
		\hyperpage{36}, \hyperpage{44}, \hyperpage{51}, 
		\hyperpage{53, 54}, \hyperpage{56}, \hyperpage{101}, 
		\hyperpage{117}
  \item theorem scheme, \hyperpage{33}
  \item tilde (\texttt{\char`\~}), \hyperpage{114, 115}
  \item token, \hyperpage{36}, \hyperpage{43, 44}, \hyperpage{88}, 
		\hyperpage{91}, \hyperpage{93--95}, 
		\hyperpage{113--115}, \hyperpage{132}
  \item topology, \hyperpage{3}
  \item transfinite induction, \hyperpage{74}
  \item transfinite recursion, \hyperpage{74}
  \item transitive class, \hyperpage{68}
  \item transitive set, \hyperpage{68}
  \item tree-style proof, \hyperpage{41}, \hyperpage{112}
  \item trusting computers, \hyperpage{20}
  \item truth table, \hyperpage{55}
  \item turnstile ({$\,\vdash$}), \hyperpage{36}, \hyperpage{71}, 
		\hyperpage{93}, \hyperpage{101}
  \item Tymoczko, Thomas, \hyperpage{16}, \hyperpage{20}
  \item type, \hyperpage{94}, \hyperpage{101}

  \indexspace

  \item Ulam, Stanislaw, \hyperpage{21}
  \item unification, \hyperpage{29}, \hyperpage{44}, \hyperpage{113}
    \subitem ambiguous, \hyperpage{45}, \hyperpage{113}, 
		\hyperpage{128}, \hyperpage{131}
  \item union, \hyperpage{67, 68}, \hyperpage{152}
  \item universal class ($V$), \hyperpage{66}
  \item universal quantifier ($\forall$), \hyperpage{55}
    \subitem restricted, \hyperpage{66}
  \item universe of a formal system, \hyperpage{143}
  \item Unix file names, \hyperpage{39}, \hyperpage{121}
  \item unordered pair, \hyperpage{67}, \hyperpage{152}
  \item unordered triple, \hyperpage{67}

  \indexspace

  \item variable, \hyperpage{xi}, \hyperpage{36}, \hyperpage{38}, 
		\hyperpage{94}, \hyperpage{97}, \hyperpage{108}
    \subitem in a formal system, \hyperpage{140}
    \subitem in ordinary mathematics, \hyperpage{97}
    \subitem in predicate calculus, \hyperpage{52}, \hyperpage{55}
    \subitem in set theory, \hyperpage{53}, \hyperpage{57}
    \subitem Metamath, \hyperpage{89}
  \item variable declaration, \hyperpage{36}, \hyperpage{95}
  \item variable substitution, \hyperpage{xi}, \hyperpage{29}, 
		\hyperpage{35, 36}, \hyperpage{38}, \hyperpage{44, 45}, 
		\hyperpage{58, 59}, \hyperpage{80, 81}, \hyperpage{90}, 
		\hyperpage{94}, \hyperpage{110}, \hyperpage{113}, 
		\hyperpage{128}, \hyperpage{141}
  \item variable type, \hyperpage{94}, \hyperpage{101}
  \item variable-type hypothesis, \hyperpage{37}, \hyperpage{100}
    \subitem in a formal system, \hyperpage{142}
  \item Venn diagram, \hyperpage{57}

  \indexspace

  \item Wang, Hao, \hyperpage{13}
  \item weak logic, \hyperpage{16}, \hyperpage{19}, \hyperpage{27}
  \item well-formed formula (wff), \hyperpage{ix}, \hyperpage{18, 19}, 
		\hyperpage{32}, \hyperpage{35}, \hyperpage{54--56}, 
		\hyperpage{58}, \hyperpage{77}, \hyperpage{110}, 
		\hyperpage{118}, \hyperpage{157}
  \item well-ordering, \hyperpage{68}
  \item Wen-ts{\"{u}}n, Wu, \hyperpage{24}
  \item white space, \hyperpage{88}, \hyperpage{91}, 
		\hyperpage{113--116}
  \item Whitehead, Alfred North, \hyperpage{4}, \hyperpage{28}
  \item Wiles, Andrew, \hyperpage{21}
  \item Word (Microsoft), \hyperpage{31}
  \item word processor, \hyperpage{31}
  \item Wos, Larry, \hyperpage{25}

  \indexspace

  \item Zermelo-Fraenkel set theory, \hyperpage{9}, \hyperpage{30}, 
		\hyperpage{52}, \hyperpage{57}
  \item ZFC set theory, \hyperpage{58}, \hyperpage{150}

\end{theindex}