Linked bibliography for the SEP article "The Epsilon Calculus" by Jeremy Avigad and Richard Zach

This is an automatically generated and experimental page

If everything goes well, this page should display the bibliography of the aforementioned article as it appears in the Stanford Encyclopedia of Philosophy, but with links added to PhilPapers records and Google Scholar for your convenience. Some bibliographies are not going to be represented correctly or fully up to date. In general, bibliographies of recent works are going to be much better linked than bibliographies of primary literature and older works. Entries with PhilPapers records have links on their titles. A green link indicates that the item is available online at least partially.

This experiment has been authorized by the editors of the Stanford Encyclopedia of Philosophy. The original article and bibliography can be found here.

The following list of references provides a starting point for exploring the literature, but is by no means comprehensive.

Hilbert's Program

The following source books have many of the original papers:

Overviews of the historical development of logic and proof theory in the Hilbert school can be found in

The Early History of the Epsilon Calculus and Epsilon Substitution Method

The original work:

  • Ackermann, W., 1924, ‘Begründung des ’’tertium non datur’’ mittels der Hilbertschen Theorie der Widerspruchsfreiheit’, Mathematische Annalen, 93: 1–36. (Scholar)
  • Ackermann, W., 1937–38, ‘Mengentheoretische Begründung der Logik’, Mathematische Annalen, 115: 1–22. (Scholar)
  • Ackermann, W., 1940, ‘Zur Widerspruchsfreiheit der Zahlentheorie’, Mathematische Annalen, 117: 162–194. (Scholar)
  • Hilbert, D., 1922, ‘Neubegründung der Mathematik: Erste Mitteilung’, Abhandlungen aus dem Seminar der Hamburgischen Universität, 1: 157–177, English translation in Mancosu, 1998, 198–214 and Ewald, 1996, 1115–1134. (Scholar)
  • Hilbert, D., ‘Die logischen Grundlagen der Mathematik’, Mathematische Annalen, 88: 151–165, English translation in Ewald, 1996, 1134–1148. (Scholar)
  • Hilbert, D., Bernays, P., 1934, Grundlagen der Mathematik , Vol. 1, Berlin: Springer. (Scholar)
  • Hilbert, D., Bernays, P., 1939, Grundlagen der Mathematik , Vol. 2, Berlin: Springer. (Scholar)
  • von Neumann, J., 1927, ‘Zur Hilbertschen Beweistheorie’, Mathematische Zeitschrift, 26: 1–46. (Scholar)

Ackermann's 1940 proof is discussed in

Maehara showed how to prove the second epsilon theorem using cut elimination, and then strengthened the theorem to include the schema of extensionality, in

An early application of epsilon substitution is Georg Kreisel's no-counterexample interpretation.

The following provide modern presentations of Hilbert's epsilon calculus, not just from an introductory standpoint:

Corrections to errors in the literature (including Leisenring's book) can be found in

A variation of the epsilon calculus based on Skolem functions, and therefore compatible with first-order logic, is discussed in

  • Davis, M., and R. Fechter, 1991, ‘A free variable version of the first-order predicate calculus’, Journal of Logic and Computation, 1: 431–451.

General References for Proof Theory

The following contains a number of proof-theoretic results that are proved using methods similar to the ones used by Hilbert, Bernays, and Ackermann, though using Skolem functions instead of epsilon terms:

  • Shoenfield, J., 1967, Mathematical Logic, Reading, Mass.: Addison-Wesley, republished by the Association for Symbolic Logic, 2001. (Scholar)

For more on ordinal analysis, see, for example:

Herbrand's Theorem

Herbrand's theorem originally appeared in

English translations can be found in van Heijenoort (see above), and

  • Herbrand, J., 1971, Collected Works, W. Goldfarb (ed.), Cambridge, Mass.: Harvard University Press. (Scholar)

Further historical information can be found in

The literature on Herbrand's theorem is vast. For some general overviews, in addition to the general proof-theoretic references above, see

  • Buss, S., 1995, ‘On Herbrand's theorem’, Logic and Computational Complexity (Lecture Notes in Computer Science 960), Indianapolis, IN, 1994; Berlin: Springer, 195–209 [Buss 1995 available online in PDF]. (Scholar)
  • Girard, J.-Y., 1982, ‘Herbrand's theorem and proof theory’, Proceedings of the Herbrand Symposium, Amsterdam: North-Holland, 29-38. (Scholar)
  • Statman, R., 1979, ‘Lower bounds on Herbrand's theorem’, Proceedings of the American Mathematical Society, 75: 104–107. (Scholar)
  • Voronkov, A., 1999, ‘Simultaneous rigid E-unification and other decision problems related to the Herbrand theorem’, Theoretical Computer Science, 224: 319–352. (Scholar)

A striking application of Herbrand's theorem and related methods is found in Luckhardt's analysis of Roth's theorem:

For a discussion of useful extensions of Herbrand's methods, see

A model-theoretic version of this is discussed in

More Recent Developments in the Epsilon Substitution Method

In the following two papers, William Tait analyzed the epsilon substitution method in terms of continuity considerations:

More streamlined and modern versions of this approach can be found in:

  • Avigad, J., 2002, ‘Update procedures and the 1-consistency of arithmetic’, Mathematical Logic Quarterly, 48: 3–13. (Scholar)
  • Mints, G., 2001, ‘The epsilon substitution method and continuity’, in W. Sieg et al. (eds.), Reflections on the Foundations of Mathematics: Essays in Honor of Solomon Feferman, Lecture Notes in Logic 15, Association for Symbolic Logic. (Scholar)

The following paper shows that the epsilon substitution method for first-order arithmetic is, in fact, strongly normalizing:

Connections between cut elimination and epsilon substitution method are explored in

The epsilon substitution method has been extended to predicative fragments of second-order arithmetic in:

The following papers address impredicative theories:

  • Arai, T., 2003, ‘Epsilon substitution method for ID101  ∨   Σ01)’, Annals of Pure and Applied Logic, 121: 163–208. (Scholar)
  • Mints, G., 2001, ‘An approach to an epsilon-substitution method for ID1’, preprint, Institute Mittag Leffler, 45, MLI, Stockholm. (Scholar)

A development of set theory based on the epsilon-calculus is given by

Epsilon Operators in Linguistics, Philosophy, and Non-classical Logics

The following is a list of some publications in the area of language and linguistics of relevance to the epsilon calculus and its applications. The reader is directed in particular to the collections von Heusinger and Egli (2000) and von Heusinger et al. (2002) for further discussion and references.

Generated Sun Dec 10 06:44:10 2017