\begin{thebibliography}{}

\bibitem[\protect\citeauthoryear{Ackermann\protect\ackermannindex}{1925}]{acke%
rmann-1925}
Wilhelm Ackermann\protect\ackermannindex.
\newblock {Begr\ue ndung des \glqq tertium non datur\grqq\ mittel\es\ der
  \hilbert\-schen Theorie der Widerspruch\esi freiheit}.
\newblock {\em {\MathematischeAnnalen}}, 93:1--36, 1925.
\newblock Received \Mar\,30, 1924. Inauguraldissertation, \Goettingen\,1924.

\bibitem[\protect\citeauthoryear{Ackermann\protect\ackermannindex}{1940}]{acke%
rmann-consistency-of-arithmetic}
Wilhelm Ackermann\protect\ackermannindex.
\newblock {Zur Wider\-spruch\esi frei\-heit der Zahlen\-theorie}.
\newblock {\em {\MathematischeAnnalen}}, 117:163--194, 1940.
\newblock Received \Aug\,15, 1939.

\bibitem[\protect\citeauthoryear{Andrew\protect\index{Andrews, Peter
  B.}s}{2002}]{andrews}
Peter~B. Andrew\protect\index{Andrews, Peter B.}s.
\newblock {\em An Introduction to Mathematical Logic and Type Theory: To Truth
  Through Proof}.
\newblock {\academicpress}, 2002.
\newblock \nth 2\,\ed\ (\nth 1\,\ed\ 1986).

\bibitem[\protect\citeauthoryear{Andrew\protect\index{Andrews, Peter
  B.}s}{2003}]{andrews-herbrand-award}
Peter~B. Andrew\protect\index{Andrews, Peter B.}s.
\newblock {\herbrand\ Award} acceptance speech.
\newblock {\em J. Automated Reasoning}, 31:169--187, 2003.

\bibitem[\protect\citeauthoryear{Anelli\protect\index{Anellis!Irving
  H.}s}{1991}]{anellis-loewenheim}
Irving~H. Anelli\protect\index{Anellis!Irving H.}s.
\newblock The {\loewenheimskolemtheorem}, theories of quantification, and proof
  theory.
\newblock 1991.
\newblock In \cite[\PP{71}{83}]{drucker}.

\bibitem[\protect\citeauthoryear{Anelli\protect\index{Anellis!Irving
  H.}s}{1992}]{anellis-heijenoort-long}
Irving~H.\protect\index{Heijenoort!Jean van}
  Anelli\protect\index{Anellis!Irving H.}s.
\newblock {\em Logic and Its History in the Work and Writings of\/
  {\heijenoortname}}.
\newblock Modern Logic Publ., Ames (IA), 1992.

\bibitem[\protect\citeauthoryear{Anelli\protect\index{Anellis!Irving
  H.}s}{2006}]{anellis-skolem-function}
Irving~H. Anelli\protect\index{Anellis!Irving H.}s.
\newblock \goedel\ and the naming of \skolem\ functions.
\newblock In {\em Sovremennaja logika: problemy teorii, istorii i primenenija v
  nauke. Materialy IX Obshcherossijskoj nauchnoj konferencii. Sankt-Peterburg,
  \Jun\,22--24, 2006}, pages 410--413. Izdatel\'stvo Sankt Peterburgskogo
  Universiteta, \StPetersburg, 2006.
\newblock {ISBN 5-288-03998-4}.

\bibitem[\protect\citeauthoryear{Artin\protect\index{Artin!Emil} \bgroup\&\
  \egroup Schreier}{1927}]{artin-schreier}
Emil Artin\protect\index{Artin!Emil} and Otto Schreier.
\newblock {Algebraische Konstruktion reeller K\oe rper}.
\newblock {\em {\AbhandlungenmathHamburgname}}, 5:85--99, 1927.
\newblock Hamburg, Mathematisches Seminar, \Jun\,1926. Facsimile also in
  \cite[\PP{258}{272}]{artin-collected}.

