Hostname: page-component-669899f699-tpknm Total loading time: 0 Render date: 2025-04-26T21:26:45.400Z Has data issue: false hasContentIssue false
  • English
  • Français

A SIMPLIFIED PROOF OF THE EPSILON THEOREMS

Part of: Proof theory and constructive mathematics

Published online by Cambridge University Press:  10 July 2023

STEFAN HETZL Open the ORCID record for STEFAN HETZL [Opens in a new window]
STEFAN HETZL*
Affiliation:
INSTITUTE OF DISCRETE MATHEMATICS AND GEOMETRY TU WIEN, WIEDNER HAUPTSTRASSE 8-10 1040 VIENNA, AUSTRIA URL: https://www.dmg.tuwien.ac.at/hetzl/
*
E-mail: [email protected]
Get access Rights & Permissions [Opens in a new window]

Abstract

We formulate Hilbert’s epsilon calculus in the context of expansion proofs. This leads to a simplified proof of the epsilon theorems by disposing of the need for prenexification, Skolemisation, and their respective inverse transformations. We observe that the natural notion of cut in the epsilon calculus is associative.

Keywords

proof theoryepsilon calculusexpansion proofsHerbrand’s theorem

MSC classification

Primary: 03F05: Cut-elimination and normal-form theorems 03F07: Structure of proofs
Type
Research Article
Information
The Review of Symbolic Logic , Volume 17 , Issue 4 , December 2024 , pp. 1248 - 1263
Check for updates
Copyright
© The Author(s), 2023. Published by Cambridge University Press on behalf of The Association for Symbolic Logic

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

Article purchase

Temporarily unavailable

References

BIBLIOGRAPHY

Ackermann, W. (1940). Zur Widerspruchsfreiheit der Zahlentheorie. Mathematische Annalen, 117, 162–194.CrossRefGoogle Scholar
Aguilera, J. P., & Baaz, M. (2019). Unsound inferences make proofs shorter. Journal of Symbolic Logic, 84(1), 102–122.CrossRefGoogle Scholar
Andrews, P. B., Bishop, M., Issar, S., Nesmith, D., Pfenning, F., & Xi, H. (1996). TPS: A theorem-proving system for classical type theory. Journal of Automated Reasoning, 16(3), 321–353.CrossRefGoogle Scholar
Aschieri, F., Hetzl, S., & Weller, D. (2019). Expansion trees with cut. Mathematical Structures in Computer Science, 29(8), 1009–1029.CrossRefGoogle Scholar
Avigad, J. (2003). Eliminating definitions and Skolem functions in first-order logic. ACM Transactions on Computational Logic, 4, 402–415.CrossRefGoogle Scholar
Avigad, J., & Zach, R. The epsilon calculus. In Zalta, E. N., editor. The Stanford Encyclopedia of Philosophy (Spring 2020 Edition). Stanford: Metaphysics Research Lab, Stanford University, 2020.Google Scholar
Baaz, M., Hetzl, S., & Weller, D. (2012). On the complexity of proof deskolemization. Journal of Symbolic Logic, 77(2), 669–686.CrossRefGoogle Scholar
Baaz, M., Leitsch, A., & Lolic, A. (2018). A sequent-calculus based formulation of the extended first epsilon theorem. In Artëmov, S. N. and Nerode, A., editors. International Symposium on the Logical Foundations of Computer Science (LFCS). Lecture Notes in Computer Science, Vol. 10703. Cham: Springer, pp. 55–71.CrossRefGoogle Scholar
Baaz, M., Leitsch, A., & Lolic, A. (2020). An abstract form of the first epsilon theorem. Journal of Logic and Computation, 30(8), 1447–1468.CrossRefGoogle Scholar
Chaudhuri, K., Hetzl, S., & Miller, D. (2016). A multi-focused proof system isomorphic to expansion proofs. Journal of Logic and Computation, 26(2), 577–603.CrossRefGoogle Scholar
Church, A. (1940). A formulation of the simple theory of types. Journal of Symbolic Logic, 5(2), 56–68.CrossRefGoogle Scholar
Clote, P., & Krajíček, J. (1993). Open problems. In Clote, P. and Krajíček, J., editors. Arithmetic, Proof Theory and Computational Complexity. Oxford: Oxford University Press, pp. 1–19.CrossRefGoogle Scholar
Davis, M., & Fechter, R. (1991). A free variable version of the first-order predicate calculus. Journal of Logic and Computation, 1(4), 431–451.CrossRefGoogle Scholar
Heijltjes, W. (2010). Classical proof forestry. Annals of Pure and Applied Logic, 161(11), 1346–1366.CrossRefGoogle Scholar
Hetzl, S., Libal, T., Riener, M., & Rukhaia, M. Understanding resolution proofs through Herbrand’s theorem. In Galmiche, D. and Larchey-Wendling, Dominique, editors. Automated Reasoning with Analytic Tableaux and Related Methods. Lecture Notes in Computer Science, Vol. 8123. Berlin–Heidelberg: Springer, 2013, pp. 157–171.CrossRefGoogle Scholar
Hetzl, S., & Weller, D. (2013). Expansion trees with cut. Preprint. Available from: http://arxiv.org/abs/1308.0428.Google Scholar
Hilbert, D., & Bernays, P. (1939). Grundlagen der Mathematik II. Berlin: Springer.Google Scholar
Hyland, J. M. E. (2002). Proof theory in the abstract. Annals of Pure and Applied Logic, 114, 43–78.CrossRefGoogle Scholar
Leitsch, A., & Lolic, A. (2019). Extraction of expansion trees. Journal of Automated Reasoning, 62(3), 393–430.CrossRefGoogle ScholarPubMed
Maehara, S. (1955). The predicate calculus with $\varepsilon$ -symbol. Journal of the Mathematical Society of Japan, 7(4):323–344.CrossRefGoogle Scholar
McKinley, R. (2013). Proof nets for Herbrand’s theorem. ACM Transactions on Computational Logic, 14(1), 5:1–5:31.CrossRefGoogle Scholar
Miller, D. (1987). A compact representation of proofs. Studia Logica, 46(4), 347–370.CrossRefGoogle Scholar
Mints, G. (1996). Thoralf Skolem and the epsilon substitution method for predicate logic. Nordic Journal of Philosophical Logic, 1(2), 133–146.Google Scholar
Moser, G., & Zach, R. (2006). The epsilon calculus and Herbrand complexity. Studia Logica, 82(1), 133–155.CrossRefGoogle Scholar
Tait, W. (2010). The substitution method revisited. In Feferman, S., and Sieg, W., editors. Proofs, Categories and Computations: Essays in Honor of Grigori Mints. London: College Publications, pp. 231–241.Google Scholar
Weller, D. (2011). On the elimination of quantifier-free cuts. Theoretical Computer Science, 412(49), 6843–6854.CrossRefGoogle ScholarPubMed