Linked bibliography for the SEP article "The Epsilon Calculus" by Jeremy Avigad |
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:
- Bennacerraf, P., Putnam, H. (eds.), 1983, Philosophy of Mathematics, 2nd ed., Cambridge: Cambridge University Press (Scholar)
- Ewald, W. B. (ed.), 1996, From Kant to Hilbert. A Source Book in the Foundations of Mathematics, Vol. 2, Oxford: Oxford University Press (Scholar)
- Mancosu, P. (ed.), 1998, From Brouwer to Hilbert. The Debate on the Foundations of Mathematics in the 1920s, Oxford: Oxford University Press (Scholar)
- van Heijenoort, J. (ed.), 1967, From Frege to Gödel. A Source Book in Mathematical Logic. Cambridge, Mass.: Harvard University Press (Scholar)
Overviews of the historical development of logic and proof theory in the Hilbert school can be found in
- Avigad J. and Reck, E., 2001, ‘Clarifying the nature of the infinite: the development of metamathematics and proof theory’, Carnegie Mellon University Technical Report CMU-PHIL-120 [Available online in PDF] (Scholar)
- Hallett, M., 1995, ‘Hilbert and logic’, M. Marion and R. S. Cohen, Quebec Studies in the Philosophy of Science, Vol. 1, Dordrecht: Kluwer, 135-187 (Scholar)
- Mancosu, P., 1998a, ‘Hilbert and Bernays on metamathematics’, in Mancosu, 1998, 149-188 (Scholar)
- Moore, G. H., 1997, ‘Hilbert and the emergence of modern mathematical logic’, Theoria (Segunda Epoca), 12: 65-90 (Scholar)
- Peckhaus, V., 1990, Hilbertprogramm und Kritische Philosophie, Göttingen: Vandenhoek & Ruprecht (Scholar)
- Sieg, W., 1988, ‘Hilbert's program sixty years later’, Journal of Symbolic Logic, 53: 338-348 (Scholar)
- Sieg, W., 1990, ‘Reflections on Hilbert's program’, W. Sieg (ed.), Acting and Reflecting, Dordrecht: Kluwer (Scholar)
- Sieg, W., 1999, ‘Hilbert's Programs: 1917-1922’, Bulletin of Symbolic Logic, 5: 1-44 [Available online in Postscript] (Scholar)
- Zach, R., 1999, ‘Completeness before Post: Bernays, Hilbert, and the development of propositional logic’, Bulletin of Symbolic Logic, 5: 331--366 [Available online in Postscript] (Scholar)
- Zach, R., 2003, ‘The practice of finitism. Epsilon calculus and consistency proofs in Hilbert's Program’, Synthese 137: 211-259. [Preprint available online] (Scholar)
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
- Hilbert, D., Bernays, P., 1970, ‘Grundlagen der Mathematik’, Vol. 2, 2nd, edition, Berlin: Springer, Supplement V (Scholar)
- Wang, H., 1963, A Survey of Mathematical Logic, Peking: Science Press (Scholar)
Maehara showed how to prove the second epsilon theorem using cut elimination, and then strengthened the theorem to include the schema of extensionality, in
- Maehara, S., 1955, ‘The predicate calculus with ε-symbol’, Journal of the Mathematical Society of Japan, 7: 323-344 (Scholar)
- Maehara, S., 1957, ‘Equality axiom on Hilbert's ε-symbol’, Journal of the Faculty of Science, University of Tokyo, Section 1, 7: 419-435 (Scholar)
An early application of epsilon substitution is Georg Kreisel's no-counterexample interpretation.
- Kreisel, G, 1951, ‘On the interpretation of non-finitist proofs - part I’, Journal of Symbolic Logic, 16: 241-267 (Scholar)
The following provide modern presentations of Hilbert's epsilon calculus, not just from an introductory standpoint:
- Leisenring, A. C., 1969, Mathematical Logic and Hilbert's Epsilon-Symbol, London: Macdonald (Scholar)
- Mints, G., 1996, ‘Thoralf Skolem and the epsilon substitution method for predicate logic’, Nordic Journal of Philosophical Logic, 1: 133-146 [Available online] (Scholar)
- Moser, G., 2000, The Epsilon Substitution Method, Master's Thesis, University of Leeds (Scholar)
- Moser, G., Zach, R., 2006, ‘The epsilon calculus and Herbrand complexity’, Studia Logica, 82(1): 133-155. [Preprint available online in PDF] (Scholar)
Corrections to errors in the literature (including Leisenring's book) can be found in
- Flannagan, T. B., 1975, ‘On an extension of Hilbert's second ε-theorem’, Journal of Symbolic Logic, 40: 393-397 (Scholar)
- Ferrari, P. L., 1987, ‘A note on a proof of Hilbert's second ε-theorem’, Journal of Symbolic Logic, 52: 214-215 (Scholar)
- Yashahura, M., 1982, ‘Cut elimination in ε-calculi’, Zeitschrift für mathematische Logik und Grundlagen der Mathematik, 28: 311-316 (Scholar)
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
- Buss, S. (ed.), 1998. The Handbook of Proof Theory, Amsterdam: North-Holland (Scholar)
- Takeuti, G., 1987, Proof Theory, second edition. Amsterdam: North-Holland, Amsterdam (Scholar)
- Troelstra, A. S., Schwichtenberg, H., 2000, Basic Proof Theory, second edition. Cambridge: Cambridge University Press (Scholar)
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:
- Takeuti, G., Proof Theory (see above)
- Pohlers, Wolfram, 1998, ‘Subsystems of set theory and second-order number theory’, in S. Buss (ed.), The Handbook of Proof Theory (see above), 209-335 (Scholar)
Herbrand's Theorem
Herbrand's theorem originally appeared in
- Herbrand, J., 1930, Recherches sur la thèorie de la dèmonstration, Dissertation, University of Paris (Scholar)
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
- Dreben, B., Andrews, P., Aanderaa, S., 1963, ‘False lemmas in Herbrand’, Bulletin of the American Mathematical Society, 69: 699-706 (Scholar)
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 (Indianapolis, IN, 1994), Lecture Notes in Computer Science 960, Berlin: Springer, 195-209 [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:
- Luckhardt, H., 1989, ‘Herbrand-Analysen zweier Beweise des Satzes von Roth: Polynomiale Anzahlschranken’, Journal of Symbolic Logic, 54: 234-263 (Scholar)
For a discussion of useful extensions of Herbrand's methods, see
- Sieg, W., 1991, ‘Herbrand analyses’, Archive for Mathematical Logic, 30: 409-441 (Scholar)
A model-theoretic version of this is discussed in
- Avigad, J., 2002, ‘Saturated models of universal theories’, to appear in the Annals of Pure and Applied Logic (Scholar)
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:
- Tait, W. W., 1960, ‘The substitution method.’ Journal of Symbolic Logic , 30: 175-192. (Scholar)
- Tait, W. W., 1965, ‘Functionals defined by transfinite recursion,’ Journal of Symbolic Logic 30: 155-174. (Scholar)
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:
- Mints, G., 1996, ‘Strong termination for the epsilon substitution method’, Journal of Symbolic Logic, 61: 1193-1205 (Scholar)
A connection between cut elimination and epsilon substitution method is explored in
- Mints, G., 1994, ‘Gentzen-type systems and Hilbert's epsilon substitution method. I’, Logic, Methodology and Philosophy of Science, IX (Uppsala, 1991), Amsterdam: North-Holland, 91-122 (Scholar)
The epsilon substitution method has been extended to predicative fragments of second-order arithmetic in:
- Mints, G., Tupailo, S., Buchholz, W., 1996, ‘Epsilon substitution method for elementary analysis’, Archive for Mathematical Logic, 35: 103-130 (Scholar)
- Mints, G., Tupailo, S., 1999, ‘Epsilon-substitution method for the ramified language and Δ11-comprehension rule’, in A. Cantini et al. (eds.), Logic and Foundations of Mathematics (Florence, 1995), Dordrecht: Kluwer, 107-130 (Scholar)
- Arai, T., 2002, ‘Epsilon substitution method for theories of jump hierarchies’, Archive for Mathematical Logic, 2: 123-153 (Scholar)
The following papers address impredicative theories:
- Arai, T., 2003, ‘Epsilon substitution method for ID1(Π01 ∨ Σ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
- Bourbaki, N., 1958, Theorie des ensembles , Paris: Hermann (Scholar)
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.
- Bell, J. L., 1993a. ‘Hilbert's epsilon-operator and classical logic’, Journal of Philosophical Logic, 22: 1-18 (Scholar)
- Bell, J. L., 1993b. ‘Hilbert's epsilon operator in intuitionistic type theories’, Mathematical Logic Quarterly 39: 323-337 (Scholar)
- Chierchia, G., 1992. ‘Anaphora and dynamic logic’. Linguistics and Philosophy, 15: 111-183 (Scholar)
- DeVidi, D., 1995. ‘Intuitionistic epsilon- and tau-calculi’, Mathematical Logic Quarterly 41: 523--546 (Scholar)
- Evans, G., 1980, ‘Pronouns’, Linguistic Inquiry , 11: 337-362 (Scholar)
- Egli, U., von Heusinger, K., 1995, ‘The epsilon operator and E-type pronouns’, in U. Egli et al. (eds.), Lexical Knowledge in the Organization of Language, Amsterdam: Benjamins, 121-141 (Current Issues in Linguistic Theory 114) (Scholar)
- Fine, K., 1985. Reasoning with Arbitrary Objects. Oxford: Blackwell. (Scholar)
- Fitting, M., 1975. ‘A modal logic epsilon-calculus’, Notre Dame Journal of Formal Logic, 16: 1--16
- Hintikka, J., Kulas, J., 1985. Anaphora and Definite Descriptions: Two Applications of Game-Theoretical Semantics. Dordrecht: Reidel (Scholar)
- Kempson, R., Meyer Viol, W., and Gabbay, D., 2001. Dynamic Syntax: The Flow of Language Understanding. Oxford: Blackwell (Scholar)
- Meyer Viol, W. P. M., 1995, Instantial Logic. An Investigation into Reasoning with Instances . Ph.D. thesis, University of Utrecht. ILLC Dissertation Series 1995-11 (Scholar)
- Meyer Viol, W., 1995a. ‘A proof-theoretic treatment of assignments’, Bulletin of the IGPL, 3: 223-243 [Available online]
- Mostowski, A., 1963. ‘The Hilbert epsilon function in many-valued logics’, Acta Philosophica Fennica, 16: 169-188. (Scholar)
- Reinhart, T., 1992. ‘Wh-in-situ: An apparent paradox’. In: P. Dekker and M. Stokhof (eds.). Proceedings of the Eighth Amsterdam Colloquium December 17-20, 1991. ILLC. University of Amsterdam, 483-491 (Scholar)
- Reinhart, T., 1997. ‘Quantifier scope: How labor is divided between QR and choice functions’. Linguistics and Philosophy, 20: 335-397 (Scholar)
- Slater, B. H. 1986, ‘E-type pronouns and ε-terms’, Canadian Journal of Philosophy, 16: 27-38
- Slater, B. H. 1988, ‘Hilbertian reference’, Noûs, 22: 283-97 (Scholar)
- Slater, B. H. 1994, ‘The epsilon calculus’ problematic’, Philosophical Papers, 23: 217-42 (Scholar)
- Slater, B.H. 2000, ‘Quantifier/variable-binding’, Linguistics and Philosophy, 23: 309-21 (Scholar)
- von Heusinger, K., 1997. ‘Definite descriptions and choice functions’. In: S. Akama (ed.). Logic, Language and Computation. Dordrecht: Kluwer, 61-91 (Scholar)
- von Heusinger, K., 2000, ‘The Reference of Indefinites’, in von Heusinger and Egli, (2000), 265-284 (Scholar)
- von Heusinger, K., 2004, ‘Choice functions and the anaphoric semantics of definite NPs’, Research in Language and Computation, 2: 309-329. (Scholar)
- von Heusinger, K., Egli, U., (eds.), 2000. Reference and Anaphoric Relations. Dordrecht: Kluwer, 265-284 (Scholar)
- von Heusinger, K., Egli, U., 2000a. ‘ Introduction: Reference and the Semantics of Anaphora’, in von Heusinger and Egli (2000), 1-13 (Scholar)
- von Heusinger, K., Kempson, R., Meyer-Viol, W., (eds.), 2002. Proceedings of the Workshop Choice Function and Natural Language Semantics, Arbeitspapier 110. Fachbereich Sprachwissenschaft, Universität Konstanz (Scholar)
- Winter, Y., 1997. ‘Choice functions and the scopal semantics of indefinites’. Linguistics and Philosophy, 20: 399-467 (Scholar)
Generated Tue May 21 08:49:21 2013