\bibitem[\protect\citeauthoryear{Artin\protect\index{Artin!Emil}}{1927}]{artin%
-1927}
Emil Artin\protect\index{Artin!Emil}.
\newblock {\Ue ber die Zerlegung definiter Funktionen in
  Quadrate}\index{Artin!'s Theorem}.
\newblock {\em {\AbhandlungenmathHamburgname}}, 5:100--115, 1927.
\newblock Hamburg, Mathematisches Seminar, \Jun\,1926. Facsimile also in
  \cite[\PP{273}{288}]{artin-collected}.

\bibitem[\protect\citeauthoryear{Artin\protect\index{Artin!Emil}}{1965}]{artin%
-collected}
Emil Artin\protect\index{Artin!Emil}.
\newblock {\em Collected Papers}.
\newblock \addisonwesley, 1965.
\newblock \Ed\ by Serge Lang and John T. Tate. Reprinted 1982 by
  \springerverlag.

\bibitem[\protect\citeauthoryear{Autexier}{2005}]{sergecore}
Serge Autexier.
\newblock The {\sc core} calculus.
\newblock 2005.
\newblock In \cite[\PP{84}{98}]{twentiethCADEfive}.

\bibitem[\protect\citeauthoryear{Baaz \bgroup\&\ \egroup
  Ferm{\"u}ller}{1995}]{baazdelta}
Matthias Baaz and {\mbox{Ch}}ristian~G. Ferm{\"u}ller.
\newblock Non-elementary speedups between different versions of tableaux.
\newblock In Peter Baumgartner, Reiner H{\"a}hnle, and Joachim Posegga,
  editors, {\em \thefourthTABLEAUninetyfive}, number 918 in Lecture Notes in
  Artificial Intelligence, pages 217--230. \springerverlag, 1995.

\bibitem[\protect\citeauthoryear{Baaz \bgroup\&\ \egroup
  Leitsch}{1995}]{baazleitschcolllog}
Matthias Baaz and Alexander Leitsch.
\newblock Methods of functional extension.
\newblock {\em Collegium Logicum --- Annals of the {\goedelname\ Society}},
  1:87--122, 1995.

\bibitem[\protect\citeauthoryear{Badesa}{2004}]{badesa-loewenheim}
Calixto Badesa.
\newblock {\em The Birth of Model Theory --- \loewenheim's Theorem in the Frame
  of the Theory of Relatives}.
\newblock {\princetonunipress}, 2004.
\newblock {Translated} by \michael\ Maudsley.

\bibitem[\protect\citeauthoryear{Behmann}{1922}]{behmann}
Heinrich Behmann.
\newblock {Beitr\ae ge zur Algebra der Logik, in\esi besondere zum
  Entscheidung\esi problem}.
\newblock {\em {\MathematischeAnnalen}}, 86:163--229, 1922.
\newblock Received \Jul\,16, 1921. Corrected in \cite{behmann-correction}.

\bibitem[\protect\citeauthoryear{Behmann}{1923}]{behmann-correction}
Heinrich Behmann.
\newblock {Druckfehler\-berichtigung zu dem Aufsatz \cite{behmann}}.
\newblock {\em {\MathematischeAnnalen}}, 88:168, 1923.

\bibitem[\protect\citeauthoryear{Berka \bgroup\&\ \egroup
  Kreiser}{1973}]{logiktexte}
Karel Berka and Lothar Kreiser, editors.
\newblock {\em {Logik-Texte -- Kommentierte Au\esi wahl zur Geschichte der
  modernen Logik}}.
\newblock Akademie-Verlag, \Berlin, 1973.
\newblock \nth 2\,\rev\,\ed\ (\nth 1\,\ed\,1971; \nth
  4\,\rev\,\rev\,\ed\,1986).

\bibitem[\protect\citeauthoryear{Bernays\protect\index{Bernays, Paul}
  \bgroup\&\ \egroup Sch{\oe nfinkel}}{1928}]{bernays-schoenfinkel}
Paul Bernays\protect\index{Bernays, Paul} and Moses Sch{\oe nfinkel}.
\newblock {Zum Entscheidung\esi problem der mathematischen Logik}.
\newblock {\em {\MathematischeAnnalen}}, 99:342--372, 1928.
\newblock Received \Mar\,24, 1927.

\bibitem[\protect\citeauthoryear{Bernays\protect\index{Bernays,
  Paul}}{1928}]{grundlagenvortrag-zusatz}
Paul Bernays\protect\index{Bernays, Paul}.
\newblock {Zusatz zu \hilbert\es\ Vortrag \glqq Die Grundlagen der
  Mathematik\grqq}.
\newblock {\em {\AbhandlungenmathHamburgname}}, 6:89--92, 1928.
\newblock {English} translation {\em On the Consistency of Arithmetic} in
  \cite[\PP{485}{489}]{heijenoort-source-book}.

\bibitem[\protect\citeauthoryear{Bitbol \bgroup\&\ \egroup
  Gayon}{2006}]{Bitbol-Gayon}
Michel Bitbol and Jean Gayon, editors.
\newblock {\em L'\'epist\'emologie fran\c caise, 1830--1970}.
\newblock Presses Universitaires de France, Paris, 2006.

\bibitem[\protect\citeauthoryear{Bourbaki\protect\bourbakiindex}{1939\ff}]{bou%
rbaki}
Nicola{\es} Bourbaki\protect\bourbakiindex.
\newblock {\em {Th\'eorie des Ensembles}}.
\newblock {\'El\'ements des Math\'ematique}. Hermann, \Paris, 1939\ff.

\bibitem[\protect\citeauthoryear{Brady}{2000}]{brady}
Geraldine Brady.
\newblock {\em From {\protectedpeirceindex\peirce} to {\skolem}: A Neglected
  Chapter in the History of Logic}.
\newblock {\northholland}, 2000.

\bibitem[\protect\citeauthoryear{Brouwe\protect\index{Brouwer, L. E.
  J.}r}{1925a}]{brouwer1}
\brouwerfirstname\ Brouwe\protect\index{Brouwer, L. E. J.}r.
\newblock {Zur Begr\ue ndung der intutionistischen Mathematik I}.
\newblock {\em {\MathematischeAnnalen}}, 93:244--257, 1925.

\bibitem[\protect\citeauthoryear{Brouwe\protect\index{Brouwer, L. E.
  J.}r}{1925b}]{brouwer2}
\brouwerfirstname\ Brouwe\protect\index{Brouwer, L. E. J.}r.
\newblock {Zur Begr\ue ndung der intutionistischen Mathematik II}.
\newblock {\em {\MathematischeAnnalen}}, 95:453--472, 1925.

\bibitem[\protect\citeauthoryear{Brouwe\protect\index{Brouwer, L. E.
  J.}r}{1926}]{brouwer3}
\brouwerfirstname\ Brouwe\protect\index{Brouwer, L. E. J.}r.
\newblock {Zur Begr\ue ndung der intutionistischen Mathematik III}.
\newblock {\em {\MathematischeAnnalen}}, 96:451--488, 1926.

\bibitem[\protect\citeauthoryear{Cantor}{1932}]{cantor-collected}
Georg Cantor.
\newblock {\em {Gesammelte Abhandlungen mathematischen und philosophischen
  Inhalt\es}}.
\newblock \springerverlag, 1932.
\newblock Ed. by \zermeloname, reprinted by \georg\ Olms Verlag, \Hildesheim,
  1962.

\bibitem[\protect\citeauthoryear{Cartwright}{1965}]{hadamard-RS-memories}
Mary\protect\index{Hadamard, Jacques S.}~L. Cartwright.
\newblock {Jacques Hadamard (1865--1963)}.
\newblock {\em Biographical Memoirs of Fellows of the Royal Society},
  11:75--99, 1965.

\bibitem[\protect\citeauthoryear{Chang \bgroup\&\ \egroup
  Lee}{1973}]{chang-lee}
Chin-Liang Chang and Richard Char-Tung Lee.
\newblock {\em Symbolic logic and mechanical theorem proving}.
\newblock {\academicpress}, 1973.

\bibitem[\protect\citeauthoryear{Chevalley\protect\index{Chevalley!Claude}
  \bgroup\&\ \egroup
  Herbrand\protect\index{Herbrand!Jacques}}{1931}]{chevally-herbrand-lost-one}
Claude Chevalley\protect\index{Chevalley!Claude} and Jacques
  Herbrand\protect\index{Herbrand!Jacques}.
\newblock Groupes topologiques, groupes fuchsiens, groupes libres.
\newblock {\em \comptesrendusname}, 192:724--726, 1931.

\bibitem[\protect\citeauthoryear{Chevalley\protect\index{Chevalley!Claude}
  \bgroup\&\ \egroup Lautman\protect\index{Lautman,
  Albert}}{1931}]{herbrand-praise}
Claude\protect\index{Herbrand!Jacques}
  Chevalley\protect\index{Chevalley!Claude} and Albert
  Lautman\protect\index{Lautman, Albert}.
\newblock Notice biographique sur {\herbrand}.
\newblock {\em {Annuaire de l'Association amicale de secours des anciens
  \'el\`eves de l'\EcoleNormaleSuperieure}}, 1931:13--15, 1931.
\newblock Also in \cite[\PP{13}{15}]{herbrand-ecrits-logiques}. \ {English}
  translation {\em Biographical Note on \herbrand} in
  \cite[\PP{25}{28}]{herbrand-logical-writings}.

\bibitem[\protect\citeauthoryear{Chevalley\protect\index{Chevalley!Claude}}{19%
35}]{herbrand-thoughts}
Claude\protect\index{Herbrand!Jacques}
  Chevalley\protect\index{Chevalley!Claude}.
\newblock {Sur la pens\'ee de \herbrandname}.
\newblock {\em {\leinseignementmathematiquename}}, 34:97--102, 1935.
\newblock Also in \cite[\PP{17}{20}]{herbrand-ecrits-logiques}. \ {E}nglish
  translation {\em On \herbrand's Thought} in
  \cite[\PP{25}{28}]{herbrand-logical-writings}.

\bibitem[\protect\citeauthoryear{Chevalley\protect\index{Chevalley!Claude}}{19%
82}]{chevalley1982-herbrand-colloquium}
Claude\protect\index{Herbrand!Jacques}
  Chevalley\protect\index{Chevalley!Claude}.
\newblock {Jacques Herbrand}.
\newblock 1982.
\newblock In \cite[\PP{1}{2}]{herbrand-symposium}.

\bibitem[\protect\citeauthoryear{Craig\protect\index{Craig!William}}{1957a}]{c%
raig57:_linear_reason}
William Craig\protect\index{Craig!William}.
\newblock Linear reasoning --- a new form of the {\herbrand--\gentzen}
  {Theorem}.
\newblock {\em {\jslname}}, 22:250--268, 1957.

\bibitem[\protect\citeauthoryear{Craig\protect\index{Craig!William}}{1957b}]{c%
raig57:_three_uses_herbr_gentz_theor}
William Craig\protect\index{Craig!William}.
\newblock Three uses of the {\herbrand--\gentzen} {Theorem} in relating model
  theory and proof theory.
\newblock {\em {\jslname}}, 22:269--285, 1957.

\bibitem[\protect\citeauthoryear{Dalen\protect\index{Dalen, Dirk
  van}}{1974}]{dalen74:_review}
Dirk~van\protect\index{Herbrand!Jacques}\protect\index{Goldfarb, Warren}
  Dalen\protect\index{Dalen, Dirk van}.
\newblock Review: \herbrandname: Logical writings by \goldfarbname.
\newblock {\em The Journal of Philosophy}, 71:544--549, 1974.

\bibitem[\protect\citeauthoryear{Davis\protect\index{Davis!Martin} \bgroup\&\
  \egroup Putnam}{1960}]{davis-putnam-procedure}
Martin Davis\protect\index{Davis!Martin} and Hilary Putnam.
\newblock A computing procedure for quantification theory.
\newblock {\em J. of the ACM}, 7:201--215, 1960.

\bibitem[\protect\citeauthoryear{Davis\protect\index{Davis!Martin}}{1963}]{dav%
is-1963}
Martin Davis\protect\index{Davis!Martin}.
\newblock Eliminating the irrelevant from mechanical proofs.
\newblock In {\em Proceedings of Symposia in Applied Mathematics}, volume~15,
  pages 15--30, 1963.
\newblock Also in \cite[\Vol\,1, \PP{315}{330}]{siekmannwrightson}.

\bibitem[\protect\citeauthoryear{Dawson\protect\index{Dawson, John W.,
  Jr.}}{1991}]{dawson-reception-goedel}
John~W. Dawson\protect\index{Dawson, John W., Jr.}, \jr.
\newblock The reception of {\goedel's} incompleteness theorems.
\newblock 1991.
\newblock In \cite[\PP{84}{100}]{drucker}.

\bibitem[\protect\citeauthoryear{Dawson\protect\index{Dawson, John W.,
  Jr.}}{1993}]{goedel-herbrand}
John~W. Dawson\protect\index{Dawson, John W., Jr.}, \jr.
\newblock Prelude to recursion theory: the
  \goedel\protect\index{Goedel@G\"odel!Kurt}--\herbrand\ correspondence.
\newblock 1993.
\newblock In \cite[\PP{1}{13}]{first-goedel-symposium}.

\bibitem[\protect\citeauthoryear{Delzell}{1996}]{unwinding-artin}
Charles~N. Delzell.
\newblock {\kreisel's} unwinding of {\artin'\es} proof.
\newblock 1996.
\newblock In \cite[\PP{113}{246}]{kreiseliana}.

\bibitem[\protect\citeauthoryear{Dieudonn\'e\protect\index{Dieudonn\'e,
  Jean}}{1982}]{dieudonne-1982}
Jean Dieudonn\'e\protect\index{Dieudonn\'e, Jean}.
\newblock {\herbrandname} et la th\'eorie des nombres.
\newblock 1982.
\newblock In \cite[\PP{3}{7}]{herbrand-symposium}.

\bibitem[\protect\citeauthoryear{Dieudonn\'e\protect\index{Dieudonn\'e,
  Jean}}{1999}]{chevalley-praise}
Jean Dieudonn\'e\protect\index{Dieudonn\'e, Jean}.
\newblock {\chevalleyname}.
\newblock {\em Transformation Groups}, 4:103--113, 1999.
\newblock Dedicated to the memory of Claude
  Chevalley\protect\index{Chevalley!Claude}.

\bibitem[\protect\citeauthoryear{Dreben\protect\index{Dreben, Burton}
  \bgroup\&\ \egroup Denton}{1963}]{supplement-to-herbrand}
Burton\protect\index{Herbrand!Jacques} Dreben\protect\index{Dreben, Burton} and
  John Denton.
\newblock A supplement to \herbrand.
\newblock {\em {\jslname}}, 31(3):393--398, 1963.

\bibitem[\protect\citeauthoryear{Dreben\protect\index{Dreben, Burton}
  \bgroup\&\ \egroup Denton}{1970}]{herbrand-style-consistency-proofs}
Burton Dreben\protect\index{Dreben, Burton} and John Denton.
\newblock \herbrand-style consistency proofs.
\newblock 1970.
\newblock In \cite[\PP{419}{433}]{conference-intuitionism-proof-theory}.

\bibitem[\protect\citeauthoryear{Dreben\protect\index{Dreben, Burton}
  \bgroup\&al.\egroup }{1963}]{false-lemmas-in-herbrand}
Burton\protect\index{Herbrand!Jacques} Dreben\protect\index{Dreben, Burton},
  Peter~B. Andrew\protect\index{Andrews, Peter B.}s, and St{{\aa}}l Aanderaa.
\newblock False lemmas in \herbrand.
\newblock {\em {\bullamsname}}, 69:699--706, 1963.

\bibitem[\protect\citeauthoryear{Drucker}{1991}]{drucker}
Thomas Drucker, editor.
\newblock {\em Perspectives on the History of Mathematical Logic}.
\newblock {\birkhaeuser}, 1991.

\bibitem[\protect\citeauthoryear{Dubreil}{1983}]{Dubreil-1983-a}
Paul Dubreil.
\newblock Souvenirs d'un boursier {Rockefeller} 1929--1931.
\newblock {\em Cahiers du s\'eminaire d'histoire des math\'ematiques},
  4:61--73, 1983.

\bibitem[\protect\citeauthoryear{Dubucs \bgroup\&\ \egroup
  \'Egr\'e}{2006}]{DubucsEgre-Herbrand-PUF}
Jacques\protect\index{Herbrand!Jacques} Dubucs and Paul \'Egr\'e.
\newblock {\herbrandname}.
\newblock 2006.
\newblock In \cite[\PP{301}{322}]{Bitbol-Gayon}.

\bibitem[\protect\citeauthoryear{Enderton}{1972}]{enderton}
Herbert~B. Enderton.
\newblock {\em A Mathematical Introduction to Logic}.
\newblock {\academicpress}, 1972.

\bibitem[\protect\citeauthoryear{Ewald}{1996}]{ewald-1996}
William Ewald, editor.
\newblock {\em From {\kant} to {\hilbert} --- A source book in the foundations
  of mathematics}.
\newblock {\oxfordunipress}, 1996.

\bibitem[\protect\citeauthoryear{Feferman\protect\index{Feferman,
  Sol(omon)}}{1996}]{unwinding}
Sol(omon) Feferman\protect\index{Feferman, Sol(omon)}.
\newblock {\kreisel's ``Unwinding'' Program}.
\newblock 1996.
\newblock In \cite[\PP{247}{273}]{kreiseliana}.

\bibitem[\protect\citeauthoryear{Feigenbaum \bgroup\&\ \egroup
  Feldman}{1963}]{computers-and-thought}
Edward~A. Feigenbaum and J.~Feldman, editors.
\newblock {\em Computers and Thought}.
\newblock {\mcgrawhill}, 1963.

\bibitem[\protect\citeauthoryear{Forster\protect\index{Forster, Thomas
  E.}}{1997}]{forster-years-on}
Thomas~E. Forster\protect\index{Forster, Thomas E.}
\newblock {\quine's NF---60 years on}.
\newblock {\em American Mathematical Monthly}, 104:838--845, 1997.

\bibitem[\protect\citeauthoryear{Frege\protect\index{Frege,
  Gottlob}}{1879}]{begriffsschrift}
Gottlob Frege\protect\index{Frege, Gottlob}.
\newblock {\em {\Begriffsschrift, eine der arithmetischen nachgebildete
  Formelsprache de\es\ reinen Denken\es}}.
\newblock {Verlag von L. Nebert, \Halle}, 1879.
\newblock Corrected facsimile in \cite{begriffsschrift-und-andere}. \ Reprint
  of \PP{III}{VIII} and \PP{1}{54} in \cite[\PP{48}{106}]{logiktexte}. \
  {English} translation in \cite[\PP{1}{82}]{heijenoort-source-book}.

\bibitem[\protect\citeauthoryear{Frege\protect\index{Frege,
  Gottlob}}{1884}]{frege-grundlagen}
Gottlob Frege\protect\index{Frege, Gottlob}.
\newblock {\em {Die Grundlagen der Arithmetik}}.
\newblock Verlag von M. \& H. Marcus, \Breslau, 1884.
\newblock Reprinted 1934. Reprinted as facsimile: \georg\ Olms Verlag,
  \Hildesheim, 1990.

\bibitem[\protect\citeauthoryear{Frege\protect\index{Frege,
  Gottlob}}{1893/1903}]{frege-grundgesetze}
Gottlob Frege\protect\index{Frege, Gottlob}.
\newblock {\em Grundgesetze der Arithmetik --- \Begriffsschrift lich
  abgeleitet}.
\newblock Verlag von \hermann\ Pohle, \Jena, 1893/1903.
\newblock As facsimile with corrigenda by \christian\ Thiel: \georg\ Olms
  Verlag, \Hildesheim, 1998. English translation:
  \cite{frege-grundgesetze-furth}.

\bibitem[\protect\citeauthoryear{Frege\protect\index{Frege,
  Gottlob}}{1964a}]{frege-grundgesetze-furth}
Gottlob Frege\protect\index{Frege, Gottlob}.
\newblock {\em The Basic Laws of Arithmetic}.
\newblock \Univ\ of California Press, 1964.
\newblock English translation of \cite{frege-grundgesetze}, with an
  introduction, by {\namefont Montgomery Furth}.

\bibitem[\protect\citeauthoryear{Frege\protect\index{Frege,
  Gottlob}}{1964b}]{begriffsschrift-und-andere}
Gottlob Frege\protect\index{Frege, Gottlob}.
\newblock {\em {\Begriffsschrift\ und andere Auf\-s\ae tze}}.
\newblock \wissenschaftlichebuchgesellschaftdarmstadt, 1964.
\newblock {Zweite Au\fli age, mit \husserlname s und \scholzname' Anmerkungen,
  herau\esi gegeben von {\namefont Ignacio Angelelli}}.

\bibitem[\protect\citeauthoryear{Gabbay \bgroup\&\ \egroup
  Woods}{2004\ff}]{handbook-of-the-history-of-logic}
Dov Gabbay and John Woods, editors.
\newblock {\em Handbook of the History of Logic}.
\newblock \northholland, 2004\ff.

\bibitem[\protect\citeauthoryear{Gentzen}{1935}]{gentzen}
Gerhard Gentzen.
\newblock {Untersuchungen \ue ber das logische Schlie\sz en}.
\newblock {\em Mathematische Zeitschrift}, 39:176--210,405--431, 1935.
\newblock Also in \cite[\PP{192}{253}]{logiktexte}. {English} translation in
  \cite{gentzen-collected}.

\bibitem[\protect\citeauthoryear{Gentzen}{1936}]{gentzenfirstconsistent}
Gerhard Gentzen.
\newblock {Die Wider\-spruch\esi frei\-heit der reinen Zahlentheorie}.
\newblock {\em {\MathematischeAnnalen}}, 112:493--565, 1936.
\newblock {English} translation in \cite{gentzen-collected}.

\bibitem[\protect\citeauthoryear{Gentzen}{1938}]{gentzenconsistent}
Gerhard Gentzen.
\newblock {Die gegenw\ae rtige Lage in der mathematischen
  Grund\-lagen\-forschung -- Neue Fassung des Wider\-spruch\esi frei\-heit\esi
  beweise\es\ f\ue r die reine Zahlentheorie}.
\newblock {\em {Forschungen zur Logik und zur Grundlegung der exakten
  Wissenschaften, Neue Folge}}, 4:3--44, 1938.
\newblock {Reprinted as facsimile by
  \wissenschaftlichebuchgesellschaftdarmstadt, Verlag von S. Hirzel, Stuttgart.
  \ {English} translation in \cite{gentzen-collected}}.

\bibitem[\protect\citeauthoryear{Gentzen}{1943}]{gentzenepsilon}
Gerhard Gentzen.
\newblock {Bewei\esi barkeit und Unbewei\esi barkeit von Anfang\esi f\ae llen
  der tran\esi finiten Induktion in der reinen Zahlentheorie}.
\newblock {\em {\MathematischeAnnalen}}, 119:140--161, 1943.
\newblock {Received \Jul\,9, 1942. English translation in
  \cite{gentzen-collected}}.

\bibitem[\protect\citeauthoryear{Gentzen}{1969}]{gentzen-collected}
Gerhard Gentzen.
\newblock {\em The Collected Papers of \gentzenname}.
\newblock {\northholland}, 1969.
\newblock \Ed\ by \szaboname.

\bibitem[\protect\citeauthoryear{Gilmore}{1960}]{gilmore-1960}
Paul~C. Gilmore.
\newblock A proof method for quantification theory: Its justification and
  realization.
\newblock {\em IBM Journal Research and Development}, 4:28--35, 1960.
\newblock Also in \cite[\Vol\,I, \PP{151}{161}]{siekmannwrightson}.

\bibitem[\protect\citeauthoryear{G{\oe
  del}\protect\index{Goedel@G\"odel!Kurt}}{1930}]{goedel-completeness}
Kurt G{\oe del}\protect\index{Goedel@G\"odel!Kurt}.
\newblock {Die Vollst\ae ndigkeit der Axiome des logischen Funktionen\-kalk\ue
  ls}.
\newblock {\em {\monatsheftempname}}, 37:349--360, 1930.
\newblock With {English} translation also in \cite[\Vol\,I,
  \PP{102}{123}]{goedelcollected}.

\bibitem[\protect\citeauthoryear{G{\oe
  del}\protect\index{Goedel@G\"odel!Kurt}}{1931}]{goedel}
Kurt G{\oe del}\protect\index{Goedel@G\"odel!Kurt}.
\newblock {\Ue ber formal unentscheidbare S\ae tze der \PM\ und verwandter
  Sy\esi teme I}.
\newblock {\em {\monatsheftempname}}, 38:173--198, 1931.
\newblock With {English} translation also in \cite[\Vol\,I,
  \PP{145}{195}]{goedelcollected}. {English} translation also in
  \cite[\PP{596}{616}]{heijenoort-source-book} and in \cite{goedel-meltzer}.

\bibitem[\protect\citeauthoryear{G{\oe
  del}\protect\index{Goedel@G\"odel!Kurt}}{1934}]{goedel-lecture-notes}
Kurt G{\oe del}\protect\index{Goedel@G\"odel!Kurt}.
\newblock {\em On Undecidable Propositions of Formal Mathematical Systems}.
\newblock The \Inst\ for Advanced Study, 1934.
\newblock {L}ecture notes by {\kleenename} and {\rossername}. With {English}
  translation also in \cite[\Vol\,I, \PP{346}{372}]{goedelcollected}.

\bibitem[\protect\citeauthoryear{G{\oe
  del}\protect\index{Goedel@G\"odel!Kurt}}{1939}]{goedel-consistency-continuum}
Kurt G{\oe del}\protect\index{Goedel@G\"odel!Kurt}.
\newblock Consistency proof for the generalized continuum hypothesis.
\newblock In {\em \Proc\ of the National Academy of Sciences, U.S.A., 25},
  pages 220--224, 1939.
\newblock Also in \cite[\Vol\,II, \PP{28}{32}]{goedelcollected}.

\bibitem[\protect\citeauthoryear{G{\oe
  del}\protect\index{Goedel@G\"odel!Kurt}}{1962}]{goedel-meltzer}
Kurt G{\oe del}\protect\index{Goedel@G\"odel!Kurt}.
\newblock {\em On formally undecidable propositions of {\PM} and related
  systems}.
\newblock Basic Books, \NewYork, 1962.
\newblock English translation of \cite{goedel} by {\sc B. Meltzer}. With an
  introduction by {\sc R. B. Braithwaite}. \nth 2\,\ed\ by Dover Publications,
  1992.

\bibitem[\protect\citeauthoryear{G{\oe
  del}\protect\index{Goedel@G\"odel!Kurt}}{1986ff.}]{goedelcollected}
Kurt G{\oe del}\protect\index{Goedel@G\"odel!Kurt}.
\newblock {\em Collected Works}.
\newblock {\oxfordunipress}, 1986ff.
\newblock \Ed\ by \fefermanname\protect\index{Feferman, Sol(omon)},
  \dawsonname\protect\index{Dawson, John W., Jr.}, \goldfarbname,
  \heijenoortname\protect\index{Heijenoort!Jean van}, \kleenename,
  \parsonsname, \siegname, \etalabbrev.

\bibitem[\protect\citeauthoryear{Goldfarb\protect\index{Goldfarb, Warren}
  \bgroup\&\ \egroup Scanlon\protect\index{Scanlon, Thomas M.,
  Jr.}}{1974}]{goldfarb-herbrand-consistency}
Warren Goldfarb\protect\index{Goldfarb, Warren} and Thomas~M.
  Scanlon\protect\index{Scanlon, Thomas M., Jr.}, \jr.
\newblock The {$\omega$}-consistency of number theory via \herbrand's theorem.
\newblock {\em {\jslname}}, 39:678--692, 1974.

\bibitem[\protect\citeauthoryear{Goldfarb\protect\index{Goldfarb,
  Warren}}{1993}]{goldfarb-herbrand-goedel}
Warren Goldfarb\protect\index{Goldfarb, Warren}.
\newblock \herbrand's error and \goedel's correction.
\newblock {\em Modern Logic}, 3:103--118, 1993.

\bibitem[\protect\citeauthoryear{Gonseth}{1941}]{gonseth-1941}
Ferdinand Gonseth, editor.
\newblock {\em Les Entretiens de {Z}urich sur les Fondements et la M\'ethode
  des Sciences Math\'e\-matiques, {\Dec\,6--9}, 1938}. S. A. Leemann fr\`eres
  {\&} Cie., \Zuerich, 1941.

\bibitem[\protect\citeauthoryear{Gove}{1993}]{webster}
Philipp~Babcock Gove, editor.
\newblock {\em Webster's Third New International Dictionary}.
\newblock Merriam-Webster, Springfield (MA), 1993.
\newblock Principal copyright 1961.

\bibitem[\protect\citeauthoryear{Hadamar\protect\index{Hadamard, Jacques
  S.}d}{1949}]{hadamard-psychology}
Jacques~S. Hadamar\protect\index{Hadamard, Jacques S.}d.
\newblock {\em The Psychology of Invention in the Mathematical Field}.
\newblock {\princetonunipress}, 1949.
\newblock \nth 2\,\rev\,\ed\ (\nth 1\,\ed\,1945).

\bibitem[\protect\citeauthoryear{Hasse\protect\index{Hasse, Helmut} \bgroup\&\
  \egroup {Herbrand \sr}\protect\index{Herbrand!Jacques, Sr.\ (Herbrand's
  father)}}{1931}]{hasse-herbrand-senior-correspondence}
Helmut Hasse\protect\index{Hasse, Helmut} and Jacques {Herbrand
  \sr}\protect\index{Herbrand!Jacques, Sr.\ (Herbrand's father)}.
\newblock Letters exchanged between \hassename\ and \jacques\ \herbrand\ \sr.
\newblock Available from the Nieders\ae chsische Staat\es- und Universit\ae
  t\esi bibliothek -- Abteilung f\ue r Handschriften und seltene Drucke,
  \Goettingen, Germany, 1931.

\bibitem[\protect\citeauthoryear{Heijenoort\protect\index{Heijenoort!Jean
  van}}{1968}]{heijenoort-tree-herbrand}
Jean~van\protect\index{Herbrand!Jacques}
  Heijenoort\protect\index{Heijenoort!Jean van}.
\newblock On the relation between the falsifiability tree method and the
  {\herbrand} method in quantification theory.
\newblock Unpublished typescript, \Nov\,20, 1968, \PPcount{12};
  \heijenoortname\ Papers, 1946--1988, Archives of American Mathematics, Center
  for American History, \Univ\ of Texas at Austin, Box\,3.8/86-33/1. \ Copy in
  \anellis\ Archives\protect\index{Anellis!Archives}, 1968.

\bibitem[\protect\citeauthoryear{Heijenoort\protect\index{Heijenoort!Jean
  van}}{1971a}]{heijenoort-source-book}
Jean~van Heijenoort\protect\index{Heijenoort!Jean van}.
\newblock {\em From {\frege} to {\goedel}: A Source Book in Mathematical Logic,
  1879--1931}.
\newblock {\harvardunipress}, 1971.
\newblock {\nth 2\,\rev\ \ed\ (\nth 1\,\ed\,1967)}.

\bibitem[\protect\citeauthoryear{Heijenoort\protect\index{Heijenoort!Jean
  van}}{1971b}]{heijenoort-mints}
Jean~van Heijenoort\protect\index{Heijenoort!Jean van}.
\newblock Reviews of articles by \mintsname.
\newblock {\em {\jslname}}, 36:524--528, 1971.

\bibitem[\protect\citeauthoryear{Heijenoort\protect\index{Heijenoort!Jean
  van}}{1975}]{heijenoort-herbrand}
Jean~van\protect\index{Herbrand!Jacques}
  Heijenoort\protect\index{Heijenoort!Jean van}.
\newblock \herbrand.
\newblock Unpublished typescript, \May\,18, 1975, \PPcount{15};
  \heijenoortname\ Papers, 1946--1988, Archives of American Mathematics, Center
  for American History, \Univ\ of Texas at Austin, Box\,3.8/86-33/1. \ Copy in
  \anellis\ Archives\protect\index{Anellis!Archives}, 1975.

\bibitem[\protect\citeauthoryear{Heijenoort\protect\index{Heijenoort!Jean
  van}}{1982}]{heijenoort-oeuvre-herbrand}
Jean~van\protect\index{Herbrand!Jacques}
  Heijenoort\protect\index{Heijenoort!Jean van}.
\newblock {L'\oefranz uvre} logique de {\herbrand} et son contexte historique.
\newblock 1982.
\newblock In \cite[\PP{57}{85}]{herbrand-symposium}.

\bibitem[\protect\citeauthoryear{Heijenoort\protect\index{Heijenoort!Jean
  van}}{1986a}]{heijenoort-absolutism-relativism}
Jean~van Heijenoort\protect\index{Heijenoort!Jean van}.
\newblock Absolutism and relativism in logic.
\newblock 1986.
\newblock In \cite[\PP{75}{83}]{heijenoort-selected-essays}.

\bibitem[\protect\citeauthoryear{Heijenoort\protect\index{Heijenoort!Jean
  van}}{1986b}]{heijenoort-selected-essays}
Jean~van Heijenoort\protect\index{Heijenoort!Jean van}.
\newblock {\em Selected Essays}.
\newblock Bibliopolis, Napoli, copyright 1985. Also published by Librairie
  Philosophique J. Vrin, \Paris, 1986, 1986.

\bibitem[\protect\citeauthoryear{Heijenoort\protect\index{Heijenoort!Jean
  van}}{1986c}]{heijenoort-work-herbrand}
Jean~van\protect\index{Herbrand!Jacques}
  Heijenoort\protect\index{Heijenoort!Jean van}.
\newblock \herbrand's work in logic and its historical context.
\newblock 1986.
\newblock In \cite[\PP{99}{121}]{heijenoort-selected-essays}.

\bibitem[\protect\citeauthoryear{Herbrand\protect\index{Herbrand!Jacques}
  \bgroup\&\ \egroup
  Chevalley\protect\index{Chevalley!Claude}}{1931}]{herbrand-chevalley}
Jacques Herbrand\protect\index{Herbrand!Jacques} and Claude
  Chevalley\protect\index{Chevalley!Claude}.
\newblock Nouvelle d\'e\-mon\-stra\-tion du th\'eor\`eme d'existence en
  th\'eorie du corps de classes.
\newblock {\em {\comptesrendusname}}, 193:814--815, 1931.

\bibitem[\protect\citeauthoryear{Herbrand\protect\index{Herbrand!Jacques}}{192%
8}]{herbrand-first}
Jacques Herbrand\protect\index{Herbrand!Jacques}.
\newblock {Sur la th\'eorie de la d\'e\-mon\-stra\-tion}.
\newblock {\em {\comptesrendusname}}, 186:1274--1276, 1928.
\newblock Also in \cite[\PP{21}{23}]{herbrand-ecrits-logiques}. \ Annotated
  {English} translation {\em On Proof Theory}\/ by
  \goldfarbname\protect\index{Goldfarb, Warren}\ with an extended note by
  \drebenname\protect\index{Dreben, Burton}\ and \goldfarb\ in
  \cite[\PP{29}{34}]{herbrand-logical-writings}.

\bibitem[\protect\citeauthoryear{Herbrand\protect\index{Herbrand!Jacques}}{192%
9a}]{herbrand-second}
Jacques Herbrand\protect\index{Herbrand!Jacques}.
\newblock Non-contradiction des axiomes arithm\'etiques.
\newblock {\em {\comptesrendusname}}, 188:303--304, 1929.
\newblock Also in \cite[\PP{25}{26}]{herbrand-ecrits-logiques}. \ Annotated
  {English} translation {\em The Consistency of the Axioms of Arithmetic} by
  \goldfarbname\protect\index{Goldfarb, Warren}\ in
  \cite[\PP{35}{37}]{herbrand-logical-writings}. \bibcrit{An abstract of
  \citep[\litchapref 4]{herbrand-PhD}}.

\bibitem[\protect\citeauthoryear{Herbrand\protect\index{Herbrand!Jacques}}{192%
9b}]{herbrand-lost-one}
Jacques Herbrand\protect\index{Herbrand!Jacques}.
\newblock Recherche des solutions born{\'e}es de certaines {\'e}quations
  fonctionnelles.
\newblock {\em \comptesrendusname}, 189:669--671, 811, 1929.

\bibitem[\protect\citeauthoryear{Herbrand\protect\index{Herbrand!Jacques}}{192%
9c}]{herbrand-fourth}
Jacques Herbrand\protect\index{Herbrand!Jacques}.
\newblock Sur le probl\'eme fondamental des math\'ematiques.
\newblock {\em {\comptesrendusname}}, 189:554--556+720, 1929.
\newblock Also in \cite[\PP{31}{33}]{herbrand-ecrits-logiques}. \ Annotated
  {English} translation {\em On the Fundamental Problem of Mathematics} by
  \goldfarbname\protect\index{Goldfarb, Warren}\ in
  \cite[\PP{41}{43}]{herbrand-logical-writings}. \bibcrit{An abstract of
  \citep{herbrand-fundamental-problem}}.

\bibitem[\protect\citeauthoryear{Herbrand\protect\index{Herbrand!Jacques}}{192%
9d}]{herbrand-third}
Jacques Herbrand\protect\index{Herbrand!Jacques}.
\newblock Sur quelques propri\'et\'es des propositions vraies et leurs
  applications.
\newblock {\em {\comptesrendusname}}, 188:1076--1078, 1929.
\newblock Also in \cite[\PP{27}{29}]{herbrand-ecrits-logiques}. \ Annotated
  English translation {\em On several properties of true propositions and their
  applications} by \goldfarbname\protect\index{Goldfarb, Warren}\ in
  \cite[\PP{38}{40}]{herbrand-logical-writings}. \bibcrit{An abstract of
  \citep[\litchapwithsectref 5 6]{herbrand-PhD}}.

\bibitem[\protect\citeauthoryear{Herbrand\protect\index{Herbrand!Jacques}}{193%
0a}]{herbrand-lost-two}
Jacques Herbrand\protect\index{Herbrand!Jacques}.
\newblock D{\'e}termination des groupes de ramification d'un corps {\`a} partir
  de ceux d'un sur-corps.
\newblock {\em \comptesrendusname}, 191:980--982, 1930.

\bibitem[\protect\citeauthoryear{Herbrand\protect\index{Herbrand!Jacques}}{193%
0b}]{herbrand-PhD}
Jacques Herbrand\protect\index{Herbrand!Jacques}.
\newblock {\em \herbrandPhDtitle}.
\newblock PhD thesis, Universit\'e de Paris, 1930.
\newblock {Th\`eses} pr\'esent\'ees \`a la facult\'e des Sciences de Paris pour
  obtenir le grade de docteur \`es sciences math\'ematiques --- \frenchnth 1
  \nolinebreak th\`ese: Recherches sur la th\'eorie de la d\'emonstration ---
  \frenchnth 2 \nolinebreak th\`ese: Propositions donn\'ees par la facult\'e,
  Les \'equations de Fredholm --- Soutenues le 1930 devant la commission
  d'examen --- Pr\'esident: M. \vessiot, Examinateurs: MM. {\namefont Denjoy,
  Frechet} --- Vu et approuv\'e, \Paris, le 20\,Juin\,1929, Le doyen de la
  facult\'e des Sciences, {\namefont C. Maurain} --- Vu et permis d'imprimer,
  \Paris, le 20\,Juin\,1929, Le recteur de l'Academie de \Paris, {\namefont S.
  Charlety} --- No.\,d'ordre\,2121, S\'erie\,A, No.\,de\,S\'erie\,1252 ---
  Imprimerie J. Dziewulski, Varsovie --- \Univ\ de \Paris. \ Also in Prace
  \WarsawScientificSocietyIII\ Nauk Matematyczno-Fizychnych, Nr.\,33,
  \Warszawa. \ Also in \cite[\PP{35}{153}]{herbrand-ecrits-logiques}. \
  Annotated {E}nglish translation {\em Investigations in Proof Theory}\/ by
  \goldfarbname\protect\index{Goldfarb, Warren}\ (\litchapfromtoref 1 4) and
  \drebenname\protect\index{Dreben, Burton}\ and \heijenoortname\ (\litchapref
  5) with a brief introduction by \goldfarb\ and extended notes by \goldfarb\
  \mbox{(\litnotefromtoref A C, K--M, O)}, \dreben\ (\litnotefromtoref F I),
  \dreben\ and \goldfarb\ (\litnoterefss D J N), and \dreben, \huffname, and
  \hailperinname\ (\litnoteref E) in
  \cite[\PP{44}{202}]{herbrand-logical-writings}. \ {E}nglish translation of
  \litsectref 5 with a different introduction by \heijenoort\ and some
  additional extended notes by \dreben\ also in
  \cite[\PP{525}{581}]{heijenoort-source-book}. \ \bibcrit{\herbrand's
  \PhDthesis, his cardinal work, dated \herbrandPhDdating; submitted at the
  \Univ\ of \Paris; defended at the Sorbonne \herbrandPhDdefensedate; printed
  in \WarszawaEnglish, 1930.}

\bibitem[\protect\citeauthoryear{Herbrand\protect\index{Herbrand!Jacques}}{193%
0c}]{herbrand-1930b}
Jacques Herbrand\protect\index{Herbrand!Jacques}.
\newblock Nouvelle d\'emonstration et g\'en\'eralisation d'un th\'eor\`eme de
  {Minkowski}.
\newblock {\em {\comptesrendusname}}, 191:1282--1285, 1930.

\bibitem[\protect\citeauthoryear{Herbrand\protect\index{Herbrand!Jacques}}{193%
0d}]{herbrand-hilbert}
Jacques\protect\index{Hilbert!David} Herbrand\protect\index{Herbrand!Jacques}.
\newblock Les bases de la logique hilbertienne.
\newblock {\em {Revue de M\'eta\-physique et de Morale}}, 37:243--255, 1930.
\newblock Also in \cite[\PP{155}{166}]{herbrand-ecrits-logiques}. \ Annotated
  {English} translation {\em The Principles of Hilbert's Logic} in
  \cite[\PP{203}{214}]{herbrand-logical-writings}. \ \bibcrit{\herbrand's
  personal view on meta-mathematics and \hilbertsprogram}.

\bibitem[\protect\citeauthoryear{Herbrand\protect\index{Herbrand!Jacques}}{193%
1a}]{herbrand-note-PhD}
Jacques Herbrand\protect\index{Herbrand!Jacques}.
\newblock Note non signe\'e sur \cite{herbrand-PhD}.
\newblock {\em Annales de l'Universit\'e de Paris}, 6:186--189, 1931.
\newblock Also in \cite[\PP{209}{214}]{herbrand-ecrits-logiques}. \ {English}
  translation {\em Unsigned Note on \herbrand's Thesis written by \herbrand\
  himself}\/ in \cite[\PP{272}{276}]{herbrand-logical-writings}. \ \bibcrit{The
  philosophy of metamathematics in the \hilbert\ school (roughly following
  \citep{grundlagenvortrag}) and the positioning of \citep{herbrand-PhD} in it
  are sketched for non-experts}.

\bibitem[\protect\citeauthoryear{Herbrand\protect\index{Herbrand!Jacques}}{193%
1b}]{herbrand-note-hadamard}
Jacques Herbrand\protect\index{Herbrand!Jacques}.
\newblock Notice pour {\jacques\ \hadamard}.
\newblock 1931.
\newblock In \cite[\PP{215}{219}]{herbrand-ecrits-logiques}. \ With annotations
  and a brief introduction by \heijenoortname. \ {E}nglish translation {\em
  Note for \jacques\ \hadamard}\/ by \goldfarbname\ in
  \cite[\PP{277}{281}]{herbrand-logical-writings}. \ \bibcrit{Abstracts for
  non-experts of \herbrand's mathematical contributions addressed to his
  presenter to the Academy of Sciences}.

\bibitem[\protect\citeauthoryear{Herbrand\protect\index{Herbrand!Jacques}}{193%
1c}]{herbrand-corps-abstract}
Jacques Herbrand\protect\index{Herbrand!Jacques}.
\newblock Sur la th\'eorie des corps de nombres de degr\'e infini.
\newblock {\em {\comptesrendusname}}, 193:504--506, 1931.
\newblock \bibcrit{{Abstract} of
  \makeaciteoftwo{herbrand-corps-I}{herbrand-corps-II}}.

\bibitem[\protect\citeauthoryear{Herbrand\protect\index{Herbrand!Jacques}}{193%
1d}]{herbrand-group}
Jacques Herbrand\protect\index{Herbrand!Jacques}.
\newblock Sur la th\'eorie des groupes de d\'ecomposition, d'inertie et de
  ramication.
\newblock {\em {\jmathpuresapplname}}, 9:481--498, 1931.

\bibitem[\protect\citeauthoryear{Herbrand\protect\index{Herbrand!Jacques}}{193%
1e}]{herbrand-fundamental-problem}
Jacques Herbrand\protect\index{Herbrand!Jacques}.
\newblock Sur le probl\`eme fondamental de la logique math\'ematique.
\newblock {\em Revue de M\'etaphysique et de Morale}, 24:12--56, 1931.
\newblock Also in \cite[\PP{167}{207}]{herbrand-ecrits-logiques}. \ Annotated
  {English} translation {\em On the Fundamental Problem of Mathematical Logic}
  in \cite[\PP{215}{271}]{herbrand-logical-writings}.

\bibitem[\protect\citeauthoryear{Herbrand\protect\index{Herbrand!Jacques}}{193%
1f}]{herbrand-lost-three}
Jacques Herbrand\protect\index{Herbrand!Jacques}.
\newblock Sur les unit{\'e}s d'un corps alg{\'e}brique.
\newblock {\em \comptesrendusname}, 192:24--27+188, 1931.

\bibitem[\protect\citeauthoryear{Herbrand\protect\index{Herbrand!Jacques}}{193%
2a}]{herbrand-consistency-of-arithmetic}
Jacques Herbrand\protect\index{Herbrand!Jacques}.
\newblock Sur la non-contradiction de {l'Arithmetique}.
\newblock {\em {\jreineundangewandtemathematikname}}, 166:1--8, 1932.
\newblock Received \Jul\,27, 1931. \ Without \hasse's obituary also in
  \cite[\PP{221}{232}]{herbrand-ecrits-logiques}. \ Annotated {English}
  translation {\em On the Consistency of Arithmetic} in
  \cite[\PP{618}{628}]{heijenoort-source-book}. \ Annotated {English}
  translation also in \cite[\PP{282}{298}]{herbrand-logical-writings}. \
  \bibcrit{Consistency of arithmetic, foreshadowing of (total) recursive
  functions, discussion of \citep{goedel}}.

\bibitem[\protect\citeauthoryear{Herbrand\protect\index{Herbrand!Jacques}}{193%
2b}]{herbrand-1932}
Jacques Herbrand\protect\index{Herbrand!Jacques}.
\newblock Sur les classes des corps circulaires.
\newblock {\em {\jmathpuresapplname}}, 9:417--441, 1932.

\bibitem[\protect\citeauthoryear{Herbrand\protect\index{Herbrand!Jacques}}{193%
2c}]{herbrand-1932a}
Jacques Herbrand\protect\index{Herbrand!Jacques}.
\newblock Sur les th\'eor\`emes du genre principal et des id\'eaux principaux.
\newblock {\em {\AbhandlungenmathHamburgname}}, 9:84--92, 1932.

\bibitem[\protect\citeauthoryear{Herbrand\protect\index{Herbrand!Jacques}}{193%
2d}]{herbrand-corps-I}
Jacques Herbrand\protect\index{Herbrand!Jacques}.
\newblock Th\'eorie arithm\'etique des corps de nombres de degr\'e infini ---
  {I}.~{Extensions} alg\'ebriques finies de corps infinis.
\newblock {\em {\MathematischeAnnalen}}, 106:473--501, 1932.

\bibitem[\protect\citeauthoryear{Herbrand\protect\index{Herbrand!Jacques}}{193%
2e}]{herbrand-discriminant}
Jacques Herbrand\protect\index{Herbrand!Jacques}.
\newblock Une propri\'et\'e du discriminant des corps alg\'ebriques.
\newblock {\em Annales Scientifiques de l'\EcoleNormaleSuperieure},
  S\'erie\,3,\,49:105--112, 1932.

\bibitem[\protect\citeauthoryear{Herbrand\protect\index{Herbrand!Jacques}}{193%
2f}]{herbrand-algebraic-functions}
Jacques Herbrand\protect\index{Herbrand!Jacques}.
\newblock {Zur Theorie der algebraischen Funktionen}.
\newblock {\em {\MathematischeAnnalen}}, 106:502, 1932.
\newblock From letters to \noethername. Received \Dec\,23, 1931.

\bibitem[\protect\citeauthoryear{Herbrand\protect\index{Herbrand!Jacques}}{193%
3}]{herbrand-corps-II}
Jacques Herbrand\protect\index{Herbrand!Jacques}.
\newblock Th\'eorie arithm\'etique des corps de nombres de degr\'e infini ---
  {II}.~{Extensions} alg\'ebriques de degr\'e infini.
\newblock {\em {\MathematischeAnnalen}}, 108:699--717, 1933.
\newblock \Ed\ and with a last paragraph by
  \chevalleyname\protect\index{Chevalley!Claude}.

\bibitem[\protect\citeauthoryear{Herbrand\protect\index{Herbrand!Jacques}}{193%
6}]{herbrand-1936}
Jacques Herbrand\protect\index{Herbrand!Jacques}.
\newblock {\em Le D\'eveloppement Moderne de la Th\'eorie des Corps
  Alg\'ebriques --- Corps de classes et lois de r\'eciprocit\'e}.
\newblock M\'emorial des Sciences Math\'ematiques, Fascicule\,LXXV.
  {\gauthiervillars}, 1936.
\newblock \Ed\ and with an appendix by
  \chevalleyname\protect\index{Chevalley!Claude}.

\bibitem[\protect\citeauthoryear{Herbrand\protect\index{Herbrand!Jacques}}{196%
8}]{herbrand-ecrits-logiques}
Jacques Herbrand\protect\index{Herbrand!Jacques}.
\newblock {\em \'Ecrits Logiques}.
\newblock Presses Universitaires de France, Paris, 1968.
\newblock \Ed\ by Jean van Heijenoort. {E}nglish translation is
  \citep{herbrand-logical-writings}. \bibcrit{\/\herbrand's logical writings,
  faultily retyped}.

\bibitem[\protect\citeauthoryear{Herbrand\protect\index{Herbrand!Jacques}}{197%
1}]{herbrand-logical-writings}
Jacques Herbrand\protect\index{Herbrand!Jacques}.
\newblock {\em Logical Writings}.
\newblock {\harvardunipress}, 1971.
\newblock \Ed\ by \goldfarbname\protect\index{Goldfarb, Warren}. Translation of
  \citep{herbrand-ecrits-logiques} with additional annotations, brief
  introductions, and extended notes by \goldfarb,
  \drebenname\protect\index{Dreben, Burton}, and \heijenoortname. \
  \bibcrit{Still the best source on \herbrand's logical writings today}.

\bibitem[\protect\citeauthoryear{Heyting\protect\index{Heyting,
  Arend}}{1930a}]{heyting-1930-logic}
Arend Heyting\protect\index{Heyting, Arend}.
\newblock {Die formalen Regeln der intuitionistischen Logik}.
\newblock {\em {Sitzung\esi berichte der Preu\sz i\-schen Akademie der
  Wissenschaften, \Berlin, Physikalisch-mathematische Klasse II}}, 1930:42--56,
  1930.
\newblock Short version also in \cite{logiktexte}, \PP{173}{178}.

\bibitem[\protect\citeauthoryear{Heyting\protect\index{Heyting,
  Arend}}{1930b}]{heyting-1930-mathematics}
Arend Heyting\protect\index{Heyting, Arend}.
\newblock {Die formalen Regeln der intuitionistischen Mathematik}.
\newblock {\em {Sitzung\esi berichte der Preu\sz i\-schen Akademie der
  Wissenschaften, \Berlin, Physikalisch-mathematische Klasse II}}, 1930:57--71,
  158--169, 1930.

\bibitem[\protect\citeauthoryear{Heyting\protect\index{Heyting,
  Arend}}{1971}]{heyting}
Arend Heyting\protect\index{Heyting, Arend}.
\newblock {\em Intuitionism --- An Introduction}.
\newblock {\northholland}, 1971.
\newblock \nth 3\,\rev\,\ed\ (\nth 1\,\ed\,1956).

\bibitem[\protect\citeauthoryear{Hilbert \bgroup\&\ \egroup
  Bernays}{1968/70}]{grundlagen}
David Hilbert and Paul Bernays.
\newblock {\em {Die Grundlagen der Mathematik}}.
\newblock \springerverlag, 1968/70.
\newblock \nth 2\,\rev\,\ed\ (\nth 1\,\ed\,1934/39).

\bibitem[\protect\citeauthoryear{Hilbert\protect\index{Hilbert!David}
  \bgroup\&\ \egroup Ackermann\protect\ackermannindex}{1928}]{grundzuege}
David Hilbert\protect\index{Hilbert!David} and Wilhelm
  Ackermann\protect\ackermannindex.
\newblock {\em {Grundz\ue ge der theoretischen Logik}}.
\newblock \springerverlag, 1928.
\newblock \nth 1\,\ed, the final version in a serious of three thorough
  revisions is \cite{grundzuege-vierte}.

\bibitem[\protect\citeauthoryear{Hilbert\protect\index{Hilbert!David}
  \bgroup\&\ \egroup
  Ackermann\protect\ackermannindex}{1959}]{grundzuege-vierte}
David Hilbert\protect\index{Hilbert!David} and Wilhelm
  Ackermann\protect\ackermannindex.
\newblock {\em {Grundz\ue ge der theoretischen Logik}}.
\newblock \springerverlag, 1959.
\newblock \nth 4\,\ed, most thoroughly revised edition of \cite{grundzuege}.

\bibitem[\protect\citeauthoryear{Hilbert\protect\index{Hilbert!David}}{1899}]{%
grundlagen-der-geometrie}
David Hilbert\protect\index{Hilbert!David}.
\newblock {Grundlagen der Geometrie}.
\newblock 1899.
\newblock In \cite[\PP{1}{92}]{anon-1899}. \nth 1\,\ed\ without \appendixes.
  Reprinted in \cite[\PP{436}{525}]{hilbert-2004}. \bibcrit{Last edition of
  ``Grundlagen der Geometrie'' by \hilbert\ is
  \cite{grundlagen-der-geometrie-siebte}, which is also most complete regarding
  the appendixes. Last three editions by\/ \bernaysname\ are
  \makeaciteofthree{grundlagen-der-geometrie-neunte}{grundlagen-der-geometrie-%
zehnte}{grundlagen-der-geometrie-elfte}, which are also most complete regarding
  supplements and figures. Its first appearance as a separate book was the
  French translation \cite{principes-fondamentaux-de-la-geometrie}. Two
  substantially different {English} translations are
  \cite{foundations-of-geometry} and \cite{foundations-of-geometry-second}}.

\bibitem[\protect\citeauthoryear{Hilbert\protect\index{Hilbert!David}}{1922}]{%
neubegruendung}
David Hilbert\protect\index{Hilbert!David}.
\newblock {Neubegr\ue ndung der Mathematik (Erste Mitteilung)}.
\newblock {\em {\AbhandlungenmathHamburgname}}, 1:157--177, 1922.
\newblock Reprinted with additional notes in \cite[\Vol\,3,
  \PP{157}{177}]{hilbert-gesammelte}. {English} translation in
  \citep[\PP{1115}{1134}]{ewald-1996}.

\bibitem[\protect\citeauthoryear{Hilbert\protect\index{Hilbert!David}}{1923}]{%
grundlagen-der-geometrie-sechste}
David Hilbert\protect\index{Hilbert!David}.
\newblock {\em {Grundlagen der Geometrie. --- Sechste unver\ae nderte Au\fli
  age. Anastati\-scher Nachdruck. Mit zahlreichen in den Text gedruckten
  Figuren}}.
\newblock Verlag und Druck von B. G. Teubner, \Leipzig, \Berlin, 1923.
\newblock {\nth 6}\,\rev\,\extd\,\ed\ of \cite{grundlagen-der-geometrie},
  anastatic reprint of \cite{grundlagen-der-geometrie-fuenfte}.

\bibitem[\protect\citeauthoryear{Hilbert\protect\index{Hilbert!David}}{1926}]{%
unendliche}
David Hilbert\protect\index{Hilbert!David}.
\newblock {\Ue ber das Unendliche --- Vortrag, gehalten am 4.\,Juni\,1925
  gelegentlich einer zur Ehrung de\es\ Andenken\es\ an \weierstrass\ von der
  West\-f\ae lischen \Math\ \Ges\ veranstalteten Mathematiker-Zusammenkunft in
  M\ue nster i. W.}
\newblock {\em {\MathematischeAnnalen}}, 95:161--190, 1926.
\newblock Received \Jun\,24, 1925. \ Reprinted as Appendix\,VIII of
  \cite{grundlagen-der-geometrie-siebte}. \ {E}nglish translation {\em On the
  infinite} by \bauermengelbergname\protect\index{Bauer-Mengelberg, Stefan}
  with an introduction by \heijenoortname\ in
  \cite[\PP{367}{392}]{heijenoort-source-book}.

\bibitem[\protect\citeauthoryear{Hilbert\protect\index{Hilbert!David}}{1928}]{%
grundlagenvortrag}
David Hilbert\protect\index{Hilbert!David}.
\newblock {Die Grundlagen der Mathematik --- Vortrag, gehalten auf Einladung
  des Mathematischen Seminars im Juli 1927 in \Hamburg}.
\newblock {\em {\AbhandlungenmathHamburgname}}, 6:65--85, 1928.
\newblock Reprinted as Appendix\,IX of \cite{grundlagen-der-geometrie-siebte}.
  \ {E}nglish translation {\em The foundations of mathematics}\/ by
  \bauermengelbergname\protect\index{Bauer-Mengelberg, Stefan} and
  \foellesdalname\ with a short introduction by \heijenoortname\ in
  \cite[\PP{464}{479}]{heijenoort-source-book}.

\bibitem[\protect\citeauthoryear{Hilbert\protect\index{Hilbert!David}}{1930a}]%
{grundlagen-der-geometrie-siebte}
David Hilbert\protect\index{Hilbert!David}.
\newblock {\em {Grundlagen der Geometrie. --- Siebente umgearbeitete und
  vermehrte Au\fli age. Mit 100 in den Text gedruckten Figuren}}.
\newblock Verlag und Druck von B. G. Teubner, \Leipzig, \Berlin, 1930.
\newblock {\nth 7}\,\rev\,\extd\,\ed\ of \cite{grundlagen-der-geometrie},
  thoroughly revised edition of \cite{grundlagen-der-geometrie-sechste}, \extd\
  with three new \appendixes\ (now ten in total) (Appendix\,VIII:
  \cite{unendliche}) (Appendix\,IX: \cite{grundlagenvortrag}) (Appendix\,X:
  \cite{probleme-grundlegung}).

\bibitem[\protect\citeauthoryear{Hilbert\protect\index{Hilbert!David}}{1930b}]%
{probleme-grundlegung}
David Hilbert\protect\index{Hilbert!David}.
\newblock {Probleme der Grundlegung der Mathematik}.
\newblock {\em {\MathematischeAnnalen}}, 102:1--9, 1930.
\newblock {Vortrag gehalten auf dem Internationalen Mathematiker-Kongre\sz\ in
  \Bologna, \Sep\,3, 1928}. \ Received March\,25, 1929. \ Reprinted as
  Appendix\,X of \cite{grundlagen-der-geometrie-siebte}. \ Short version in
  {\em Atti del congresso internationale dei matematici, \Bologna, 3--10
  settembre 1928}, \Vol\,1, \PP{135}{141}, Bologna, 1929.

\bibitem[\protect\citeauthoryear{Hilbert\protect\index{Hilbert!David}}{1931}]{%
zahlenlehre}
David Hilbert\protect\index{Hilbert!David}.
\newblock {Die Grundlegung der elementaren Zahlenlehre}.
\newblock {\em {\MathematischeAnnalen}}, 104:485--494, 1931.
\newblock {English} translation in \citep[\PP{1148}{1157}]{ewald-1996}.

\bibitem[\protect\citeauthoryear{Hilbert\protect\index{Hilbert!David}}{1932\ff%
}]{hilbert-gesammelte}
David Hilbert\protect\index{Hilbert!David}.
\newblock {\em {Gesammelte Abhandlungen}}.
\newblock \springerverlag, 1932\ff.

\bibitem[\protect\citeauthoryear{Hintikka}{1996}]{hintikkaprinciples}
K.~Jaakko~J. Hintikka.
\newblock {\em The Principles of Mathematics Revisited}.
\newblock {\cambridgeunipress}, 1996.

\bibitem[\protect\citeauthoryear{Howard \bgroup\&\ \egroup
  Rubin}{1998}]{weakaxiomofchoice}
Paul Howard and Jean~E. Rubin.
\newblock {\em Consequences of the Axiom of Choice}.
\newblock American Math.\ Society, 1998.

\bibitem[\protect\citeauthoryear{Kant\protect\index{Kant,
  Immanuel}}{1781}]{KrVA}
Immanuel Kant\protect\index{Kant, Immanuel}.
\newblock {\em {Critik der reinen Vernunft}}.
\newblock Johann Friedrich Hartknoch, Riga, 1781.
\newblock \nth 1\,\ed.

\bibitem[\protect\citeauthoryear{Kant\protect\index{Kant,
  Immanuel}}{1787}]{KdrV}
Immanuel Kant\protect\index{Kant, Immanuel}.
\newblock {\em {Critik der reinen Vernunft}}.
\newblock Johann Friedrich Hartknoch, Riga, 1787.
\newblock \nth 2 thoroughly \rev\,\ed\ of \cite{KrVA}. English translation:
  \cite{KdrV-English}.

\bibitem[\protect\citeauthoryear{Kant\protect\index{Kant,
  Immanuel}}{2008}]{KdrV-English}
Immanuel Kant\protect\index{Kant, Immanuel}.
\newblock {\em {Critique of Pure Reason}}.
\newblock Penguin Classics, 2008.
\newblock English translation of \cite{KdrV}, including the differences of the
  first edition (\cite{KrVA}), by {\namefont Max M\ue ller} and {\namefont
  Marcus Weigelt}, \nth 2\,\rev\,\ed\ (\nth 1\,\ed\,2007).

\bibitem[\protect\citeauthoryear{Kleene}{1938}]{kleene-1938}
Stephen~Cole Kleene.
\newblock On notation for ordinal numbers.
\newblock {\em {\jslname}}, 3(150--155), 1938.

\bibitem[\protect\citeauthoryear{Kleene}{1952}]{kleene}
Stephen~Cole Kleene.
\newblock {\em Introduction to Metamathematics}.
\newblock {\vannostrand}, 1952.

\bibitem[\protect\citeauthoryear{Kreisel}{1951}]{kreisel-1951}
Georg Kreisel.
\newblock On the interpretation of non-finitist proofs --- {Part\,I}.
\newblock {\em {\jslname}}, 16:241--267, 1951.

\bibitem[\protect\citeauthoryear{Kreisel}{1952}]{kreisel-1952}
Georg Kreisel.
\newblock On the interpretation of non-finitist proofs --- {Part\,II}.
\newblock {\em {\jslname}}, 17:43--58, iv, 1952.

\bibitem[\protect\citeauthoryear{Kreisel}{1958}]{kreisel-1958}
Georg Kreisel.
\newblock Mathematical significance of consistency proofs.
\newblock {\em {\jslname}}, 23:155--182, 1958.

\bibitem[\protect\citeauthoryear{Kreisel}{1982}]{kreisel-1982}
Georg Kreisel.
\newblock Finiteness theorems in arithmetic: an application of {\herbrand's}
  theorem for {$\Sigmaoffont_2$}-formulas.
\newblock 1982.
\newblock In \cite[\PP{39}{55}]{herbrand-symposium}.

\bibitem[\protect\citeauthoryear{Lemmermeyer \bgroup\&\ \egroup
  Roquette\protect\index{Roquette, Peter}}{2006}]{noether-hasse-correspondence}
Franz\protect\index{Hasse, Helmut}\protect\index{Noether, Emmy} Lemmermeyer and
  Peter Roquette\protect\index{Roquette, Peter}.
\newblock {\em \hassename--\noethername\ --- Die {Korrespondenz} 1925--1935}.
\newblock {Universit\ae t\esi verlag \Goettingen}, 2006.

\bibitem[\protect\citeauthoryear{L{\oe
  wenheim}\protect\loewenheimindex}{1915}]{loewenheim-1915}
Leopold L{\oe wenheim}\protect\loewenheimindex.
\newblock {\Ue ber M\oe glich\-keiten im Relativ\-kalk\ue l}.
\newblock {\em {\MathematischeAnnalen}}, 76:228--251, 1915.
\newblock {English} translation {\em On Possibilities in the Calculus of
  Relatives} by \bauermengelbergname\protect\index{Bauer-Mengelberg, Stefan}
  with an introduction by \heijenoortname\ in
  \cite[\PP{228}{251}]{heijenoort-source-book}.

\bibitem[\protect\citeauthoryear{Loveland}{1978}]{loveland}
Donald~W. Loveland.
\newblock {\em Automated Theorem Proving: A Logical Basis}.
\newblock {\northholland}, 1978.

\bibitem[\protect\citeauthoryear{Marchisotto \bgroup\&\ \egroup
  Smit{\protect\index{Smith, James T.}}h}{2007}]{smith-pieri}
Elena~Anne Marchisotto and James~T. Smit{\protect\index{Smith, James T.}}h.
\newblock {\em The Legacy of Mario Pieri in Geometry and Arithmetic}.
\newblock \birkhaeuser, 2007.

\bibitem[\protect\citeauthoryear{Menzler-Trott}{2001}]{menzler-gentzen-german}
Eckart Menzler-Trott.
\newblock {\em {\gentzen}'s Problem}.
\newblock \birkhaeuser, 2001.
\newblock \Rev\ English translation is \cite{menzler-gentzen-english}.

\bibitem[\protect\citeauthoryear{Menzler-Trott}{2007}]{menzler-gentzen-english}
Eckart Menzler-Trott.
\newblock {\em Logic's Lost Genius --- The Life of {\gentzenname}}.
\newblock \AMSname, 2007.
\newblock \Rev\ English translation of \cite{menzler-gentzen-german}.

\bibitem[\protect\citeauthoryear{Miller}{1992}]{miller}
Dale~A. Miller.
\newblock Unification under a mixed prefix.
\newblock {\em {\jscname}}, 14:321--358, 1992.

\bibitem[\protect\citeauthoryear{Moore}{1987}]{moore-1987}
Gregory~H. Moore.
\newblock A house divided against itself: The emergence of first-order logic as
  the basis for mathematics.
\newblock 1987.
\newblock In \cite[\PP{98}{136}]{phillips-1987}.

\bibitem[\protect\citeauthoryear{Myhill \bgroup\&al.\egroup
  }{1970}]{conference-intuitionism-proof-theory}
John Myhill, Akiko Kino, and Richard Vesley, editors.
\newblock {\em Intuitionism and Proof Theory. Proceedings of the International
  Conference Intuitionism and Proof Theory, Buffalo, 1968}.
\newblock \northholland, 1970.

\bibitem[\protect\citeauthoryear{Neumann\protect\index{Neumann, John
  von}}{1925}]{neumann-1925}
John~von Neumann\protect\index{Neumann, John von}.
\newblock {Eine Axiomatisierung der Mengenlehre}.
\newblock {\em {\jreineundangewandtemathematikname}}, 154:219--240, 1925.
\newblock Correction in \cite{neumann-1925-correction}. \ {E}nglish translation
  {\em An Axiomatization of Set Theory} by
  \bauermengelbergname\protect\index{Bauer-Mengelberg, Stefan} with an
  introduction by \heijenoortname\ in
  \cite[\PP{393}{413}]{heijenoort-source-book}.

\bibitem[\protect\citeauthoryear{Neumann\protect\index{Neumann, John
  von}}{1926}]{neumann-1925-correction}
John~von Neumann\protect\index{Neumann, John von}.
\newblock {Berichtigung zu der Arbeit \glqq Eine Axiomatisierung der
  Mengenlehre\grqq}.
\newblock {\em {\jreineundangewandtemathematikname}}, 155:128, 1926.
\newblock {Correction of \citep{neumann-1925}}.

\bibitem[\protect\citeauthoryear{Neumann\protect\index{Neumann, John
  von}}{1927}]{neumann-1927}
John~von\protect\index{Hilbert!David} Neumann\protect\index{Neumann, John von}.
\newblock {Zur \hilbert schen Bewei\esi theorie}.
\newblock {\em Mathematische Zeitschrift}, 26:1--46, 1927.
\newblock Received \Jul\,29, 1925. \ \bibcrit{First occurrence of the notion
  of\/ {\em basic typus}\/ (Grundtypu\es), the cardinal notion in the theory of
  \math\varepsilon-substitution. Clarification that the consitency proof of
  \citep{ackermann-1925} does not include second order with comprehension.}

\bibitem[\protect\citeauthoryear{Neumann\protect\index{Neumann, John
  von}}{1928}]{neumann-1928}
John~von Neumann\protect\index{Neumann, John von}.
\newblock {Die Axiomatisierung der Mengenlehre}.
\newblock {\em Mathematische Zeitschrift}, 27(669--752), 1928.

\bibitem[\protect\citeauthoryear{Newell \bgroup\&al.\egroup
  }{1957}]{newell-shaw-simon}
Allen Newell, J.~C. Shaw, and Herbert~A. Simon.
\newblock Empirical explorations with the {Logic Theory Machine}: A case study
  in heuristics.
\newblock In {\em \Proc\ Western Joint Computer \Conf}, pages 218--230. The
  Institute of Radio Engineers, \NewYork, 1957.
\newblock Also in \cite[\PP{109}{133}]{computers-and-thought}. \ Also in
  \cite[\Vol\,I, \PP{49}{73}]{siekmannwrightson}.

\bibitem[\protect\citeauthoryear{Nicod\protect\index{Nicod,
  Jean}}{1917}]{nicod}
Jean Nicod\protect\index{Nicod, Jean}.
\newblock A reduction in the number of primitive propositions of logic.
\newblock {\em Proc. Cambridge Philosophical Soc.}, 19:32--44, 1917.
\newblock Received \Oct\,30, 1916.
  \url{http://commons.wikimedia.org/wiki/Category:Jean_Nicod_texts_(English)}.

\bibitem[\protect\citeauthoryear{Nieuwenhuis}{2005}]{twentiethCADEfive}
Robert Nieuwenhuis, editor.
\newblock {\em {\thetwentiethCADEfive}}, number 3632 in Lecture Notes in
  Artificial Intelligence. \springerverlag, 2005.

\bibitem[\protect\citeauthoryear{Nonnengart}{1996}]{strongskolem}
Andreas Nonnengart.
\newblock Strong skolemization.
\newblock Research Report MPI-I-96-2-010, {\MPII}, Im Stadtwald, D--66123 \SB,
  1996.
\newblock
  {\url{http://domino.mpi-inf.mpg.de/internet/reports.nsf/NumberView/1996-2-01%
0}}.

\bibitem[\protect\citeauthoryear{Odifreddi\protect\index{Kreisel,
  Georg}}{1996}]{kreiseliana}
Piergiorgio Odifreddi\protect\index{Kreisel, Georg}, editor.
\newblock {\em Kreiseliana --- About and Around {\kreiselname}}.
\newblock A K Peters, Wellesley (MA), 1996.

\bibitem[\protect\citeauthoryear{Parsons}{1998}]{parsons-finitism}
Charles Parsons.
\newblock Finitism and intuitive knowledge.
\newblock 1998.
\newblock In \cite[\PP{249}{270}]{schirn-1998}.

\bibitem[\protect\citeauthoryear{Peckhaus\protect\index{Peckhaus,
  Volker}}{2004}]{schroeder-handbook}
Volker Peckhaus\protect\index{Peckhaus, Volker}.
\newblock {\schroeder's} logic.
\newblock 2004.
\newblock In \cite[\Vol\,3: The Rise of Modern Logic: From \leibniz\ to \frege,
  \PP{557}{610}]{handbook-of-the-history-of-logic}.

\bibitem[\protect\citeauthoryear{Peirce\protectedpeirceindex}{1885}]{peirce-18%
85}
Charles~S. Peirce\protectedpeirceindex.
\newblock On the algebra of logic: A contribution to the philosophy of
  notation.
\newblock {\em American J. of Mathematics}, 7:180--202, 1885.
\newblock Also in \cite[\PP{162}{190}]{peirce-chrono-five}.

\bibitem[\protect\citeauthoryear{Peirce\protectedpeirceindex}{1993}]{peirce-ch%
rono-five}
Charles~S. Peirce\protectedpeirceindex.
\newblock {\em Writings of\/ \peircename\ --- A Chronological Edition, \Vol\,5,
  1884--1886}.
\newblock \indianaunipress, 1993.
\newblock \Ed\ by {\namefont Christian J. W. Kloesel}.

\bibitem[\protect\citeauthoryear{Phillips}{1987}]{phillips-1987}
Esther~R. Phillips, editor.
\newblock {\em Studies in the History of Mathematics}.
\newblock {Mathematics Association of America, \Washington}, 1987.

\bibitem[\protect\citeauthoryear{Pieri}{1907/8}]{pieri}
Mario Pieri.
\newblock Sopra gli assiomi aritmetici.
\newblock {\em Il Bollettino delle seduta della Accademia Gioenia di Scienze
  Naturali in Catania}, Series\,2, 1--2:26--30, 1907/8.
\newblock English translation {\em On the Axioms of Arithmetic}\/ in
  \citep[\litsectref{4.2}, \PP{308}{313}]{smith-pieri}.

\bibitem[\protect\citeauthoryear{Presburger\protect\index{Presburger!Moj\.zes{%
}z}}{1930}]{presburger}
Moj{\zwithdot}esz Presburger\protect\index{Presburger!Moj\.zes{}z}.
\newblock {\Ue ber die Vollst\ae ndigkeit eine\es\ gewissen Sy\esi tem\es\ der
  Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation
  hervortritt}.
\newblock In {\em Sprawozdanie z I Kongresu metematyk\'ow kraj\'ow s\l
  owianskich, Warszawa 1929, (Comptes-rendus du \frenchnth 1 Congr\`es des
  Math\'ematiciens des Pays Slaves, Varsovie 1929)}, pages 92--101+395, 1930.
\newblock Remarks and {E}nglish translation:
  \cite{presburger-remarks-translation}.

\bibitem[\protect\citeauthoryear{Reid}{1970}]{reid-hilbert}
Constance Reid.
\newblock {\em {\hilbert}}.
\newblock \springerverlag, 1970.

\bibitem[\protect\citeauthoryear{Ribet}{1976}]{ribet76:_q}
Kenneth~A. Ribet.
\newblock A modular construction of unramified $p$-extensions of
  {$\mathbf{Q}(\mu p)$}.
\newblock {\em Inventiones mathematicae}, 34:151--162, 1976.

\bibitem[\protect\citeauthoryear{Robinson\protect\index{Robinson, J. Alan}
  \bgroup\&\ \egroup Voronkow}{2001}]{HandbookAR}
Alan Robinson\protect\index{Robinson, J. Alan} and Andrei Voronkow, editors.
\newblock {\em Handbook of Automated Reasoning}.
\newblock {\elsevier}, 2001.

\bibitem[\protect\citeauthoryear{Robinson\protect\index{Robinson, J.
  Alan}}{1965}]{resolution}
J.~Alan Robinson\protect\index{Robinson, J. Alan}.
\newblock A machine-oriented logic based on the resolution principle.
\newblock {\em J. of the ACM}, 12:23--41, 1965.
\newblock Also in \cite[\Vol\,1, \PP{397}{415}]{siekmannwrightson}.

\bibitem[\protect\citeauthoryear{Roquette\protect\index{Roquette,
  Peter}}{2000}]{roquette-artin}
Peter\protect\index{Hasse, Helmut} Roquette\protect\index{Roquette, Peter}.
\newblock On the history of \artin\es\protect\index{Artin!Emil} {$L$}-functions
  and conductors --- seven letters from \artin\ to \hasse\ in the year\,1930.
\newblock {\em Mitteilungen der Mathematischen Gesellschaft in Hamburg},
  19:5--50, 2000.
\newblock Web version updated \Jul\,23, 2003.

\bibitem[\protect\citeauthoryear{Roquette\protect\index{Roquette,
  Peter}}{2007}]{roquette-email}
Peter\protect\index{Hasse, Helmut}\protect\index{Herbrand!Jacques}
  Roquette\protect\index{Roquette, Peter}.
\newblock The correspondence \hassename--\herbrandname.
\newblock Personal e-mail communications with \roquettename. \Cf\ also
  \cite{hasse-herbrand-correspondence}, 2007.

\bibitem[\protect\citeauthoryear{Roquette\protect\index{Roquette,
  Peter}}{2009}]{hasse-herbrand-correspondence}
Peter Roquette\protect\index{Roquette, Peter}, editor.
\newblock {\em \hassename--\herbrandname\ --- The complete correspondence,
  including the six letters of \herbrand\ to \hasse, dated from \May\,11 to
  \Jul\,23, 1931, and a letter from \wedderburnname\ to \hasse\ on \herbrand's
  planned visit to \Princetonnostate, dated \May\,25, 1931}.
\newblock 2009.
\newblock To appear\protect\index{Hasse,
  Helmut}\protect\index{Herbrand!Jacques}\protect\index{Wedderburn, Joseph H.
  M.}

\bibitem[\protect\citeauthoryear{Rosser}{1936}]{rosser-incompleteness}
J.~Barkley\protect\index{Church, Alonzo}\protect\index{Goedel@G\"odel!Kurt}
  Rosser.
\newblock Extensions of some theorems of \goedel\ and \church.
\newblock {\em {\jslname}}, 1:87--91, 1936.

\bibitem[\protect\citeauthoryear{Rubin \bgroup\&\ \egroup
  Rubin}{1985}]{axiomofchoice}
Herman Rubin and Jean~E. Rubin.
\newblock {\em Equivalents of the {Axiom of Choice}}.
\newblock {\northholland}, 1985.
\newblock \nth 2\,\rev\,\ed\ (\nth 1\,\ed\,1963).

\bibitem[\protect\citeauthoryear{Scanlon\protect\index{Scanlon, Thomas M.,
  Jr.}}{1973}]{scanlon73:_consis_number_theor_via_theor}
Thomas~M. Scanlon\protect\index{Scanlon, Thomas M., Jr.}, \jr.
\newblock The consistency of number theory via {\herbrand's} {Theorem}.
\newblock {\em {\jslname}}, 38:29--58, 1973.

\bibitem[\protect\citeauthoryear{Schirn}{1998}]{schirn-1998}
Matthias Schirn, editor.
\newblock {\em The Philosophy of Mathematics Today}.
\newblock {\oxfordunipress}, 1998.

\bibitem[\protect\citeauthoryear{Schr{\"o}der\protect\index{Schr\"oder!Ernst}}%
{1895}]{schroeder-vorlesungen-III}
Ernst Schr{\"o}der\protect\index{Schr\"oder!Ernst}.
\newblock {\em {Vorlesungen \ue ber die Algebra der Logik, \Vol\,3, Algebra der
  Logik und der Relative, Vorlesungen I-XII}}.
\newblock \teubnerverlag, \Leipzig, 1895.
\newblock {E}nglish translation of some parts in \cite{brady}.

\bibitem[\protect\citeauthoryear{Sch{\ue tte}}{1960}]{schuette60:_beweis}
Kurt Sch{\ue tte}.
\newblock {\em {Bewei\esi theorie}}.
\newblock Number 103 in Grundlehren der mathematischen Wissenschaften.
  \springerverlag, 1960.
\newblock Thoroughly revised {English} translation: \cite{schuette-1977}.

\bibitem[\protect\citeauthoryear{Sch{\ue tte}}{1977}]{schuette-1977}
Kurt Sch{\ue tte}.
\newblock {\em Proof theory}.
\newblock Number 225 in Grundlehren der mathematischen Wissenschaften.
  \springerverlag, 1977.
\newblock Translated from a thorough revision of \cite{schuette60:_beweis} by
  \crossleyname.

\bibitem[\protect\citeauthoryear{Sieg\protect\index{Sieg,
  Wilfried}}{2005}]{sieg05:_only}
Wilfried Sieg\protect\index{Sieg, Wilfried}.
\newblock Only two letters: The correspondence between {\herbrand} and
  {\goedel}.
\newblock {\em Bulletin of Symbolic Logic}, 11:172--184, 2005.

\bibitem[\protect\citeauthoryear{Siek{\-}mann{\protect\siekmannindex}
  \bgroup\&\ \egroup Wrightson}{1983}]{siekmannwrightson}
J{\"o}rg Siek{\-}mann{\protect\siekmannindex} and Graham Wrightson, editors.
\newblock {\em Automation of Reasoning}.
\newblock \springerverlag, 1983.

\bibitem[\protect\citeauthoryear{Siek{\-}mann{\protect\siekmannindex}}{1989}]{%
siekmann-1989}
J{\"o}rg Siek{\-}mann{\protect\siekmannindex}.
\newblock Unification theory.
\newblock {\em {\jslname}}, 7:207--274, 1989.

\bibitem[\protect\citeauthoryear{Skolem\protect\skolemindex}{1919}]{skolem-191%
9}
Thoralf Skolem\protect\skolemindex.
\newblock {Untersuchungen \ue ber die Axiome des Klassen\-kalk\ue l\es\ und \ue
  ber Pro\-duk\-ta\-tion\es- und Summation\esi probleme, welche gewisse Klassen
  von Au\esi sagen be\-tref\-fen}.
\newblock {\em {\skriftername, \skrifterpublisher}}, 1919/3:1--37, 1919.
\newblock Dated \May\,26, 1917\@. \ Also in \cite[\PP{67}{101}]{skolem-1970}. \
  \bibcrit{First explicit occurrence of quantifier elimination}.

\bibitem[\protect\citeauthoryear{Skolem\protect\skolemindex}{1920}]{skolem-192%
0}
Thoralf Skolem\protect\skolemindex.
\newblock {Logisch-kombinatorische Untersuchungen \ue ber die Erf\ue llbarkeit
  und Bewei\esi barkeit mathematischer S\ae tze nebst einem Theorem \ue ber
  dichte Mengen}.
\newblock {\em {\skriftername, \skrifterpublisher}}, 1920/4:1--36, 1920.
\newblock Also in \cite[\PP{103}{136}]{skolem-1970}. \ {E}nglish translation of
  \litsectref 1 {\em Logico-Combinatorial Investigations in the Satisfiability
  or Provability of Mathematical Propositions: A simplified proof of a theorem
  by \loewenheimname\ and generalizations of the theorem} by
  \bauermengelbergname\protect\index{Bauer-Mengelberg, Stefan} with an
  introduction by \heijenoortname\ in
  \cite[\PP{252}{263}]{heijenoort-source-book}. \
  \bibcrit{\loewenheimskolemtheorem\ via \skolemnormalform\ and choice of a
  sub-model}.

\bibitem[\protect\citeauthoryear{Skolem\protect\skolemindex}{1923a}]{skolem-19%
23a}
Thoralf Skolem\protect\skolemindex.
\newblock {Begr\ue ndung der elementaren Arithmetik durch die rekurrierende
  Denkweise ohne Anwendung scheinbarer Ver\ae nderlichen mit unendlichem Au\esi
  dehnung\esi bereich}.
\newblock {\em {\skriftername, \skrifterpublisher}}, 1923/6:1--38, 1923.
\newblock Written 1919. \ Also in \cite[\PP{153}{188}]{skolem-1970}. \
  {E}nglish translation {\em The foundations of elementary arithmetic
  established by means of the recursive mode of thought, without the use of
  apparent variables ranging over infinite domains}\/ by
  \bauermengelbergname\protect\index{Bauer-Mengelberg, Stefan} with an
  introduction by \heijenoortname\ in
  \cite[\PP{302}{333}]{heijenoort-source-book}.

\bibitem[\protect\citeauthoryear{Skolem\protect\skolemindex}{1923b}]{skolem-19%
23b}
Thoralf Skolem\protect\skolemindex.
\newblock {Einige Bemerkungen zur axiomatischen Begr\ue ndung der Mengenlehre}.
\newblock In {\em \Proc\ \nth 5 Scandinaviska Matematikerkongressen,
  {H}elsingfors, July\,4--7,\,1922}, pages 217--232, Helsingfors, 1923.
  Akademiska Bokhandeln.
\newblock Also in \cite[\PP{137}{152}]{skolem-1970}. \ {E}nglish translation
  {\em Some remarks on Axiomatized Set Theory} by
  \bauermengelbergname\protect\index{Bauer-Mengelberg, Stefan}\ with an
  introduction by \heijenoortname\ in
  \cite[\PP{290}{301}]{heijenoort-source-book}. \ \bibcrit{The best written
  and, together with \citep{skolem-1920}, the most relevant publication on the
  \loewenheimskolemtheorem; although there is some minor gap in the proof
  according to \citet{wang-skolem}, cured in \citep{skolem-1929}. \ Includes
  \skolemsparadox\ and a proof of the \loewenheimskolemtheorem\ which does not
  require any weak forms of the \axiomofchoice, via \skolemnormalform\ and
  construction of a model without assuming the previous existence of another
  one}.

\bibitem[\protect\citeauthoryear{Skolem\protect\skolemindex}{1928}]{skolem-192%
8}
Thoralf Skolem\protect\skolemindex.
\newblock {\Ue ber die mathematische Logik (Nach einem Vortrag gehalten im
  Norwegischen Mathematischen Verein am {22.\,Oktober\,1928})}.
\newblock {\em Nordisk Matematisk Tidskrift}, 10:125--142, 1928.
\newblock Also in \cite[\PP{189}{206}]{skolem-1970}. \ {E}nglish translation
  {\em On Mathematical Logic}\/ by
  \bauermengelbergname\protect\index{Bauer-Mengelberg, Stefan}\ and
  \foellesdalname\ with an introduction by \drebenname\protect\index{Dreben,
  Burton}\ and \heijenoortname\ in
  \cite[\PP{508}{524}]{heijenoort-source-book}. \ \bibcrit{First explicit
  occurrence of \skolemization\ and \skolem\ functions}.

\bibitem[\protect\citeauthoryear{Skolem\protect\skolemindex}{1929}]{skolem-192%
9}
Thoralf Skolem\protect\skolemindex.
\newblock {\Ue ber einige Grundlagenfragen der Mathematik}.
\newblock {\em {\skriftername, \skrifterpublisher}}, 1929/4:1--49, 1929.
\newblock Also in \cite[\PP{227}{273}]{skolem-1970}. \ \bibcrit{Detailed
  discussion of \skolemsparadox\ and the \loewenheimskolemtheorem}.

\bibitem[\protect\citeauthoryear{Skolem\protect\skolemindex}{1941}]{skolem-194%
1}
Thoralf Skolem\protect\skolemindex.
\newblock Sur la port\'ee du th\'eor\`eme de {\loewenheimskolem}.
\newblock 1941.
\newblock In \cite[\PP{25}{52}]{gonseth-1941}. \ Also in
  \cite[\PP{455}{482}]{skolem-1970}.

\bibitem[\protect\citeauthoryear{Skolem\protect\skolemindex}{1970}]{skolem-197%
0}
Thoralf Skolem\protect\skolemindex.
\newblock {\em Selected Works in Logic}.
\newblock Universitetsforlaget \Oslo, 1970.
\newblock \Ed\ by \fenstadname. \bibcrit {Without index, but with most funny
  spellings in the newly set titles}.

\bibitem[\protect\citeauthoryear{Smullyan}{1968}]{smullyan}
Raymond~M. Smullyan.
\newblock {\em First-Order Logic}.
\newblock \springerverlag, 1968.

\bibitem[\protect\citeauthoryear{Stanisfer}{1984}]{presburger-remarks-translat%
ion}
Ryan\protect\index{Presburger!Moj\.zes{}z} Stanisfer.
\newblock {\em Presburger's Article on Integer Arithmetic: Remarks and
  Translation}.
\newblock Dept. of Computer Science, Cornell Univ., Ithaca, NY, 1984.

\bibitem[\protect\citeauthoryear{Stern}{1982}]{herbrand-symposium}
Jacques\protect\index{Herbrand!Jacques} Stern, editor.
\newblock {\em {\Proc\ of the \herbrand\ Symposium, Logic Colloquium'81,
  Marseilles, France, \Jul\,1981}}.
\newblock {\northholland}, 1982.

\bibitem[\protect\citeauthoryear{Tai\protect\index{Tait, William
  W.}t}{1981}]{tait-finitism}
William~W. Tai\protect\index{Tait, William W.}t.
\newblock Finitism.
\newblock {\em J. of Philosophy}, 78:524--546, 1981.

\bibitem[\protect\citeauthoryear{Tai\protect\index{Tait, William
  W.}t}{2006}]{tait-2006}
William~W. Tai\protect\index{Tait, William W.}t.
\newblock {\goedel's} correspondence on proof theory and constructive
  mathematics.
\newblock {\em {\philosphiamathname}}, 14:76--111, 2006.

\bibitem[\protect\citeauthoryear{Tarski\protect\index{Tarski,
  Alfred}}{1951}]{tarski-decision}
Alfred Tarski\protect\index{Tarski, Alfred}.
\newblock {\em A Decision Method for Elementary Algebra and Geometry}.
\newblock \Univ\ of California Press, 1951.
\newblock \nth 2\,\rev\,\ed\ (\nth 1\,\ed: Rand Corporation, Santa Monica (CA),
  1948).

\bibitem[\protect\citeauthoryear{Vihan}{1995}]{last-months-gentzen}
P{\v r}emysl Vihan.
\newblock The last months of {\gentzenname} in {Prague}.
\newblock {\em Collegium Logicum --- Annals of the {\goedelname\
  Society}\protect\index{Gentzen!Gerhard}}, 1:1--7, 1995.

\bibitem[\protect\citeauthoryear{Wallen}{1990}]{wallen}
Lincoln~A. Wallen.
\newblock {\em Automated Proof Search in Non-Classical Logics}.
\newblock MIT Press, 1990.

\bibitem[\protect\citeauthoryear{Wang\protect\index{Wang,
  Hao}}{1970}]{wang-skolem}
Hao Wang\protect\index{Wang, Hao}.
\newblock A survey of \skolem's work in logic.
\newblock {\em In \cite{skolem-1970}}, pages 17--52, 1970.

\bibitem[\protect\citeauthoryear{Weyl\protect\index{Weyl,
  Hermann}}{1921}]{weyl-1921}
Hermann Weyl\protect\index{Weyl, Hermann}.
\newblock {\Ue ber die neue Grundlagenkrise der Mathematik}.
\newblock {\em Mathematische Zeitschrift}, 14:39--79, 1921.

\bibitem[\protect\citeauthoryear{Weyl\protect\index{Weyl,
  Hermann}}{1928}]{weyl-grundlagenvortrag}
Hermann\protect\index{Hilbert!'s epsilon} Weyl\protect\index{Weyl, Hermann}.
\newblock {Diskussion\esi bemerkungen zu dem zweiten \hilbert schen Vortrag \ue
  ber die Grundlagen der Mathematik}.
\newblock {\em {\AbhandlungenmathHamburgname}}, 6:86--88, 1928.

\bibitem[\protect\citeauthoryear{Whitehead{\protect\whiteheadindex} \bgroup\&\
  \egroup Russell\protect\russellindex}{1910--1913}]{PM}
Alfred~North Whitehead{\protect\whiteheadindex} and Bertrand
  Russell\protect\russellindex.
\newblock {\em Principia Mathematica}.
\newblock {\cambridgeunipress}, 1910--1913.
\newblock {\nth 1\,\ed}.

\bibitem[\protect\citeauthoryear{Wirth \bgroup\&al.\egroup
  }{2009}]{herbrand-handbook}
Claus-Peter Wirth, J{\"o}rg Siek{\-}mann, {\mbox{Ch}}ristoph Benzm{\"u}ller,
  and Serge Autexier.
\newblock \herbrandname: Life, logic, and automated deduction.
\newblock 2009.
\newblock In \cite[\Vol\,5: Logic from \russell\ to \church,
  \PP{195}{254}]{handbook-of-the-history-of-logic}.

\bibitem[\protect\citeauthoryear{Wirth}{2004}]{wirthcardinal}
Claus-Peter Wirth.
\newblock {\DescenteInfinie\ + Deduction}.
\newblock {\em Logic J. of the IGPL}, 12:1--96, 2004.
\newblock \url{http://www.ags.uni-sb.de/~cp/p/d}.

\bibitem[\protect\citeauthoryear{Wirth}{2006}]{nonpermut}
Claus-Peter Wirth.
\newblock {\em {$\lim$$+$}, {$\delta^+$}, and Non-Permutability of
  {$\beta$}-Steps}.
\newblock {SEKI-Report SR--2005--01 (ISSN 1437--4447)}. {SEKI Publications},
  Saarland Univ., 2006.
\newblock \Rev\,\ed, \url{http://arxiv.org/abs/0902.3635}. Thoroughly improved
  version is \cite{wirth-jsc-non-permut}.

\bibitem[\protect\citeauthoryear{Wirth}{2008}]{wirth-jal}
Claus-Peter Wirth.
\newblock \hilbert's epsilon as an operator of indefinite committed choice.
\newblock {\em J. Applied Logic\protect\index{Hilbert!'s epsilon}}, 6:287--317,
  2008.
\newblock \url{http://dx.doi.org/10.1016/j.jal.2007.07.009}.

\bibitem[\protect\citeauthoryear{Wirth}{2009}]{wirth-jsc}
Claus-Peter Wirth.
\newblock Shallow confluence of conditional term rewriting systems.
\newblock {\em {\jscname}}, 44:69--98, 2009.
\newblock \url{http://dx.doi.org/10.1016/j.jsc.2008.05.005}.

\bibitem[\protect\citeauthoryear{Wirth}{2011}]{wirth-jsc-non-permut}
Claus-Peter Wirth.
\newblock {\math{\lim\tight+}, \math{\delta^+}, and \NonPermutability\ of
  \math\beta-Steps}.
\newblock {\em {\jscname}}, 2011.
\newblock To appear. More funny version is \cite{nonpermut}.

\bibitem[\protect\citeauthoryear{Wittgenstein\protect\index{Wittgenstein,
  Ludwig}}{1939}]{wittgenstein}
Ludwig Wittgenstein\protect\index{Wittgenstein, Ludwig}.
\newblock {\em Lectures on the Foundations of Mathematics, \Cambridge}.
\newblock \Univ\ of \Chicago\ Press, copyright 1989, 1939.
\newblock {Cora Diamond} (\ed), from the notes of {R. G. Bosanquet}, {Norman
  Malcolm}, {Rush Rhees}, and {Yorick Smythies}.

\bibitem[\protect\citeauthoryear{Wo{\l}kowski}{1993}]{first-goedel-symposium}
Zbigniew Wo{\l}kowski, editor.
\newblock {\em {\nth 1 \Int\ Symposium on \goedel's Theorem, Paris,
  May\,27--29, 1991}}. World Scientific Publishing, 1993.

\bibitem[\protect\citeauthoryear{Zach}{2001}]{zach-finitism}
Richard Zach.
\newblock {\em \hilbert's Finitism: Historical, Philosophical, and
  Metamathematical Perspectives}.
\newblock PhD thesis, \Univ\ of California, \Berkeley, 2001.

\bibitem[\protect\citeauthoryear{Zaremba\protect\index{Zaremba, Stanis\l
  aw}}{1926}]{zaremba}
Stanis{\l}aw Zaremba\protect\index{Zaremba, Stanis\l aw}.
\newblock {\em La Logique des Math\'ematiques}.
\newblock M\'emorial des Sciences Math\'ematiques, Fascicule\,XV.
  {\gauthiervillars}, 1926.

\bibitem[\protect\citeauthoryear{Zygmunt}{1991}]{presburger-life}
Jan\protect\index{Presburger!Moj\.zes{}z} Zygmunt.
\newblock \presburgername: Life and work.
\newblock {\em History and Philosophy of Logic}, 12:211--223, 1991.

\end{thebibliography}
