ε-terms, introduced by David Hilbert , have the form εx.φ, where x is a variable and φ is a formula. Their syntactical structure is thus similar to that of a quantified formulae, but they are terms, denoting ‘an element for which φ holds, if there is any’. The topic of this paper is an investigation into the possibilities and limits of using ε-terms for automated theorem proving. We discuss the relationship between ε-terms and Skolem terms (which both can be used alternatively for the purpose of ∃-quantifier elimination), in particular with respect to efficiency and intuition. We also discuss the consequences of allowing ε-terms in theorems (and cuts). This leads to a distinction between (essentially two) semantics and corresponding calculi, one enabling efficient automated proof search, and the other one requiring human guidance but enabling a very intuitive (i.e. Semantic) treatment of ε-terms. We give a theoretical foundation of the usage of both variants in a single framework. Finally, we argue that these two approaches to ε are just the extremes of a range of ε-treatments, corresponding to a range of different possible Skolemization variants.
Giese, M., & Ahrendt, W. (1999). Hilbert’s ε-terms in automated theorem proving. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 1617, pp. 171–185). Springer Verlag. https://doi.org/10.1007/3-540-48754-9_17