\indexentry{Metamath|hyperpage}{ix}
\indexentry{formal system|hyperpage}{ix}
\indexentry{theorem|hyperpage}{ix}
\indexentry{axiom|hyperpage}{ix}
\indexentry{rule|hyperpage}{ix}
\indexentry{well-formed formula (wff)|hyperpage}{ix}
\indexentry{Metamath|hyperpage}{x}
\indexentry{computer program bugs|hyperpage}{x}
\indexentry{computer program bugs|hyperpage}{x}
\indexentry{G\"{o}del's incompleteness theorem|hyperpage}{xi}
\indexentry{formal system|hyperpage}{xi}
\indexentry{Proof Assistant|hyperpage}{xi}
\indexentry{Metamath|hyperpage}{xi}
\indexentry{latex@{\LaTeX}|hyperpage}{xi}
\indexentry{Metamath|hyperpage}{xi}
\indexentry{Metamath|hyperpage}{xi}
\indexentry{constant|hyperpage}{xi}
\indexentry{variable|hyperpage}{xi}
\indexentry{substitution!variable|hyperpage}{xi}
\indexentry{variable substitution|hyperpage}{xi}
\indexentry{formal proof|hyperpage}{xii}
\indexentry{Bourbaki, Nicholaus|hyperpage}{xii}
\indexentry{Barrow, John D.|hyperpage}{xii}
\indexentry{Metamath|hyperpage}{xiii}
\indexentry{Euclidean geometry|hyperpage}{xiii}
\indexentry{Pasch's axiom|hyperpage}{xiii}
\indexentry{Solovay, Bob|hyperpage}{xiv}
\indexentry{category theory|hyperpage}{xiv}
\indexentry{cardinal, inaccessible|hyperpage}{xiv}
\indexentry{Grothendieck, Alexander|hyperpage}{xiv}
\indexentry{Mac Lane, Saunders|hyperpage}{xiv}
\indexentry{Feferman, Solomon|hyperpage}{xiv}
\indexentry{Mizar|hyperpage}{xiv}
\indexentry{Davis, Phillip J.|hyperpage}{1}
\indexentry{Metamath|hyperpage}{2}
\indexentry{Metamath|hyperpage}{2}
\indexentry{formal system|hyperpage}{2}
\indexentry{metalanguage|hyperpage}{2}
\indexentry{axiom|hyperpage}{2}
\indexentry{logic|hyperpage}{2}
\indexentry{set theory|hyperpage}{2}
\indexentry{number theory|hyperpage}{2}
\indexentry{group theory|hyperpage}{2}
\indexentry{abstract algebra|hyperpage}{3}
\indexentry{analysis|hyperpage}{3}
\indexentry{real and complex numbers|hyperpage}{3}
\indexentry{topology|hyperpage}{3}
\indexentry{quantum logic|hyperpage}{3}
\indexentry{quantum mechanics|hyperpage}{3}
\indexentry{Metamath|hyperpage}{3}
\indexentry{Metamath!representation of numbers|hyperpage}{3}
\indexentry{computer algebra system|hyperpage}{3}
\indexentry{macsyma@{\sc macsyma}|hyperpage}{3}
\indexentry{Mathematica|hyperpage}{3}
\indexentry{Maple|hyperpage}{3}
\indexentry{Metamath|hyperpage}{3}
\indexentry{Munkres, James R.|hyperpage}{3}
\indexentry{Whitehead, Alfred North|hyperpage}{4}
\indexentry{Landau, Edmund|hyperpage}{5}
\indexentry{Auden, W.\ H.|hyperpage}{5}
\indexentry{Guillen, Michael|hyperpage}{5}
\indexentry{G\"{o}del's incompleteness theorem|hyperpage}{5}
\indexentry{Rucker, Rudy|hyperpage}{5}
\indexentry{computer program bugs|hyperpage}{7}
\indexentry{Solow, Daniel|hyperpage}{8}
\indexentry{computer program bugs|hyperpage}{8}
\indexentry{Zermelo-Fraenkel set theory|hyperpage}{9}
\indexentry{Russell's paradox|hyperpage}{9}
\indexentry{Russell's paradox|hyperpage}{9}
\indexentry{first-order logic|hyperpage}{10}
\indexentry{deduction theorem|hyperpage}{10}
\indexentry{substitution theorem|hyperpage}{11}
\indexentry{first-order logic!completeness|hyperpage}{11}
\indexentry{formal proof|hyperpage}{11}
\indexentry{metatheorem|hyperpage}{11}
\indexentry{computer program bugs|hyperpage}{11}
\indexentry{Davis, Phillip J.|hyperpage}{11}
\indexentry{informal proof|hyperpage}{12}
\indexentry{formal proof|hyperpage}{12}
\indexentry{hierarchy|hyperpage}{12}
\indexentry{cranks|hyperpage}{12}
\indexentry{Fermat's Last Theorem|hyperpage}{12}
\indexentry{Edwards, Robert E.|hyperpage}{13}
\indexentry{Davis, Phillip J.|hyperpage}{13}
\indexentry{Wang, Hao|hyperpage}{13}
\indexentry{de Millo, Richard|hyperpage}{14}
\indexentry{Metamath|hyperpage}{14}
\indexentry{formal proof|hyperpage}{14}
\indexentry{informal proof|hyperpage}{14}
\indexentry{proof length|hyperpage}{14}
\indexentry{definition|hyperpage}{14}
\indexentry{G\"{o}del's incompleteness theorem|hyperpage}{14}
\indexentry{Boolos, George S.|hyperpage}{14}
\indexentry{Mathias, Adrian R. D.|hyperpage}{14}
\indexentry{Bourbaki, Nicholaus|hyperpage}{14}
\indexentry{hierarchy|hyperpage}{14}
\indexentry{Metamath|hyperpage}{14}
\indexentry{Hilbert, David|hyperpage}{14}
\indexentry{Russell, Bertrand|hyperpage}{14}
\indexentry{Millay, Edna|hyperpage}{15}
\indexentry{Metamath|hyperpage}{15}
\indexentry{Bible|hyperpage}{15}
\indexentry{Kronecker, Leopold|hyperpage}{15}
\indexentry{Hilbert, David|hyperpage}{15}
\indexentry{Metamath|hyperpage}{15}
\indexentry{Metamath|hyperpage}{16}
\indexentry{foundations of mathematics|hyperpage}{16}
\indexentry{metalanguage|hyperpage}{16}
\indexentry{object language|hyperpage}{16}
\indexentry{weak logic|hyperpage}{16}
\indexentry{Anderson, Alan Ross|hyperpage}{16}
\indexentry{Megill, Norman|hyperpage}{16}
\indexentry{Bunder, Martin|hyperpage}{16}
\indexentry{modal logic|hyperpage}{16}
\indexentry{Boolos, George S.|hyperpage}{16}
\indexentry{quantum logic|hyperpage}{16}
\indexentry{Pavi{\v{c}}i{\'{c}}, M.|hyperpage}{16}
\indexentry{Metamath|hyperpage}{16}
\indexentry{intuitionism|hyperpage}{16}
\indexentry{constructivism|hyperpage}{16}
\indexentry{axiom|hyperpage}{16}
\indexentry{rule|hyperpage}{16}
\indexentry{intuitionism|hyperpage}{16}
\indexentry{\texttt{show trace{\char`\_}back} command|hyperpage}{16}
\indexentry{Tymoczko, Thomas|hyperpage}{16}
\indexentry{Axiom of Choice|hyperpage}{16}
\indexentry{Enderton, Herbert B.|hyperpage}{16}
\indexentry{Quine, Willard Van Orman|hyperpage}{16}
\indexentry{Curry, Haskell B.|hyperpage}{16}
\indexentry{Kline, Morris|hyperpage}{17}
\indexentry{G\"{o}del's incompleteness theorem|hyperpage}{17}
\indexentry{consistent theory|hyperpage}{17}
\indexentry{Russell's paradox|hyperpage}{17}
\indexentry{Frege, Gottlob|hyperpage}{17}
\indexentry{Kline, Morris|hyperpage}{17}
\indexentry{certainty|hyperpage}{17}
\indexentry{formal logic|hyperpage}{17}
\indexentry{gaps in proofs|hyperpage}{17}
\indexentry{formal proof|hyperpage}{18}
\indexentry{set theory|hyperpage}{18}
\indexentry{hierarchy|hyperpage}{18}
\indexentry{formal logic|hyperpage}{18}
\indexentry{formal proof|hyperpage}{18}
\indexentry{well-formed formula (wff)|hyperpage}{18}
\indexentry{automated proof verification|hyperpage}{18}
\indexentry{computer program bugs|hyperpage}{18}
\indexentry{Metamath|hyperpage}{18}
\indexentry{constructive language|hyperpage}{18}
\indexentry{formal system|hyperpage}{18}
\indexentry{syntax rules|hyperpage}{18}
\indexentry{axiom|hyperpage}{18}
\indexentry{theorem|hyperpage}{18}
\indexentry{Metamath|hyperpage}{18}
\indexentry{formal system|hyperpage}{18}
\indexentry{first-order logic|hyperpage}{19}
\indexentry{higher-order logic|hyperpage}{19}
\indexentry{weak logic|hyperpage}{19}
\indexentry{well-formed formula (wff)|hyperpage}{19}
\indexentry{Metamath!self-description|hyperpage}{19}
\indexentry{Harrison, John|hyperpage}{19}
\indexentry{reflection principle|hyperpage}{19}
\indexentry{formal proof|hyperpage}{19}
\indexentry{automated proof verification|hyperpage}{19}
\indexentry{Halmos, Paul|hyperpage}{19}
\indexentry{computers and pure mathematics|hyperpage}{19}
\indexentry{computer algebra system|hyperpage}{19}
\indexentry{automated theorem proving|hyperpage}{19}
\indexentry{computer program bugs|hyperpage}{20}
\indexentry{Tymoczko, Thomas|hyperpage}{20}
\indexentry{four-color theorem|hyperpage}{20}
\indexentry{proof length|hyperpage}{20}
\indexentry{Swart, E. R.|hyperpage}{20}
\indexentry{trusting computers|hyperpage}{20}
\indexentry{Metamath|hyperpage}{20}
\indexentry{computer program bugs|hyperpage}{20}
\indexentry{Hume, David|hyperpage}{21}
\indexentry{Ulam, Stanislaw|hyperpage}{21}
\indexentry{errors in proofs|hyperpage}{21}
\indexentry{Fermat's Last Theorem|hyperpage}{21}
\indexentry{Stark, Harold M|hyperpage}{21}
\indexentry{Miyaoka, Yoichi|hyperpage}{21}
\indexentry{Wiles, Andrew|hyperpage}{21}
\indexentry{Euclidean geometry|hyperpage}{21}
\indexentry{Pasch's axiom|hyperpage}{21}
\indexentry{Schr\"{o}der-Berstein theorem|hyperpage}{22}
\indexentry{Enderton, Herbert B.|hyperpage}{22}
\indexentry{Hilbert, David|hyperpage}{22}
\indexentry{continuum hypothesis|hyperpage}{22}
\indexentry{Cohen, Paul|hyperpage}{22}
\indexentry{infinity|hyperpage}{22}
\indexentry{cardinal, transfinite|hyperpage}{22}
\indexentry{cardinality|hyperpage}{22}
\indexentry{Cantor, Georg|hyperpage}{22}
\indexentry{four-color theorem|hyperpage}{22}
\indexentry{Kempe, A. B.|hyperpage}{22}
\indexentry{Courant, Richard|hyperpage}{22}
\indexentry{Appel, K.|hyperpage}{22}
\indexentry{Haken, W.|hyperpage}{22}
\indexentry{Koch, K.|hyperpage}{22}
\indexentry{Coxeter, H. S. M.|hyperpage}{22}
\indexentry{Poincar\'{e} conjecture|hyperpage}{22}
\indexentry{Rourke, Colin|hyperpage}{22}
\indexentry{R\^{e}go, Eduardo|hyperpage}{22}
\indexentry{Metamath|hyperpage}{22}
\indexentry{errors in proofs|hyperpage}{22}
\indexentry{set|hyperpage}{22}
\indexentry{function|hyperpage}{22}
\indexentry{mapping|hyperpage}{22}
\indexentry{domain|hyperpage}{22}
\indexentry{Metamath|hyperpage}{23}
\indexentry{computer algebra system|hyperpage}{23}
\indexentry{Mathematica|hyperpage}{23}
\indexentry{theorem|hyperpage}{23}
\indexentry{proof|hyperpage}{23}
\indexentry{Mathematica and proofs|hyperpage}{23}
\indexentry{computer program bugs|hyperpage}{23}
\indexentry{Fermat's Last Theorem|hyperpage}{23}
\indexentry{Maple|hyperpage}{23}
\indexentry{Harrison, John|hyperpage}{24}
\indexentry{decidable theory|hyperpage}{24}
\indexentry{Euclidean geometry|hyperpage}{24}
\indexentry{Tarski, Alfred|hyperpage}{24}
\indexentry{Wen-ts{\"{u}}n, Wu|hyperpage}{24}
\indexentry{Penrose, Roger|hyperpage}{24}
\indexentry{automated theorem proving|hyperpage}{24}
\indexentry{Robinson's resolution principle|hyperpage}{24}
\indexentry{hierarchy|hyperpage}{24}
\indexentry{first-order logic|hyperpage}{24}
\indexentry{Chou, Shang-Ching|hyperpage}{24}
\indexentry{Wos, Larry|hyperpage}{25}
\indexentry{Robbins algebra|hyperpage}{25}
\indexentry{Boolean algebra|hyperpage}{25}
\indexentry{Metamath|hyperpage}{25}
\indexentry{Isabelle|hyperpage}{25}
\indexentry{otter@{\sc otter}|hyperpage}{25}
\indexentry{Wos, Larry|hyperpage}{25}
\indexentry{set theory database (\texttt{set.mm})|hyperpage}{25}
\indexentry{Megill, Norman|hyperpage}{25}
\indexentry{Bledsoe, W. W.|hyperpage}{25}
\indexentry{automated theorem proving|hyperpage}{25}
\indexentry{Huntington, E. V.|hyperpage}{25}
\indexentry{Robbins, Herbert|hyperpage}{25}
\indexentry{Tarski, Alfred|hyperpage}{25}
\indexentry{dummy variable!eliminating|hyperpage}{25}
\indexentry{qed project@{\sc qed} project|hyperpage}{26}
\indexentry{Mizar|hyperpage}{26}
\indexentry{lcf@{\sc lcf}|hyperpage}{26}
\indexentry{hol@{\sc hol}|hyperpage}{26}
\indexentry{Metamath|hyperpage}{27}
\indexentry{set theory|hyperpage}{27}
\indexentry{set theory database (\texttt{set.mm})|hyperpage}{27}
\indexentry{analysis|hyperpage}{27}
\indexentry{real and complex numbers|hyperpage}{27}
\indexentry{theorem|hyperpage}{27}
\indexentry{axiom|hyperpage}{27}
\indexentry{set theory database (\texttt{set.mm})|hyperpage}{27}
\indexentry{formal system|hyperpage}{27}
\indexentry{Metamath|hyperpage}{27}
\indexentry{formal system|hyperpage}{27}
\indexentry{modal logic|hyperpage}{27}
\indexentry{intuitionism|hyperpage}{27}
\indexentry{higher-order logic|hyperpage}{27}
\indexentry{quantum logic|hyperpage}{27}
\indexentry{category theory|hyperpage}{27}
\indexentry{Hofstadter, Douglas R.|hyperpage}{27}
\indexentry{MIU-system|hyperpage}{27}
\indexentry{Hilbert, David|hyperpage}{27}
\indexentry{metalanguage|hyperpage}{27}
\indexentry{Metamath|hyperpage}{27}
\indexentry{finitary proof|hyperpage}{27}
\indexentry{weak logic|hyperpage}{27}
\indexentry{formal system|hyperpage}{27}
\indexentry{model theory|hyperpage}{28}
\indexentry{proof theory|hyperpage}{28}
\indexentry{Metamath|hyperpage}{28}
\indexentry{formalism|hyperpage}{28}
\indexentry{Hilbert, David|hyperpage}{28}
\indexentry{Kline, Morris|hyperpage}{28}
\indexentry{Behnke, H.|hyperpage}{28}
\indexentry{metamathematics|hyperpage}{28}
\indexentry{finitary proof|hyperpage}{28}
\indexentry{Shoenfield, Joseph R.|hyperpage}{28}
\indexentry{Davis, Phillip J.|hyperpage}{28}
\indexentry{Metamath|hyperpage}{28}
\indexentry{Whitehead, Alfred North|hyperpage}{28}
\indexentry{Russell, Bertrand|hyperpage}{28}
\indexentry{principia mathematica@{\em Principia Mathematica}|hyperpage}{28}
\indexentry{condensed detachment|hyperpage}{29}
\indexentry{Hindley, J. Roger|hyperpage}{29}
\indexentry{Kalman, J. A.|hyperpage}{29}
\indexentry{Meredith, C. A.|hyperpage}{29}
\indexentry{Peterson, Jeremy George|hyperpage}{29}
\indexentry{axiom|hyperpage}{29}
\indexentry{rule|hyperpage}{29}
\indexentry{theorem|hyperpage}{29}
\indexentry{substitution!variable|hyperpage}{29}
\indexentry{variable substitution|hyperpage}{29}
\indexentry{propositional calculus|hyperpage}{29}
\indexentry{first-order logic|hyperpage}{29}
\indexentry{Megill, Norman|hyperpage}{29}
\indexentry{condensed detachment!and first-order logic|hyperpage}{29}
\indexentry{unification|hyperpage}{29}
\indexentry{substitution!variable|hyperpage}{29}
\indexentry{variable substitution|hyperpage}{29}
\indexentry{Robinson's resolution principle|hyperpage}{29}
\indexentry{first-order logic|hyperpage}{29}
\indexentry{first-order logic|hyperpage}{29}
\indexentry{category theory|hyperpage}{29}
\indexentry{cardinal, inaccessible|hyperpage}{29}
\indexentry{Metamath|hyperpage}{29}
\indexentry{set theory database (\texttt{set.mm})|hyperpage}{29}
\indexentry{metatheorem|hyperpage}{29}
\indexentry{metalogical completeness|hyperpage}{29}
\indexentry{Megill, Norman|hyperpage}{29}
\indexentry{Monk, J. Donald|hyperpage}{29}
\indexentry{Tarski, Alfred|hyperpage}{29}
\indexentry{Herrlich, Horst|hyperpage}{29}
\indexentry{Blass, Andrea|hyperpage}{29}
\indexentry{distinct variables|hyperpage}{30}
\indexentry{set theory database (\texttt{set.mm})|hyperpage}{30}
\indexentry{formal proof|hyperpage}{30}
\indexentry{free variable|hyperpage}{30}
\indexentry{bound variable|hyperpage}{30}
\indexentry{proper substitution|hyperpage}{30}
\indexentry{substitution!proper|hyperpage}{30}
\indexentry{implicit axiom|hyperpage}{30}
\indexentry{empty domain|hyperpage}{30}
\indexentry{free logic|hyperpage}{30}
\indexentry{Leblanc, Hugues|hyperpage}{30}
\indexentry{Zermelo-Fraenkel set theory|hyperpage}{30}
\indexentry{Axiom of the Null Set|hyperpage}{30}
\indexentry{Axiom of Infinity|hyperpage}{30}
\indexentry{Metamath!installation|hyperpage}{31}
\indexentry{set theory database (\texttt{set.mm})|hyperpage}{31}
\indexentry{text editor|hyperpage}{31}
\indexentry{ascii@{\sc ascii}|hyperpage}{31}
\indexentry{word processor|hyperpage}{31}
\indexentry{Word (Microsoft)|hyperpage}{31}
\indexentry{plain text|hyperpage}{31}
\indexentry{printers|hyperpage}{31}
\indexentry{monospaced font|hyperpage}{31}
\indexentry{Courier font|hyperpage}{31}
\indexentry{Monaco font|hyperpage}{31}
\indexentry{latex@{\LaTeX}|hyperpage}{32}
\indexentry{AMSFonts|hyperpage}{32}
\indexentry{Metamath|hyperpage}{32}
\indexentry{number theory|hyperpage}{32}
\indexentry{Mendelson, Elliot|hyperpage}{32}
\indexentry{formal proof|hyperpage}{32}
\indexentry{axiom|hyperpage}{32}
\indexentry{syntax rules|hyperpage}{32}
\indexentry{term|hyperpage}{32}
\indexentry{metavariable|hyperpage}{32}
\indexentry{well-formed formula (wff)|hyperpage}{32}
\indexentry{implication ($\rightarrow$)|hyperpage}{32}
\indexentry{operator precedence|hyperpage}{32}
\indexentry{axiom|hyperpage}{32}
\indexentry{theorem|hyperpage}{32}
\indexentry{axiom|hyperpage}{33}
\indexentry{axiom scheme|hyperpage}{33}
\indexentry{theorem|hyperpage}{33}
\indexentry{inference rule|hyperpage}{33}
\indexentry{modus ponens|hyperpage}{33}
\indexentry{proof|hyperpage}{33}
\indexentry{reverse Polish notation (RPN)|hyperpage}{33}
\indexentry{Metamath|hyperpage}{33}
\indexentry{theorem scheme|hyperpage}{33}
\indexentry{proof scheme|hyperpage}{33}
\indexentry{axiom|hyperpage}{33}
\indexentry{rule|hyperpage}{34}
\indexentry{modus ponens|hyperpage}{34}
\indexentry{theorem|hyperpage}{34}
\indexentry{axiom|hyperpage}{34}
\indexentry{formal proof|hyperpage}{34}
\indexentry{Mendelson, Elliot|hyperpage}{34}
\indexentry{formal proof|hyperpage}{34}
\indexentry{Rucker, Rudy|hyperpage}{34}
\indexentry{Hofstadter, Douglas R.|hyperpage}{34}
\indexentry{formal proof|hyperpage}{34}
\indexentry{axiom|hyperpage}{34}
\indexentry{term|hyperpage}{35}
\indexentry{Metamath|hyperpage}{35}
\indexentry{well-formed formula (wff)|hyperpage}{35}
\indexentry{axiom|hyperpage}{35}
\indexentry{formal proof|hyperpage}{35}
\indexentry{proof step|hyperpage}{35}
\indexentry{substitution!variable|hyperpage}{35}
\indexentry{variable substitution|hyperpage}{35}
\indexentry{\texttt{show proof} command|hyperpage}{35}
\indexentry{Metamath|hyperpage}{35}
\indexentry{metavariable|hyperpage}{35}
\indexentry{metavariable|hyperpage}{36}
\indexentry{database|hyperpage}{36}
\indexentry{Metamath|hyperpage}{36}
\indexentry{token|hyperpage}{36}
\indexentry{keyword|hyperpage}{36}
\indexentry{\texttt{\$(} and \texttt{\$)} auxiliary keywords|hyperpage}{36}
\indexentry{\texttt{\$c} statement|hyperpage}{36}
\indexentry{\texttt{\$v} statement|hyperpage}{36}
\indexentry{\texttt{\$e} statement|hyperpage}{36}
\indexentry{\texttt{\$f} statement|hyperpage}{36}
\indexentry{\texttt{\$a} statement|hyperpage}{36}
\indexentry{\texttt{\$p} statement|hyperpage}{36}
\indexentry{\texttt{\$.}\ keyword|hyperpage}{36}
\indexentry{constant declaration|hyperpage}{36}
\indexentry{variable declaration|hyperpage}{36}
\indexentry{math symbol|hyperpage}{36}
\indexentry{turnstile ({$\,\vdash$})|hyperpage}{36}
\indexentry{axiom|hyperpage}{36}
\indexentry{theorem|hyperpage}{36}
\indexentry{constant|hyperpage}{36}
\indexentry{variable|hyperpage}{36}
\indexentry{constant declaration|hyperpage}{36}
\indexentry{variable declaration|hyperpage}{36}
\indexentry{metavariable|hyperpage}{36}
\indexentry{substitution!variable|hyperpage}{36}
\indexentry{variable substitution|hyperpage}{36}
\indexentry{\texttt{\$c} statement|hyperpage}{36}
\indexentry{\texttt{\$v} statement|hyperpage}{36}
\indexentry{math symbol|hyperpage}{36}
\indexentry{redeclaration of symbols|hyperpage}{36}
\indexentry{\texttt{\$f} statement|hyperpage}{36}
\indexentry{\texttt{\$e} statement|hyperpage}{36}
\indexentry{hypothesis|hyperpage}{37}
\indexentry{variable-type hypothesis|hyperpage}{37}
\indexentry{logical hypothesis|hyperpage}{37}
\indexentry{floating hypothesis|hyperpage}{37}
\indexentry{essential hypothesis|hyperpage}{37}
\indexentry{\texttt{\$a} statement|hyperpage}{37}
\indexentry{axiomatic assertion|hyperpage}{37}
\indexentry{\texttt{\$p} statement|hyperpage}{37}
\indexentry{provable assertion|hyperpage}{37}
\indexentry{label|hyperpage}{37}
\indexentry{assertion|hyperpage}{37}
\indexentry{mandatory hypothesis|hyperpage}{37}
\indexentry{\texttt{\$f} statement|hyperpage}{37}
\indexentry{\texttt{\$e} statement|hyperpage}{37}
\indexentry{\texttt{show statement} command|hyperpage}{37}
\indexentry{\texttt{\$\char`\{} and \texttt{\$\char`\}} keywords|hyperpage}{37}
\indexentry{block|hyperpage}{37}
\indexentry{\texttt{\$p} statement|hyperpage}{37}
\indexentry{assertion|hyperpage}{37}
\indexentry{math symbol|hyperpage}{37}
\indexentry{\texttt{\$=} keyword|hyperpage}{37}
\indexentry{\texttt{\$.}\ keyword|hyperpage}{37}
\indexentry{hypothesis label|hyperpage}{37}
\indexentry{push|hyperpage}{37}
\indexentry{stack|hyperpage}{37}
\indexentry{RPN stack|hyperpage}{37}
\indexentry{compressed proof|hyperpage}{37}
\indexentry{proof!compressed|hyperpage}{37}
\indexentry{normal proof|hyperpage}{37}
\indexentry{proof!normal|hyperpage}{37}
\indexentry{assertion label|hyperpage}{38}
\indexentry{pop|hyperpage}{38}
\indexentry{substitution!variable|hyperpage}{38}
\indexentry{variable substitution|hyperpage}{38}
\indexentry{Metamath|hyperpage}{38}
\indexentry{assertion|hyperpage}{38}
\indexentry{constant|hyperpage}{38}
\indexentry{variable|hyperpage}{38}
\indexentry{Metamath|hyperpage}{38}
\indexentry{command line interface (CLI)|hyperpage}{38}
\indexentry{graphical user interface (GUI)|hyperpage}{38}
\indexentry{mouse|hyperpage}{38}
\indexentry{Metamath!limitations of version 0.06|hyperpage}{38}
\indexentry{Metamath|hyperpage}{39}
\indexentry{command keyword|hyperpage}{39}
\indexentry{\texttt{read} command|hyperpage}{39}
\indexentry{Macintosh file names|hyperpage}{39}
\indexentry{file names!Macintosh|hyperpage}{39}
\indexentry{\texttt{verify proof} command|hyperpage}{39}
\indexentry{Unix file names|hyperpage}{39}
\indexentry{file names!Unix|hyperpage}{39}
\indexentry{Metamath!limitations of version 0.06|hyperpage}{39}
\indexentry{label|hyperpage}{40}
\indexentry{\texttt{show labels} command|hyperpage}{40}
\indexentry{command qualifier|hyperpage}{40}
\indexentry{\texttt{show statement} command|hyperpage}{40}
\indexentry{mandatory hypothesis|hyperpage}{40}
\indexentry{RPN order|hyperpage}{40}
\indexentry{formal proof|hyperpage}{40}
\indexentry{\texttt{show proof} command|hyperpage}{40}
\indexentry{Lemmon-style proof|hyperpage}{41}
\indexentry{proof!Lemmon-style|hyperpage}{41}
\indexentry{tree-style proof|hyperpage}{41}
\indexentry{proof!tree-style|hyperpage}{41}
\indexentry{math symbol|hyperpage}{41}
\indexentry{formal proof|hyperpage}{42}
\indexentry{\texttt{\$f} statement|hyperpage}{42}
\indexentry{\texttt{show proof} command|hyperpage}{42}
\indexentry{\texttt{exit} command|hyperpage}{42}
\indexentry{Metamath|hyperpage}{43}
\indexentry{command line interface (CLI)|hyperpage}{43}
\indexentry{command keyword|hyperpage}{43}
\indexentry{\texttt{read} command|hyperpage}{43}
\indexentry{\texttt{submit} command|hyperpage}{43}
\indexentry{command keyword|hyperpage}{43}
\indexentry{label|hyperpage}{43}
\indexentry{math symbol|hyperpage}{43}
\indexentry{token|hyperpage}{43}
\indexentry{\texttt{help} command|hyperpage}{43}
\indexentry{\texttt{]}@\texttt{?}\ in command lines|hyperpage}{43}
\indexentry{token|hyperpage}{44}
\indexentry{Proof Assistant|hyperpage}{44}
\indexentry{source buffer|hyperpage}{44}
\indexentry{\texttt{read} command|hyperpage}{44}
\indexentry{\texttt{write} command|hyperpage}{44}
\indexentry{\texttt{]}@\texttt{?}\ inside proofs|hyperpage}{44}
\indexentry{\texttt{\$=} keyword|hyperpage}{44}
\indexentry{\texttt{\$.}\ keyword|hyperpage}{44}
\indexentry{Metamath|hyperpage}{44}
\indexentry{formal proof|hyperpage}{44}
\indexentry{\texttt{show proof} command|hyperpage}{44}
\indexentry{Proof Assistant|hyperpage}{44}
\indexentry{theorem|hyperpage}{44}
\indexentry{substitution!variable|hyperpage}{44}
\indexentry{variable substitution|hyperpage}{44}
\indexentry{unification|hyperpage}{44}
\indexentry{\texttt{prove} command|hyperpage}{45}
\indexentry{Proof Assistant|hyperpage}{45}
\indexentry{\texttt{set empty{\char`\_}substitution} command|hyperpage}{45}
\indexentry{ambiguous unification|hyperpage}{45}
\indexentry{unification!ambiguous|hyperpage}{45}
\indexentry{substitution!variable|hyperpage}{45}
\indexentry{variable substitution|hyperpage}{45}
\indexentry{formal system|hyperpage}{45}
\indexentry{empty substitution|hyperpage}{45}
\indexentry{\texttt{show new{\char`\_}proof} command|hyperpage}{45}
\indexentry{\texttt{assign} command|hyperpage}{45}
\indexentry{temporary variable|hyperpage}{46}
\indexentry{Proof Assistant|hyperpage}{46}
\indexentry{formal proof|hyperpage}{46}
\indexentry{Proof Assistant|hyperpage}{47}
\indexentry{Metamath!limitations of version 0.06|hyperpage}{47}
\indexentry{Proof Assistant|hyperpage}{48}
\indexentry{\texttt{save new{\char`\_}proof} command|hyperpage}{48}
\indexentry{normal proof|hyperpage}{48}
\indexentry{proof!normal|hyperpage}{48}
\indexentry{compressed proof|hyperpage}{48}
\indexentry{proof!compressed|hyperpage}{48}
\indexentry{\texttt{show proof} command|hyperpage}{48}
\indexentry{Proof Assistant|hyperpage}{49}
\indexentry{mandatory hypothesis|hyperpage}{49}
\indexentry{\texttt{show statement} command|hyperpage}{49}
\indexentry{Rucker, Rudy|hyperpage}{51}
\indexentry{axiom|hyperpage}{51}
\indexentry{theorem|hyperpage}{51}
\indexentry{Metamath|hyperpage}{51}
\indexentry{propositional calculus|hyperpage}{51}
\indexentry{sentential logic|hyperpage}{51}
\indexentry{first-order logic|hyperpage}{52}
\indexentry{quantifier theory|hyperpage}{52}
\indexentry{predicate calculus|hyperpage}{52}
\indexentry{Zermelo-Fraenkel set theory|hyperpage}{52}
\indexentry{set theory|hyperpage}{52}
\indexentry{axioms of logic|hyperpage}{52}
\indexentry{variable!in predicate calculus|hyperpage}{52}
\indexentry{propositional calculus|hyperpage}{52}
\indexentry{predicate calculus|hyperpage}{52}
\indexentry{set theory|hyperpage}{52}
\indexentry{empty set|hyperpage}{52}
\indexentry{integer|hyperpage}{52}
\indexentry{set union|hyperpage}{52}
\indexentry{set intersection|hyperpage}{52}
\indexentry{infinite set|hyperpage}{52}
\indexentry{natural number|hyperpage}{52}
\indexentry{brace notation|hyperpage}{52}
\indexentry{class abstraction|hyperpage}{52}
\indexentry{abstraction class|hyperpage}{52}
\indexentry{stylized epsilon ($\in$)|hyperpage}{52}
\indexentry{omega ($\omega$)|hyperpage}{52}
\indexentry{integer|hyperpage}{53}
\indexentry{rational number|hyperpage}{53}
\indexentry{real number|hyperpage}{53}
\indexentry{variable!in set theory|hyperpage}{53}
\indexentry{axiom|hyperpage}{53}
\indexentry{theorem|hyperpage}{53}
\indexentry{axioms for mathematics|hyperpage}{53}
\indexentry{Metamath|hyperpage}{54}
\indexentry{set theory database (\texttt{set.mm})|hyperpage}{54}
\indexentry{propositional calculus|hyperpage}{54}
\indexentry{well-formed formula (wff)|hyperpage}{54}
\indexentry{implication ($\rightarrow$)|hyperpage}{54}
\indexentry{negation ($\lnot$)|hyperpage}{54}
\indexentry{axioms of propositional calculus|hyperpage}{54}
\indexentry{well-formed formula (wff)|hyperpage}{54}
\indexentry{axiom scheme|hyperpage}{54}
\indexentry{theorem|hyperpage}{54}
\indexentry{rule|hyperpage}{54}
\indexentry{modus ponens|hyperpage}{54}
\indexentry{theorem|hyperpage}{54}
\indexentry{Metamath|hyperpage}{54}
\indexentry{Meredith, C. A.|hyperpage}{54}
\indexentry{tautology|hyperpage}{55}
\indexentry{truth table|hyperpage}{55}
\indexentry{set theory database (\texttt{set.mm})|hyperpage}{55}
\indexentry{predicate calculus|hyperpage}{55}
\indexentry{variable!in predicate calculus|hyperpage}{55}
\indexentry{individual variable|hyperpage}{55}
\indexentry{universal quantifier ($\forall$)|hyperpage}{55}
\indexentry{equality ($=$)|hyperpage}{55}
\indexentry{stylized epsilon ($\in$)|hyperpage}{55}
\indexentry{Metamath|hyperpage}{55}
\indexentry{metavariable|hyperpage}{55}
\indexentry{math symbol|hyperpage}{55}
\indexentry{well-formed formula (wff)|hyperpage}{55}
\indexentry{axioms of predicate calculus|hyperpage}{55}
\indexentry{well-formed formula (wff)|hyperpage}{56}
\indexentry{Metamath|hyperpage}{56}
\indexentry{set theory database (\texttt{set.mm})|hyperpage}{56}
\indexentry{free variable|hyperpage}{56}
\indexentry{proper substitution|hyperpage}{56}
\indexentry{substitution!proper|hyperpage}{56}
\indexentry{Hamilton, Alan G.|hyperpage}{56}
\indexentry{theorem|hyperpage}{56}
\indexentry{rule of generalization|hyperpage}{56}
\indexentry{decision procedure|hyperpage}{56}
\indexentry{automated theorem proving|hyperpage}{56}
\indexentry{axioms of equality|hyperpage}{56}
\indexentry{equality ($=$)|hyperpage}{56}
\indexentry{free variable|hyperpage}{57}
\indexentry{set theory database (\texttt{set.mm})|hyperpage}{57}
\indexentry{Zermelo-Fraenkel set theory|hyperpage}{57}
\indexentry{set theory|hyperpage}{57}
\indexentry{Metamath|hyperpage}{57}
\indexentry{variable!in set theory|hyperpage}{57}
\indexentry{object|hyperpage}{57}
\indexentry{set|hyperpage}{57}
\indexentry{element|hyperpage}{57}
\indexentry{collection|hyperpage}{57}
\indexentry{family|hyperpage}{57}
\indexentry{member|hyperpage}{57}
\indexentry{subset|hyperpage}{57}
\indexentry{Venn diagram|hyperpage}{57}
\indexentry{axioms of set theory|hyperpage}{57}
\indexentry{Axiom of Extensionality|hyperpage}{57}
\indexentry{Axiom of Pairing|hyperpage}{57}
\indexentry{Axiom of Power Sets|hyperpage}{57}
\indexentry{Axiom of the Null Set|hyperpage}{57}
\indexentry{Axiom of Union|hyperpage}{57}
\indexentry{Axiom of Regularity|hyperpage}{57}
\indexentry{Axiom of Infinity|hyperpage}{57}
\indexentry{Axiom of Separation|hyperpage}{58}
\indexentry{Axiom of Replacement|hyperpage}{58}
\indexentry{disjoint sets|hyperpage}{58}
\indexentry{Axiom of Choice|hyperpage}{58}
\indexentry{ZFC set theory|hyperpage}{58}
\indexentry{axiom scheme|hyperpage}{58}
\indexentry{well-formed formula (wff)|hyperpage}{58}
\indexentry{Metamath|hyperpage}{58}
\indexentry{free variable|hyperpage}{58}
\indexentry{proper substitution|hyperpage}{58}
\indexentry{substitution!proper|hyperpage}{58}
\indexentry{Metamath|hyperpage}{58}
\indexentry{substitution!variable|hyperpage}{58}
\indexentry{variable substitution|hyperpage}{58}
\indexentry{set theory database (\texttt{set.mm})|hyperpage}{58}
\indexentry{\texttt{show statement} command|hyperpage}{58}
\indexentry{disjoint variables|hyperpage}{59}
\indexentry{\texttt{\$d} statement|hyperpage}{59}
\indexentry{distinct variables|hyperpage}{59}
\indexentry{substitution!variable|hyperpage}{59}
\indexentry{variable substitution|hyperpage}{59}
\indexentry{function!in predicate calculus|hyperpage}{59}
\indexentry{constant!in predicate calculus|hyperpage}{59}
\indexentry{metalogic|hyperpage}{59}
\indexentry{axioms in \texttt{set.mm}|hyperpage}{59}
\indexentry{Megill, Norman|hyperpage}{59}
\indexentry{axioms of propositional calculus|hyperpage}{59}
\indexentry{modus ponens|hyperpage}{59}
\indexentry{axioms of predicate calculus|hyperpage}{59}
\indexentry{rule of generalization|hyperpage}{60}
\indexentry{axioms of equality|hyperpage}{60}
\indexentry{\texttt{\$d} statement|hyperpage}{60}
\indexentry{distinct variables|hyperpage}{60}
\indexentry{\texttt{\$d} statement|hyperpage}{60}
\indexentry{distinct variables|hyperpage}{60}
\indexentry{axioms of set theory|hyperpage}{60}
\indexentry{conjunction ($\wedge$)|hyperpage}{60}
\indexentry{logical {\sc and} ($\wedge$)|hyperpage}{60}
\indexentry{logical equivalence ($\leftrightarrow$)|hyperpage}{60}
\indexentry{biconditional ($\leftrightarrow$)|hyperpage}{60}
\indexentry{existential quantifier ($\exists$)|hyperpage}{60}
\indexentry{distinct variables|hyperpage}{60}
\indexentry{\texttt{\$d} statement|hyperpage}{60}
\indexentry{Axiom of Extensionality|hyperpage}{61}
\indexentry{Axiom of Replacement|hyperpage}{61}
\indexentry{Axiom of Union|hyperpage}{61}
\indexentry{Axiom of Power Sets|hyperpage}{61}
\indexentry{Axiom of Regularity|hyperpage}{61}
\indexentry{Axiom of Infinity|hyperpage}{61}
\indexentry{Axiom of Choice|hyperpage}{61}
\indexentry{definition|hyperpage}{61}
\indexentry{omega ($\omega$)|hyperpage}{61}
\indexentry{natural number|hyperpage}{61}
\indexentry{natural number|hyperpage}{61}
\indexentry{Peano's postulates|hyperpage}{61}
\indexentry{creative definition|hyperpage}{62}
\indexentry{definition!creative|hyperpage}{62}
\indexentry{definition!eliminability|hyperpage}{62}
\indexentry{definiendum|hyperpage}{62}
\indexentry{definiens|hyperpage}{62}
\indexentry{dummy variable!in definitions|hyperpage}{62}
\indexentry{effectively bound variable|hyperpage}{62}
\indexentry{qualifying expression|hyperpage}{62}
\indexentry{logical equivalence ($\leftrightarrow$)|hyperpage}{62}
\indexentry{biconditional ($\leftrightarrow$)|hyperpage}{62}
\indexentry{equality ($=$)|hyperpage}{62}
\indexentry{class|hyperpage}{62}
\indexentry{Axiom of Extensionality|hyperpage}{62}
\indexentry{\texttt{show statement} command|hyperpage}{63}
\indexentry{Takeuti, Gaisi|hyperpage}{63}
\indexentry{Quine, Willard Van Orman|hyperpage}{63}
\indexentry{Bell, J. L.|hyperpage}{63}
\indexentry{Enderton, Herbert B.|hyperpage}{63}
\indexentry{connective|hyperpage}{63}
\indexentry{constant|hyperpage}{63}
\indexentry{logical equivalence ($\leftrightarrow$)|hyperpage}{63}
\indexentry{biconditional ($\leftrightarrow$)|hyperpage}{63}
\indexentry{disjunction ($\vee$)|hyperpage}{64}
\indexentry{logical {\sc or} ($\vee$)|hyperpage}{64}
\indexentry{conjunction ($\wedge$)|hyperpage}{64}
\indexentry{logical {\sc and} ($\wedge$)|hyperpage}{64}
\indexentry{existential quantifier ($\exists$)|hyperpage}{64}
\indexentry{proper substitution|hyperpage}{64}
\indexentry{substitution!proper|hyperpage}{64}
\indexentry{existential uniqueness quantifier ($\exists "!$)|hyperpage}{65}
\indexentry{class|hyperpage}{65}
\indexentry{abstraction class|hyperpage}{65}
\indexentry{class abstraction|hyperpage}{65}
\indexentry{proper class|hyperpage}{65}
\indexentry{class!proper|hyperpage}{65}
\indexentry{abstraction class|hyperpage}{65}
\indexentry{class abstraction|hyperpage}{65}
\indexentry{postfix connective|hyperpage}{65}
\indexentry{infix connective|hyperpage}{65}
\indexentry{prefix connective|hyperpage}{65}
\indexentry{Polish notation|hyperpage}{65}
\indexentry{class equality|hyperpage}{66}
\indexentry{Axiom of Extensionality|hyperpage}{66}
\indexentry{class membership|hyperpage}{66}
\indexentry{universal quantifier ($\forall$)!restricted|hyperpage}{66}
\indexentry{existential quantifier ($\exists$)!restricted|hyperpage}{66}
\indexentry{universal class ($V$)|hyperpage}{66}
\indexentry{subclass|hyperpage}{67}
\indexentry{subset|hyperpage}{67}
\indexentry{union|hyperpage}{67}
\indexentry{intersection|hyperpage}{67}
\indexentry{class difference|hyperpage}{67}
\indexentry{set difference|hyperpage}{67}
\indexentry{empty set|hyperpage}{67}
\indexentry{null set|hyperpage}{67}
\indexentry{power set|hyperpage}{67}
\indexentry{power class|hyperpage}{67}
\indexentry{singleton|hyperpage}{67}
\indexentry{unordered pair|hyperpage}{67}
\indexentry{pair|hyperpage}{67}
\indexentry{unordered triple|hyperpage}{67}
\indexentry{Kuratowski, Kazimierz|hyperpage}{67}
\indexentry{ordered pair|hyperpage}{67}
\indexentry{union|hyperpage}{68}
\indexentry{intersection|hyperpage}{68}
\indexentry{transitive class|hyperpage}{68}
\indexentry{transitive set|hyperpage}{68}
\indexentry{binary relation|hyperpage}{68}
\indexentry{abstraction class!of ordered pairs|hyperpage}{68}
\indexentry{epsilon relation|hyperpage}{68}
\indexentry{founded relation|hyperpage}{68}
\indexentry{iff|hyperpage}{68}
\indexentry{well-ordering|hyperpage}{68}
\indexentry{ordinal predicate|hyperpage}{69}
\indexentry{ordinal number|hyperpage}{69}
\indexentry{limit ordinal|hyperpage}{69}
\indexentry{successor|hyperpage}{69}
\indexentry{natural number|hyperpage}{69}
\indexentry{omega ($\omega$)|hyperpage}{69}
\indexentry{cross product|hyperpage}{69}
\indexentry{domain|hyperpage}{69}
\indexentry{range|hyperpage}{69}
\indexentry{restriction|hyperpage}{69}
\indexentry{image|hyperpage}{70}
\indexentry{composition|hyperpage}{70}
\indexentry{relation|hyperpage}{70}
\indexentry{function|hyperpage}{70}
\indexentry{one-to-one function|hyperpage}{70}
\indexentry{onto function|hyperpage}{70}
\indexentry{function value|hyperpage}{70}
\indexentry{operation|hyperpage}{71}
\indexentry{set theory database (\texttt{set.mm})|hyperpage}{71}
\indexentry{turnstile ({$\,\vdash$})|hyperpage}{71}
\indexentry{effectively not free|hyperpage}{71}
\indexentry{substitution!implicit|hyperpage}{72}
\indexentry{Axiom of Separation|hyperpage}{73}
\indexentry{Aussonderung|hyperpage}{73}
\indexentry{Axiom of the Null Set|hyperpage}{73}
\indexentry{Axiom of Pairing|hyperpage}{73}
\indexentry{Russell's paradox|hyperpage}{73}
\indexentry{Cantor's theorem|hyperpage}{73}
\indexentry{Burali-Forti paradox|hyperpage}{73}
\indexentry{Peano's postulates|hyperpage}{74}
\indexentry{successor|hyperpage}{74}
\indexentry{finite induction|hyperpage}{74}
\indexentry{mathematical induction|hyperpage}{74}
\indexentry{transfinite induction|hyperpage}{74}
\indexentry{transfinite recursion|hyperpage}{74}
\indexentry{natural number|hyperpage}{75}
\indexentry{omega ($\omega$)|hyperpage}{75}
\indexentry{Axiom of Infinity|hyperpage}{75}
\indexentry{real and complex numbers!axioms for|hyperpage}{75}
\indexentry{latex@{\LaTeX}|hyperpage}{75}
\indexentry{operation|hyperpage}{75}
\indexentry{binary relation|hyperpage}{75}
\indexentry{set theory database (\texttt{set.mm})|hyperpage}{77}
\indexentry{well-formed formula (wff)|hyperpage}{77}
\indexentry{\texttt{\$f} statement|hyperpage}{77}
\indexentry{Metamath|hyperpage}{78}
\indexentry{set theory database (\texttt{set.mm})|hyperpage}{78}
\indexentry{command keyword|hyperpage}{78}
\indexentry{\texttt{read} command|hyperpage}{78}
\indexentry{\texttt{verify proofs} command|hyperpage}{78}
\indexentry{Enderton, Herbert B.|hyperpage}{78}
\indexentry{\texttt{search} command|hyperpage}{78}
\indexentry{Metamath!limitations of version 0.06|hyperpage}{78}
\indexentry{\texttt{search} command|hyperpage}{79}
\indexentry{\texttt{show statement} command|hyperpage}{79}
\indexentry{latex@{\LaTeX}|hyperpage}{79}
\indexentry{\texttt{show statement} command|hyperpage}{79}
\indexentry{optional variable|hyperpage}{80}
\indexentry{optional hypothesis|hyperpage}{80}
\indexentry{scope|hyperpage}{80}
\indexentry{dummy variable|hyperpage}{80}
\indexentry{\texttt{show proof} command|hyperpage}{80}
\indexentry{Hamilton, Alan G.|hyperpage}{80}
\indexentry{substitution!variable|hyperpage}{80}
\indexentry{variable substitution|hyperpage}{80}
\indexentry{\texttt{show proof} command|hyperpage}{80}
\indexentry{substitution!variable|hyperpage}{81}
\indexentry{variable substitution|hyperpage}{81}
\indexentry{conjunction ($\wedge$)|hyperpage}{81}
\indexentry{logical {\sc and} ($\wedge$)|hyperpage}{81}
\indexentry{\texttt{search} command|hyperpage}{82}
\indexentry{axiom|hyperpage}{83}
\indexentry{definition|hyperpage}{83}
\indexentry{hierarchy|hyperpage}{83}
\indexentry{\texttt{show trace{\char`\_}back} command|hyperpage}{83}
\indexentry{axiom vs.\ definition|hyperpage}{83}
\indexentry{axiom|hyperpage}{83}
\indexentry{definition|hyperpage}{83}
\indexentry{labels in \texttt{set.mm}|hyperpage}{83}
\indexentry{\texttt{\$a} statement|hyperpage}{83}
\indexentry{proof length|hyperpage}{83}
\indexentry{proof length|hyperpage}{83}
\indexentry{\texttt{show usage} command|hyperpage}{84}
\indexentry{Metamath!limitations of version 0.06|hyperpage}{84}
\indexentry{compact proof|hyperpage}{84}
\indexentry{local label|hyperpage}{84}
\indexentry{\texttt{save proof} command|hyperpage}{84}
\indexentry{Russell, Bertrand|hyperpage}{87}
\indexentry{Metamath|hyperpage}{87}
\indexentry{Metamath|hyperpage}{87}
\indexentry{Metamath|hyperpage}{87}
\indexentry{parsing Metamath|hyperpage}{88}
\indexentry{Metamath!specification|hyperpage}{88}
\indexentry{Hardy, G. H.|hyperpage}{88}
\indexentry{database|hyperpage}{88}
\indexentry{ascii@{\sc ascii}|hyperpage}{88}
\indexentry{special characters|hyperpage}{88}
\indexentry{token|hyperpage}{88}
\indexentry{white space|hyperpage}{88}
\indexentry{keyword|hyperpage}{88}
\indexentry{auxiliary keyword|hyperpage}{88}
\indexentry{label|hyperpage}{88}
\indexentry{math symbol|hyperpage}{88}
\indexentry{Metamath!limitations of version 0.06|hyperpage}{88}
\indexentry{\texttt{\$(} and \texttt{\$)} auxiliary keywords|hyperpage}{89}
\indexentry{comment|hyperpage}{89}
\indexentry{\texttt{\$[} and \texttt{\$]} auxiliary keywords|hyperpage}{89}
\indexentry{included file|hyperpage}{89}
\indexentry{file inclusion|hyperpage}{89}
\indexentry{scoping statement|hyperpage}{89}
\indexentry{block|hyperpage}{89}
\indexentry{block!outermost|hyperpage}{89}
\indexentry{\texttt{\$v} statement|hyperpage}{89}
\indexentry{\texttt{\$c} statement|hyperpage}{89}
\indexentry{declaration|hyperpage}{89}
\indexentry{variable!Metamath|hyperpage}{89}
\indexentry{constant|hyperpage}{89}
\indexentry{active math symbol|hyperpage}{89}
\indexentry{redeclaration of symbols|hyperpage}{89}
\indexentry{\texttt{\$f} statement|hyperpage}{89}
\indexentry{\texttt{\$e} statement|hyperpage}{89}
\indexentry{hypothesis|hyperpage}{89}
\indexentry{\texttt{\$d} statement!simple|hyperpage}{90}
\indexentry{\texttt{\$d} statement!compound|hyperpage}{90}
\indexentry{disjoint-variable restriction|hyperpage}{90}
\indexentry{\texttt{\$a} statement|hyperpage}{90}
\indexentry{\texttt{\$p} statement|hyperpage}{90}
\indexentry{assertion|hyperpage}{90}
\indexentry{active statement|hyperpage}{90}
\indexentry{mandatory variable|hyperpage}{90}
\indexentry{mandatory hypothesis|hyperpage}{90}
\indexentry{mandatory disjoint-variable restriction|hyperpage}{90}
\indexentry{proof!Metamath|hyperpage}{90}
\indexentry{expression|hyperpage}{90}
\indexentry{substitution map|hyperpage}{90}
\indexentry{substitution!variable|hyperpage}{90}
\indexentry{variable substitution|hyperpage}{90}
\indexentry{stack|hyperpage}{90}
\indexentry{RPN stack|hyperpage}{90}
\indexentry{compressed proof|hyperpage}{91}
\indexentry{proof!compressed|hyperpage}{91}
\indexentry{\texttt{\$d} statement|hyperpage}{91}
\indexentry{Metamath|hyperpage}{91}
\indexentry{source file|hyperpage}{91}
\indexentry{ascii@{\sc ascii}|hyperpage}{91}
\indexentry{token|hyperpage}{91}
\indexentry{white space|hyperpage}{91}
\indexentry{printable character|hyperpage}{91}
\indexentry{database|hyperpage}{91}
\indexentry{keyword|hyperpage}{91}
\indexentry{label|hyperpage}{91}
\indexentry{math symbol|hyperpage}{91}
\indexentry{symbol|hyperpage}{91}
\indexentry{basic keyword|hyperpage}{91}
\indexentry{\texttt{\$c} statement|hyperpage}{91}
\indexentry{\texttt{\$v} statement|hyperpage}{91}
\indexentry{\texttt{\$e} statement|hyperpage}{91}
\indexentry{\texttt{\$f} statement|hyperpage}{91}
\indexentry{\texttt{\$d} statement|hyperpage}{91}
\indexentry{\texttt{\$a} statement|hyperpage}{91}
\indexentry{\texttt{\$p} statement|hyperpage}{91}
\indexentry{\texttt{\$=} keyword|hyperpage}{91}
\indexentry{\texttt{\$.}\ keyword|hyperpage}{91}
\indexentry{\texttt{\$\char`\{} and \texttt{\$\char`\}} keywords|hyperpage}{91}
\indexentry{basic language|hyperpage}{91}
\indexentry{auxiliary keyword|hyperpage}{92}
\indexentry{Metamath|hyperpage}{92}
\indexentry{extended language|hyperpage}{92}
\indexentry{source file|hyperpage}{92}
\indexentry{\texttt{\$(} and \texttt{\$)} auxiliary keywords|hyperpage}{92}
\indexentry{\texttt{\$[} and \texttt{\$]} auxiliary keywords|hyperpage}{92}
\indexentry{keyword|hyperpage}{92}
\indexentry{token|hyperpage}{93}
\indexentry{keyword|hyperpage}{93}
\indexentry{Metamath|hyperpage}{93}
\indexentry{token|hyperpage}{93}
\indexentry{math symbol|hyperpage}{93}
\indexentry{Metamath|hyperpage}{93}
\indexentry{turnstile ({$\,\vdash$})|hyperpage}{93}
\indexentry{axiom|hyperpage}{93}
\indexentry{definition|hyperpage}{93}
\indexentry{\texttt{\$a} statement|hyperpage}{93}
\indexentry{token|hyperpage}{93}
\indexentry{math symbol|hyperpage}{93}
\indexentry{\texttt{open tex} command|hyperpage}{93}
\indexentry{latex@{\LaTeX}|hyperpage}{93}
\indexentry{token|hyperpage}{94}
\indexentry{label|hyperpage}{94}
\indexentry{Metamath|hyperpage}{94}
\indexentry{label declaration|hyperpage}{94}
\indexentry{\texttt{\$e} statement|hyperpage}{94}
\indexentry{\texttt{\$f} statement|hyperpage}{94}
\indexentry{\texttt{\$a} statement|hyperpage}{94}
\indexentry{\texttt{\$p} statement|hyperpage}{94}
\indexentry{label reference|hyperpage}{94}
\indexentry{\texttt{\$=} keyword|hyperpage}{94}
\indexentry{\texttt{\$.}\ keyword|hyperpage}{94}
\indexentry{label sequence|hyperpage}{94}
\indexentry{proof|hyperpage}{94}
\indexentry{constant|hyperpage}{94}
\indexentry{variable|hyperpage}{94}
\indexentry{expression|hyperpage}{94}
\indexentry{Metamath|hyperpage}{94}
\indexentry{basic language|hyperpage}{94}
\indexentry{math symbol|hyperpage}{94}
\indexentry{constant|hyperpage}{94}
\indexentry{variable|hyperpage}{94}
\indexentry{substitution!variable|hyperpage}{94}
\indexentry{variable substitution|hyperpage}{94}
\indexentry{variable type|hyperpage}{94}
\indexentry{type|hyperpage}{94}
\indexentry{metavariable|hyperpage}{94}
\indexentry{\texttt{\$c} statement|hyperpage}{95}
\indexentry{constant declaration|hyperpage}{95}
\indexentry{\texttt{\$v} statement|hyperpage}{95}
\indexentry{variable declaration|hyperpage}{95}
\indexentry{constant declaration|hyperpage}{95}
\indexentry{\texttt{\$c} statement|hyperpage}{95}
\indexentry{variable declaration|hyperpage}{95}
\indexentry{\texttt{\$v} statement|hyperpage}{95}
\indexentry{simple declaration|hyperpage}{95}
\indexentry{token|hyperpage}{95}
\indexentry{math symbol|hyperpage}{95}
\indexentry{compound declaration|hyperpage}{95}
\indexentry{\texttt{\$c} statement|hyperpage}{95}
\indexentry{\texttt{\$v} statement|hyperpage}{95}
\indexentry{\texttt{\$d} statement|hyperpage}{95}
\indexentry{active math symbol|hyperpage}{96}
\indexentry{scope|hyperpage}{96}
\indexentry{distinct variables|hyperpage}{96}
\indexentry{non-trivial theory|hyperpage}{96}
\indexentry{free vs.\ bound variable|hyperpage}{96}
\indexentry{\texttt{\$d} statement|hyperpage}{96}
\indexentry{disjoint variables|hyperpage}{96}
\indexentry{\texttt{\$d} statement|hyperpage}{96}
\indexentry{proper substitution|hyperpage}{96}
\indexentry{substitution!proper|hyperpage}{96}
\indexentry{free variable|hyperpage}{96}
\indexentry{bound variable|hyperpage}{96}
\indexentry{empty substitution|hyperpage}{97}
\indexentry{variable|hyperpage}{97}
\indexentry{variable!in ordinary mathematics|hyperpage}{97}
\indexentry{metavariable|hyperpage}{97}
\indexentry{\texttt{\$d} statement|hyperpage}{97}
\indexentry{\texttt{\$d} statement|hyperpage}{97}
\indexentry{Metamath|hyperpage}{98}
\indexentry{label|hyperpage}{98}
\indexentry{distinct variables|hyperpage}{98}
\indexentry{\texttt{\$d} statement|hyperpage}{100}
\indexentry{\texttt{\$a} statement|hyperpage}{100}
\indexentry{\texttt{\$d} statement|hyperpage}{100}
\indexentry{dummy variable!eliminating|hyperpage}{100}
\indexentry{Andr{\'{e}}ka, H.|hyperpage}{100}
\indexentry{Megill, Norman|hyperpage}{100}
\indexentry{\texttt{\$e} statement|hyperpage}{100}
\indexentry{\texttt{\$f} statement|hyperpage}{100}
\indexentry{floating hypothesis|hyperpage}{100}
\indexentry{essential hypothesis|hyperpage}{100}
\indexentry{variable-type hypothesis|hyperpage}{100}
\indexentry{logical hypothesis|hyperpage}{100}
\indexentry{hypothesis|hyperpage}{100}
\indexentry{\texttt{\$f} statement|hyperpage}{100}
\indexentry{\texttt{\$d} statement|hyperpage}{100}
\indexentry{floating hypothesis|hyperpage}{100}
\indexentry{essential hypothesis|hyperpage}{100}
\indexentry{\texttt{\$e} statement|hyperpage}{101}
\indexentry{\texttt{\$f} statement|hyperpage}{101}
\indexentry{label|hyperpage}{101}
\indexentry{variable type|hyperpage}{101}
\indexentry{type|hyperpage}{101}
\indexentry{theorem|hyperpage}{101}
\indexentry{free variable|hyperpage}{101}
\indexentry{inference|hyperpage}{101}
\indexentry{Metamath|hyperpage}{101}
\indexentry{\texttt{\$p} statement|hyperpage}{101}
\indexentry{\texttt{\$e} statement|hyperpage}{101}
\indexentry{\texttt{\$f} statement|hyperpage}{101}
\indexentry{turnstile ({$\,\vdash$})|hyperpage}{101}
\indexentry{assertion|hyperpage}{101}
\indexentry{\texttt{\$a} statement|hyperpage}{102}
\indexentry{\texttt{\$p} statement|hyperpage}{102}
\indexentry{assertion|hyperpage}{102}
\indexentry{axiomatic assertion|hyperpage}{102}
\indexentry{provable assertion|hyperpage}{102}
\indexentry{\texttt{\$a} statement|hyperpage}{102}
\indexentry{\texttt{\$a} statement|hyperpage}{102}
\indexentry{\texttt{\$p} statement|hyperpage}{102}
\indexentry{\texttt{\$=} keyword|hyperpage}{102}
\indexentry{label|hyperpage}{102}
\indexentry{axiom|hyperpage}{102}
\indexentry{definition|hyperpage}{102}
\indexentry{\texttt{\$a} statement|hyperpage}{102}
\indexentry{\texttt{\$p} statement|hyperpage}{102}
\indexentry{axiom|hyperpage}{102}
\indexentry{Metamath|hyperpage}{102}
\indexentry{formal logic|hyperpage}{102}
\indexentry{\texttt{\$a} statement|hyperpage}{102}
\indexentry{axiom vs.\ definition|hyperpage}{102}
\indexentry{axiom|hyperpage}{102}
\indexentry{definition|hyperpage}{102}
\indexentry{label|hyperpage}{103}
\indexentry{\texttt{\$a} statement|hyperpage}{103}
\indexentry{axiom|hyperpage}{103}
\indexentry{rule|hyperpage}{103}
\indexentry{proper definition|hyperpage}{103}
\indexentry{definition!proper|hyperpage}{103}
\indexentry{\texttt{\$a} statement|hyperpage}{103}
\indexentry{frame|hyperpage}{103}
\indexentry{mandatory variable|hyperpage}{104}
\indexentry{mandatory hypothesis|hyperpage}{105}
\indexentry{RPN order|hyperpage}{105}
\indexentry{dummy variable|hyperpage}{105}
\indexentry{extended frame|hyperpage}{105}
\indexentry{optional variable|hyperpage}{105}
\indexentry{optional hypothesis|hyperpage}{105}
\indexentry{optional disjoint-variable restriction|hyperpage}{105}
\indexentry{\texttt{\$\char`\{} and \texttt{\$\char`\}} keywords|hyperpage}{106}
\indexentry{\texttt{\$\char`\{} and \texttt{\$\char`\}} keywords|hyperpage}{107}
\indexentry{scoping statement|hyperpage}{107}
\indexentry{block|hyperpage}{107}
\indexentry{\texttt{\$\char`\{} and \texttt{\$\char`\}} keywords|hyperpage}{107}
\indexentry{block|hyperpage}{107}
\indexentry{nested block|hyperpage}{107}
\indexentry{non-scoping statement|hyperpage}{107}
\indexentry{recursive definition|hyperpage}{107}
\indexentry{nesting level|hyperpage}{107}
\indexentry{\texttt{\$\char`\{} and \texttt{\$\char`\}} keywords|hyperpage}{107}
\indexentry{outermost block|hyperpage}{107}
\indexentry{active statement|hyperpage}{107}
\indexentry{\texttt{\$c} statement|hyperpage}{108}
\indexentry{\texttt{\$d} statement|hyperpage}{108}
\indexentry{\texttt{\$e} statement|hyperpage}{108}
\indexentry{\texttt{\$f} statement|hyperpage}{108}
\indexentry{\texttt{\$v} statement|hyperpage}{108}
\indexentry{\texttt{\$a} statement|hyperpage}{108}
\indexentry{\texttt{\$p} statement|hyperpage}{108}
\indexentry{outermost block|hyperpage}{108}
\indexentry{global statement|hyperpage}{108}
\indexentry{scope|hyperpage}{108}
\indexentry{math symbol|hyperpage}{108}
\indexentry{constant|hyperpage}{108}
\indexentry{variable|hyperpage}{108}
\indexentry{active math symbol|hyperpage}{108}
\indexentry{\texttt{\$c} statement|hyperpage}{108}
\indexentry{\texttt{\$v} statement|hyperpage}{108}
\indexentry{redeclaration of symbols|hyperpage}{108}
\indexentry{local variable|hyperpage}{108}
\indexentry{frames and scoping statements|hyperpage}{109}
\indexentry{proof!Metamath, description of|hyperpage}{109}
\indexentry{\texttt{\$p} statement|hyperpage}{109}
\indexentry{proof|hyperpage}{109}
\indexentry{\texttt{\$=} keyword|hyperpage}{109}
\indexentry{basic language|hyperpage}{109}
\indexentry{label sequence|hyperpage}{109}
\indexentry{\texttt{\$p} statement|hyperpage}{109}
\indexentry{\texttt{\$=} keyword|hyperpage}{109}
\indexentry{\texttt{verify proof} command|hyperpage}{109}
\indexentry{label reference|hyperpage}{109}
\indexentry{assertion|hyperpage}{109}
\indexentry{\texttt{\$a} statement|hyperpage}{109}
\indexentry{\texttt{\$f} statement|hyperpage}{109}
\indexentry{\texttt{\$e} statement|hyperpage}{109}
\indexentry{label|hyperpage}{109}
\indexentry{\texttt{\$a} statement|hyperpage}{109}
\indexentry{\texttt{\$p} statement|hyperpage}{109}
\indexentry{\texttt{\$f} statement|hyperpage}{109}
\indexentry{mandatory hypothesis|hyperpage}{109}
\indexentry{reverse Polish notation (RPN)|hyperpage}{109}
\indexentry{hypothesis label|hyperpage}{109}
\indexentry{assertion label|hyperpage}{109}
\indexentry{stack|hyperpage}{110}
\indexentry{RPN stack|hyperpage}{110}
\indexentry{push|hyperpage}{110}
\indexentry{mandatory hypothesis|hyperpage}{110}
\indexentry{substitution!variable|hyperpage}{110}
\indexentry{variable substitution|hyperpage}{110}
\indexentry{pop|hyperpage}{110}
\indexentry{well-formed formula (wff)|hyperpage}{110}
\indexentry{\texttt{\$p} statement|hyperpage}{112}
\indexentry{mandatory hypothesis|hyperpage}{112}
\indexentry{\texttt{show proof} command|hyperpage}{112}
\indexentry{tree-style proof|hyperpage}{112}
\indexentry{proof!tree-style|hyperpage}{112}
\indexentry{hypothesis association|hyperpage}{112}
\indexentry{label|hyperpage}{112}
\indexentry{\texttt{show proof} command|hyperpage}{112}
\indexentry{\texttt{\$d} statement|hyperpage}{113}
\indexentry{mandatory \texttt{\$d} statement|hyperpage}{113}
\indexentry{substitution!variable|hyperpage}{113}
\indexentry{variable substitution|hyperpage}{113}
\indexentry{Metamath|hyperpage}{113}
\indexentry{assertion label|hyperpage}{113}
\indexentry{mandatory hypothesis|hyperpage}{113}
\indexentry{stack|hyperpage}{113}
\indexentry{RPN stack|hyperpage}{113}
\indexentry{substitution!variable|hyperpage}{113}
\indexentry{variable substitution|hyperpage}{113}
\indexentry{unification|hyperpage}{113}
\indexentry{Proof Assistant|hyperpage}{113}
\indexentry{ambiguous unification|hyperpage}{113}
\indexentry{unification!ambiguous|hyperpage}{113}
\indexentry{extended language|hyperpage}{113}
\indexentry{white space|hyperpage}{113}
\indexentry{token|hyperpage}{113}
\indexentry{\texttt{\$(} and \texttt{\$)} auxiliary keywords|hyperpage}{113}
\indexentry{comment|hyperpage}{113}
\indexentry{\texttt{`} inside comments|hyperpage}{114}
\indexentry{\texttt{\char`\~} inside comments|hyperpage}{114}
\indexentry{token|hyperpage}{114}
\indexentry{grave accent (\texttt{`})|hyperpage}{114}
\indexentry{latex@{\LaTeX}|hyperpage}{114}
\indexentry{math mode|hyperpage}{114}
\indexentry{tilde (\texttt{\char`\~})|hyperpage}{114}
\indexentry{white space|hyperpage}{114}
\indexentry{label mode|hyperpage}{114}
\indexentry{\texttt{substitute symbol} command|hyperpage}{114}
\indexentry{\texttt{substitute label} command|hyperpage}{114}
\indexentry{token|hyperpage}{114}
\indexentry{math symbol|hyperpage}{114}
\indexentry{math mode|hyperpage}{114}
\indexentry{grave accent (\texttt{`})|hyperpage}{114}
\indexentry{Metamath|hyperpage}{114}
\indexentry{white space|hyperpage}{114}
\indexentry{Pierce's axiom|hyperpage}{114}
\indexentry{Metamath!limitations of version 0.06|hyperpage}{114}
\indexentry{Metamath!limitations of version 0.06|hyperpage}{114}
\indexentry{token|hyperpage}{115}
\indexentry{white space|hyperpage}{115}
\indexentry{Metamath!using as a math editor|hyperpage}{115}
\indexentry{latex@{\LaTeX}|hyperpage}{115}
\indexentry{label mode|hyperpage}{115}
\indexentry{tilde (\texttt{\char`\~})|hyperpage}{115}
\indexentry{Metamath|hyperpage}{115}
\indexentry{token|hyperpage}{115}
\indexentry{white space|hyperpage}{115}
\indexentry{\texttt{substitute label} command|hyperpage}{115}
\indexentry{\texttt{\$[} and \texttt{\$]} auxiliary keywords|hyperpage}{115}
\indexentry{included file|hyperpage}{115}
\indexentry{file inclusion|hyperpage}{115}
\indexentry{Metamath|hyperpage}{115}
\indexentry{source file|hyperpage}{115}
\indexentry{token|hyperpage}{115}
\indexentry{Metamath!limitations of version 0.06|hyperpage}{115}
\indexentry{Macintosh file names|hyperpage}{116}
\indexentry{file names!Macintosh|hyperpage}{116}
\indexentry{outermost block|hyperpage}{116}
\indexentry{compressed proof|hyperpage}{116}
\indexentry{proof!compressed|hyperpage}{116}
\indexentry{normal proof|hyperpage}{116}
\indexentry{proof!normal|hyperpage}{116}
\indexentry{Metamath|hyperpage}{116}
\indexentry{\texttt{\$=} keyword|hyperpage}{116}
\indexentry{mandatory hypothesis|hyperpage}{116}
\indexentry{white space|hyperpage}{116}
\indexentry{\texttt{save proof} command|hyperpage}{117}
\indexentry{\texttt{]}@\texttt{?}\ inside proofs|hyperpage}{117}
\indexentry{Proof Assistant|hyperpage}{117}
\indexentry{\texttt{save new{\char`\_}proof} command|hyperpage}{117}
\indexentry{\texttt{\$p} statement|hyperpage}{117}
\indexentry{\texttt{\$=} keyword|hyperpage}{117}
\indexentry{\texttt{]}@\texttt{?}\ inside proofs|hyperpage}{117}
\indexentry{\texttt{verify proof} command|hyperpage}{117}
\indexentry{compressed proof|hyperpage}{117}
\indexentry{proof!compressed|hyperpage}{117}
\indexentry{Metamath|hyperpage}{117}
\indexentry{axiom vs.\ definition|hyperpage}{117}
\indexentry{axiom|hyperpage}{117}
\indexentry{definition|hyperpage}{117}
\indexentry{\texttt{\$a} statement|hyperpage}{117}
\indexentry{theorem|hyperpage}{117}
\indexentry{Behnke, H.|hyperpage}{117}
\indexentry{proper definition|hyperpage}{117}
\indexentry{definition!proper|hyperpage}{117}
\indexentry{creative definition|hyperpage}{118}
\indexentry{definition!creative|hyperpage}{118}
\indexentry{Nemesszeghy, E. Z.|hyperpage}{118}
\indexentry{Le\'{s}niewski, S.|hyperpage}{118}
\indexentry{Lejewski, Czeslaw|hyperpage}{118}
\indexentry{disjunction ($\vee$)|hyperpage}{118}
\indexentry{well-formed formula (wff)|hyperpage}{118}
\indexentry{definition|hyperpage}{118}
\indexentry{axiom vs.\ definition|hyperpage}{118}
\indexentry{axiom|hyperpage}{118}
\indexentry{set theory database (\texttt{set.mm})|hyperpage}{118}
\indexentry{Goodstein, R. L.|hyperpage}{118}
\indexentry{intuitionism|hyperpage}{118}
\indexentry{Quine, Willard Van Orman|hyperpage}{119}
\indexentry{metalogic|hyperpage}{119}
\indexentry{successor|hyperpage}{119}
\indexentry{recursive definition|hyperpage}{119}
\indexentry{natural number|hyperpage}{119}
\indexentry{addition|hyperpage}{119}
\indexentry{recursive definition|hyperpage}{119}
\indexentry{ordinal addition|hyperpage}{119}
\indexentry{Robinson, T. Thacher|hyperpage}{119}
\indexentry{ordinal addition|hyperpage}{119}
\indexentry{addition!of ordinals|hyperpage}{119}
\indexentry{abstraction class!of nested ordered pairs|hyperpage}{119}
\indexentry{recursion operator|hyperpage}{119}
\indexentry{Metamath!commands|hyperpage}{121}
\indexentry{Unix file names|hyperpage}{121}
\indexentry{file names!Unix|hyperpage}{121}
\indexentry{\texttt{exit} command|hyperpage}{121}
\indexentry{Proof Assistant|hyperpage}{121}
\indexentry{\texttt{open log} command|hyperpage}{121}
\indexentry{Metamath!bugs|hyperpage}{121}
\indexentry{\texttt{close log} command|hyperpage}{121}
\indexentry{\texttt{open tex} command|hyperpage}{122}
\indexentry{latex@{\LaTeX}|hyperpage}{122}
\indexentry{\texttt{close tex} command|hyperpage}{122}
\indexentry{latex@{\LaTeX}|hyperpage}{122}
\indexentry{\texttt{submit} command|hyperpage}{122}
\indexentry{\texttt{erase} command|hyperpage}{122}
\indexentry{operating system command|hyperpage}{122}
\indexentry{\texttt{set echo} command|hyperpage}{123}
\indexentry{\texttt{set scroll} command|hyperpage}{123}
\indexentry{\texttt{set screen{\char`\_}width} command|hyperpage}{123}
\indexentry{latex@{\LaTeX}!characters per line|hyperpage}{123}
\indexentry{\texttt{beep} command|hyperpage}{123}
\indexentry{\texttt{read} command|hyperpage}{123}
\indexentry{database|hyperpage}{123}
\indexentry{Macintosh file names|hyperpage}{123}
\indexentry{file names!Macintosh|hyperpage}{123}
\indexentry{\texttt{write source} command|hyperpage}{124}
\indexentry{database|hyperpage}{124}
\indexentry{source file|hyperpage}{124}
\indexentry{Metamath!limitations of version 0.06|hyperpage}{124}
\indexentry{\texttt{\$[} and \texttt{\$]} auxiliary keywords|hyperpage}{124}
\indexentry{\texttt{show settings} command|hyperpage}{124}
\indexentry{\texttt{show memory} command|hyperpage}{124}
\indexentry{Metamath!memory usage|hyperpage}{124}
\indexentry{\texttt{show labels} command|hyperpage}{124}
\indexentry{\texttt{show statement} command|hyperpage}{124}
\indexentry{\texttt{\$f} statement|hyperpage}{124}
\indexentry{\texttt{\$e} statement|hyperpage}{124}
\indexentry{\texttt{\$a} statement|hyperpage}{124}
\indexentry{\texttt{\$p} statement|hyperpage}{124}
\indexentry{latex@{\LaTeX}|hyperpage}{124}
\indexentry{\texttt{search} command|hyperpage}{125}
\indexentry{\texttt{show proof} command|hyperpage}{125}
\indexentry{\texttt{\$p} statement|hyperpage}{125}
\indexentry{\texttt{\$f} statement|hyperpage}{125}
\indexentry{latex@{\LaTeX}|hyperpage}{125}
\indexentry{\texttt{show usage} command|hyperpage}{126}
\indexentry{\texttt{show        trace{\char`\_}back} command|hyperpage}{126}
\indexentry{\texttt{\$p} statement|hyperpage}{126}
\indexentry{\texttt{\$e} statement|hyperpage}{126}
\indexentry{\texttt{verify proof} command|hyperpage}{126}
\indexentry{\texttt{save proof} command|hyperpage}{127}
\indexentry{source buffer|hyperpage}{127}
\indexentry{basic language|hyperpage}{127}
\indexentry{Metamath!limitations of version 0.06|hyperpage}{127}
\indexentry{\texttt{prove} command|hyperpage}{127}
\indexentry{Proof Assistant|hyperpage}{127}
\indexentry{Metamath!memory usage|hyperpage}{127}
\indexentry{\texttt{show memory} command|hyperpage}{127}
\indexentry{Metamath!limitations of version 0.06|hyperpage}{127}
\indexentry{\texttt{set unification{\char`\_}timeout} command|hyperpage}{128}
\indexentry{Proof Assistant|hyperpage}{128}
\indexentry{temporary variable|hyperpage}{128}
\indexentry{\texttt{set empty{\char`\_}substitution} command|hyperpage}{128}
\indexentry{Proof Assistant|hyperpage}{128}
\indexentry{substitution!variable|hyperpage}{128}
\indexentry{variable substitution|hyperpage}{128}
\indexentry{empty substitution|hyperpage}{128}
\indexentry{formal system|hyperpage}{128}
\indexentry{ambiguous unification|hyperpage}{128}
\indexentry{unification!ambiguous|hyperpage}{128}
\indexentry{MIU-system|hyperpage}{128}
\indexentry{\texttt{set search{\char`\_}limit} command|hyperpage}{128}
\indexentry{Proof Assistant|hyperpage}{128}
\indexentry{\texttt{show new{\char`\_}proof} command|hyperpage}{128}
\indexentry{\texttt{assign} command|hyperpage}{129}
\indexentry{Proof Assistant|hyperpage}{129}
\indexentry{\texttt{]}@\texttt{?}\ inside proofs|hyperpage}{129}
\indexentry{\texttt{match} command|hyperpage}{129}
\indexentry{\texttt{\$e} statement|hyperpage}{129}
\indexentry{\texttt{let} command|hyperpage}{129}
\indexentry{Proof Assistant|hyperpage}{129}
\indexentry{temporary variable|hyperpage}{129}
\indexentry{\texttt{unify} command|hyperpage}{130}
\indexentry{\texttt{initialize} command|hyperpage}{130}
\indexentry{Proof Assistant|hyperpage}{130}
\indexentry{\texttt{delete} command|hyperpage}{130}
\indexentry{\texttt{\$f} statement|hyperpage}{130}
\indexentry{\texttt{improve} command|hyperpage}{131}
\indexentry{Proof Assistant|hyperpage}{131}
\indexentry{\texttt{\$f} statement|hyperpage}{131}
\indexentry{\texttt{\$e} statement|hyperpage}{131}
\indexentry{\texttt{\$e} statement|hyperpage}{131}
\indexentry{\texttt{save new{\char`\_}proof} command|hyperpage}{131}
\indexentry{source buffer|hyperpage}{131}
\indexentry{ambiguous unification|hyperpage}{131}
\indexentry{unification!ambiguous|hyperpage}{131}
\indexentry{basic language|hyperpage}{131}
\indexentry{\texttt{file type} command|hyperpage}{132}
\indexentry{\texttt{file type} command|hyperpage}{132}
\indexentry{Metamath!memory limits|hyperpage}{132}
\indexentry{token|hyperpage}{132}
\indexentry{Proof Assistant|hyperpage}{132}
\indexentry{latex definitions@\LaTeX\ definitions|hyperpage}{133}
\indexentry{Metamath!limitations of version 0.06|hyperpage}{133}
\indexentry{compressed proof|hyperpage}{137}
\indexentry{proof!compressed|hyperpage}{137}
\indexentry{RPN order|hyperpage}{138}
\indexentry{Metamath!as a formal system|hyperpage}{139}
\indexentry{de Saint-Exupery, Antoine|hyperpage}{139}
\indexentry{Munkres, James R.|hyperpage}{139}
\indexentry{simple infinite sequence|hyperpage}{140}
\indexentry{term|hyperpage}{140}
\indexentry{finite $n$-termed sequence|hyperpage}{140}
\indexentry{length of a sequence ({$"|\ "|$})|hyperpage}{140}
\indexentry{concatenation|hyperpage}{140}
\indexentry{symbol!in a formal system|hyperpage}{140}
\indexentry{constant!in a formal system|hyperpage}{140}
\indexentry{variable!in a formal system|hyperpage}{140}
\indexentry{Tarski, Alfred|hyperpage}{140}
\indexentry{expression!in a formal system|hyperpage}{141}
\indexentry{constant-prefixed expression|hyperpage}{141}
\indexentry{constant-variable pair|hyperpage}{141}
\indexentry{substitution!variable|hyperpage}{141}
\indexentry{variable substitution|hyperpage}{141}
\indexentry{substitution map|hyperpage}{141}
\indexentry{pre-statement!in a formal system|hyperpage}{141}
\indexentry{disjoint-variable restriction!in a formal system|hyperpage}{142}
\indexentry{variable-type hypothesis!in a formal system|hyperpage}{142}
\indexentry{logical hypothesis!in a formal system|hyperpage}{142}
\indexentry{assertion!in a formal system|hyperpage}{142}
\indexentry{mandatory variable-type hypothesis!in a formal system|hyperpage}{142}
\indexentry{mandatory disjoint-variable restriction!in a formal system|hyperpage}{142}
\indexentry{mandatory hypothesis!in a formal system|hyperpage}{142}
\indexentry{reduct!in a formal system|hyperpage}{142}
\indexentry{statement!in a formal system|hyperpage}{142}
\indexentry{Andr{\'{e}}ka, H.|hyperpage}{142}
\indexentry{formal system|hyperpage}{142}
\indexentry{axiomatic statement!in a formal system|hyperpage}{142}
\indexentry{closure|hyperpage}{142}
\indexentry{provable statement!in a formal system|hyperpage}{143}
\indexentry{universe of a formal system|hyperpage}{143}
\indexentry{propositional calculus|hyperpage}{144}
\indexentry{inference|hyperpage}{145}
\indexentry{predicate calculus|hyperpage}{145}
\indexentry{individual metavariable|hyperpage}{145}
\indexentry{free variable|hyperpage}{147}
\indexentry{proper substitution|hyperpage}{147}
\indexentry{substitution!proper|hyperpage}{147}
\indexentry{effectively not free|hyperpage}{147}
\indexentry{effectively not free|hyperpage}{147}
\indexentry{metalogical completeness|hyperpage}{148}
\indexentry{simple metatheorem|hyperpage}{148}
\indexentry{metalogical completeness|hyperpage}{148}
\indexentry{Megill, Norman|hyperpage}{148}
\indexentry{metalogical completeness|hyperpage}{148}
\indexentry{definition|hyperpage}{150}
\indexentry{logical equivalence ($\leftrightarrow$)|hyperpage}{150}
\indexentry{biconditional ($\leftrightarrow$)|hyperpage}{150}
\indexentry{conjunction ($\wedge$)|hyperpage}{150}
\indexentry{disjunction ($\vee$)|hyperpage}{150}
\indexentry{existential quantifier ($\exists$)|hyperpage}{150}
\indexentry{ZFC set theory|hyperpage}{150}
\indexentry{Axiom of Extensionality|hyperpage}{151}
\indexentry{Axiom of Replacement|hyperpage}{151}
\indexentry{Axiom of Union|hyperpage}{151}
\indexentry{Axiom of Power Sets|hyperpage}{151}
\indexentry{Axiom of Regularity|hyperpage}{151}
\indexentry{Axiom of Infinity|hyperpage}{151}
\indexentry{Axiom of Choice|hyperpage}{151}
\indexentry{class abstraction|hyperpage}{151}
\indexentry{abstraction class|hyperpage}{151}
\indexentry{Takeuti, Gaisi|hyperpage}{151}
\indexentry{Quine, Willard Van Orman|hyperpage}{151}
\indexentry{proper class|hyperpage}{151}
\indexentry{class!proper|hyperpage}{151}
\indexentry{class variable|hyperpage}{151}
\indexentry{empty set|hyperpage}{152}
\indexentry{union|hyperpage}{152}
\indexentry{unordered pair|hyperpage}{152}
\indexentry{formal system|hyperpage}{155}
\indexentry{MIU-system|hyperpage}{155}
\indexentry{well-formed formula (wff)|hyperpage}{157}
\indexentry{Hofstadter, Douglas R.|hyperpage}{157}
\indexentry{latex@{\LaTeX}|hyperpage}{159}
\indexentry{latex@{\LaTeX}|hyperpage}{159}
\indexentry{AMSFonts|hyperpage}{159}