This is a file in the archives of the Stanford Encyclopedia of Philosophy. 
version history

Stanford Encyclopedia of PhilosophyA  B  C  D  E  F  G  H  I  J  K  L  M  N  O  P  Q  R  S  T  U  V  W  X  Y  Z

last substantive content change

The epsilon calculus is a logical formalism developed by David Hilbert in the service of his program in the foundations of mathematics. The epsilon operator is a termforming operator which replaces quantifiers in ordinary predicate logic. Specifically, in the calculus, a term x A denotes some x satisfying A(x), if there is one. In Hilbert's Program, the epsilon terms play the role of ideal elements; the aim of Hilbert's finitistic consistency proofs is to give a procedure which removes such terms from a formal proof. The procedures by which this is to be carried out are based on Hilbert's epsilon substitution method. The epsilon calculus, however, has applications in other contexts as well. The first general application of the epsilon calculus was in Hilbert's epsilon theorems, which in turn provide the basis for the first correct proof of Herbrand's theorem. More recently, variants of the epsilon operator have been applied in linguistics and linguistic philosophy to deal with anaphoric pronouns.
By the turn of the century David Hilbert and Henri Poincaré were recognized as the two most important mathematicians of their generation. Hilbert's range of mathematical interests was broad, and included an interest in the foundations of mathematics: his Foundations of Geometry was published in 1899, and of the list of questions posed to the International Congress of Mathematicians in 1900, three addressed distinctly foundational issues.
Following the publication of Russell's paradox, Hilbert presented an address to the Third International Congress of Mathematicians in 1904, where, for the first time, he sketched his plan to provide a rigorous foundation for mathematics via syntactic consistency proofs. But he did not return to the subject in earnest until 1917, when he began a series of lectures on the foundations of mathematics with the assistance of Paul Bernays. Although Hilbert was impressed by the work of Russell and Whitehead in their Principia Mathematica, he became convinced that the logicist attempt to reduce mathematics to logic could not succeed, due in particular to the nonlogical character of their axiom of reducibility. At the same time, he judged the intuitionistic rejection of the law of the excluded middle as unacceptable to mathematics. Therefore, in order to counter concerns raised by the discovery of the logical and settheoretic paradoxes, a new approach was needed to justify modern mathematical methods.
By the summer of 1920, Hilbert had formulated such an approach. First, modern mathematical methods were to be represented in formal deductive systems. Second, these formal systems were to be proved syntactically consistent, not by exhibiting a model or reducing their consistency to another system, but by a direct metamathematical argument of an explicit, "finitary" character. The epsilon calculus was to provide the first component of this program, while his epsilon substitution method was to provide the second.
The epsilon calculus is, in its most basic form, an extension of firstorder predicate logic with an "epsilon operation" that picks out, for any true existential formula, a witness to the existential quantifier. The extension is conservative in the sense that it does not add any new firstorder consequences. But, conversely, quantifiers can be defined in terms of the epsilons, so firstorder logic can be understood in terms of quantifierfree reasoning involving the epsilon operation. It is this latter feature that makes the calculus convenient for the purpose of proving consistency. Suitable extensions of the epsilon calculus make it possible to embed stronger, quantificational theories of numbers and sets in quantifierfree calculi. Hilbert expected that it would be possible to demonstrate the consistency of such extensions.
In his Hamburg lecture in 1921 (1922), Hilbert first presented the idea of using choice functions to deal with the principle of the excluded middle in a formal system for arithmetic. These ideas were developed into the epsilon calculus and the epsilon substitution method in a series of lecture courses between 1921 and 1923, and in Hilbert's (1923). The final presentation of the epsiloncalculus can be found in Wilhelm Ackermann's dissertation (1924).
This section will describe a version of the calculus corresponding to firstorder logic, while extensions to first and secondorder arithmetic will be described below.
Let L be a firstorder language, which is to say, a list of constant, function, and relation symbols with specified arities. The set of epsilon terms and the set of formulae of L are defined inductively, simultaneously, as follows:
Substitution and the notions of free and bound variable, are defined in the usual way; in particular, the variable x becomes bound in the term x A. The intended interpretation is that x A denotes some x satisfying A, if there is one. Thus, the epsilon terms are governed by the following axiom (Hilbert's "transfinite axiom"):
A(x) A(x A)
In addition, the epsilon calculus includes a complete set of axioms governing the classical propositional connectives, and axioms governing the equality symbol. The only rules of the calculus are the following:
Earlier forms of the epsilon calculus (such as that presented in (Hilbert 1923)) use a dual form of the epsilon operator, in which x A returns a value falsifying A(x). The version above was used in Ackermann's dissertation, and has become standard.
Note that the calculus just described is quantifierfree. Quantifiers can be defined as follows:
x A(x) A(x A)
x A(x) A(x (A))
The usual quantifier axioms and rules can be derived from these, so the definitions above serve to embed firstorder logic in the epsilon calculus. The converse is, however, not true: not every formula in the epsilon calculus is the image of an ordinary quantified formula under this embedding. Hence, the epsilon calculus is more expressive than the predicate calculus, simply because epsilon term can be combined in more complex ways than quantifiers.
It is worth noting that epsilon terms are nondeterministic, thereby representing a form of the axiom of choice. For example, in a language with constant symbols a and b, x (x = a x = b) is either a or b, but the calculus leaves it entirely open as to which is the case. One can add to the calculus a schema of extensionality,
x (A(x) B(x)) x A = x B
which asserts that the epsilon operator assigns the same witness to
equivalent formulae A and B. For many applications,
however, this additional schema is not necessary.
The second volume of Hilbert and Bernays' Grundlagen der Mathematik (1939) provides an account of results on the epsiloncalculus that had been proved by that time. This includes a discussion of the first and second epsilon theorems with applications to firstorder logic, the epsilon substitution method for arithmetic with open induction, and a development of analysis (that is, secondorder arithmetic) with the epsilon calculus.
The first and second epsilon theorems are as follows:
First epsilon theorem: Suppose {A} is a set of quantifierfree formulae not involving the epsilon symbol. If A is derivable from in the epsilon calculus, then A is derivable from in quantifierfree predicate logic.
Second epsilon theorem: Suppose {A} is a set of formulae not involving the epsilon symbol. If A is derivable from in the epsilon calculus, then A is derivable from in predicate logic.
In the first epsilon theorem, "quantifierfree predicate logic" is intended to include the substitution rule above, so quantifierfree axioms behave like their universal closures. Since the epsilon calculus includes firstorder logic, the first epsilon theorem implies that any detour through firstorder predicate logic used to derive a quantifierfree theorem from quantifierfree axioms can ultimately be avoided. The second epsilon theorem shows that any detour through the epsilon calculus used to derive a theorem in the language of the predicate calculus from axioms in the language of the predicate calculus can also be avoided.
More generally, the first epsilon theorem establishes that quantifiers and epsilons can always be eliminated from a proof of a quantifierfree formula from other quantifierfree formulae. This is of particular importance for Hilbert's program, since the epsilons play the role of ideal elements in mathematics. If quantifierfree formulae correspond to the "real" part of the mathematical theory, the first epsilontheorem shows that ideal elements can be eliminated from proofs of real statements, provided the axioms are also real statements.
This idea is made precise in a certain general consistency theorem which Hilbert and Bernays derive from the first epsilontheorem, which says the following: Let F be any formal system which results from the predicate calculus by addition of constant, function, and predicate symbols plus true axioms which are quantifier and epsilonfree, and suppose the truth of atomic formulae in the new language is decidable. Then F is consistent in the strong sense that every derivable quantifier and epsilonfree formula is true. Hilbert and Bernays use this theorem to give a finitistic consistency proof of elementary geometry (1939, Sec 1.4).
The difficulty for giving consistency proofs for arithmetic and analysis consists in extending this result to cases where the axioms also contain ideal elements, i.e., epsilons.
Hilbert and Bernays used the methods of the epsilon calculus to establish theorems about first order logic that make no reference to the epsilon calculus itself. One such example is Herbrand's theorem . This is often formulated as the statement that if an existential formula
x_{1} … x_{k} A(x_{1},…, x_{k})
is derivable in firstorder predicate logic (without equality), where A is quantifierfree, then there are sequences of terms t_{1}^{1}, …, t_{k}^{1}, …, t_{1}^{n}, …, t_{k}^{n}, such that
A(t_{1}^{1},…,t_{k}^{1}) … A(t_{1}^{n}, …, t_{k}^{n})
is a tautology. If one is dealing with firstorder logic with equality, one has to replace "tautology" by "tautological consequence of substitution instances of the equality axioms"; following Shoenfield we will use the term "quasitautology" to describe such a formula.
The version of Herbrand's theorem just described follows immediately from the Extended First Epsilon Theorem of Hilbert and Bernays. Using methods associated with the proof of the second epsilon theorem, however, Hilbert and Bernays derived a stronger result that, like Herbrand's original formulation, provides more information. To understand the two parts of the theorem below, it helps to consider a particular example. Let A be the formula
x_{1} x_{2} x_{3} x_{4} B(x_{1}, x_{2} , x_{3}, x_{4})
where B is quantifierfree. The negation of A is equivalent to
x_{1} x_{2} x_{3} x_{4} B(x_{1}, x_{2}, x _{3}, x_{4}).
By Skolemizing, i.e., using function symbols to witness the existential quantifiers, we obtain
f_{2}, f_{4} x_{1}, x_{3} B(x_{1}, f_{2}(x_{1}), x_{3}, f_{4}(x_{1}, x_{3})).
Taking the negation of this, we see that the original formula is "equivalent" to
f_{2}, f_{4} x_{1}, x_{3} B(x_{1}, f_{2}(x_{1}), x_{3}, f_{4}(x_{1}, x_{3})).
The first clause of the theorem below, in this particular instance, says that the formula A above is derivable in firstorder logic if and only if there is a sequence of terms t_{1}^{1}, t_{3}^{1}, …, t_{1}^{n}, t_{3}^{n} in the expanded language with f_{2} and f_{4} such that
B(t_{1}^{1}, f _{2}(t_{1}^{1}), t_{3} ^{1}, f_{4}(t_{1}^{1}, t _{3}^{1})) … B(t_{1}^{n}, f_{2}(t_{1}^{n}), t_{3}^{n}, f_{2}(t_{1}^{n}, t_{3}^{n}))
is a quasitautology.
The second clause of the theorem below, in this particular instance, says that the formula A above is derivable in firstorder logic if and only if there are sequences of variables x_{2}^{1} , x_{4}^{1},…, x_{2}^{n} , x_{4}^{n} and terms s_{1}^{1}, s_{3}^{1},…, s_{1}^{n}, s_{3}^{n} in the original language such that
B(s_{1}^{1}, x_{2}^{1}, s_{3}^{1}, x_{4}^{1}) … B(s_{1}^{n}, x_{2}^{n}, s_{3}^{n}, x_{4}^{n})
is a quasitautology, and such that A is derivable from this formula using only the quantifier and idempotency rules described below.
More generally, suppose A is any prenex formula, of the form
Q_{1}x_{1} … Q_{n}x_{n} B(x_{1}, …, x_{n}),
where B is quantifierfree. Then B is said to be the matrix of A, and an instance of B is obtained by substituting terms in the language of B for some of its variables. The Herbrand normal form A^{H} of A is obtained by
deleting each universal quantifier, and
replacing each universally quantified variable x_{i} by f_{i}(x_{i}^{1}, …, x_{i}^{k(i)}), where x_{i}^{1}, …, x_{i}^{k(i)} are the variables corresponding to the existential quantifiers preceding Q_{i} in A (in order), and f_{i} is a new function symbol designated for this role.
When we refer to an instance of the matrix of A^{H}, we mean a formula that is obtained by substituting terms in the expanded language in the matrix of A^{H}. We can now state Hilbert and Bernays's formulation of
Herbrand's theorem. (1) A prenex formula A is derivable in the predicate calculus if and only if there is a disjunction of instances of the matrix of A^{H} which is a quasitautology.
(2) A prenex formula A is derivable in the predicate calculus if and only if there is a disjunction _{j} B_{j} of instances of the matrix of A, such that _{j} B_{j} is a quasitautology, and A is derivable from _{j} B_{j} using the following rules:
as well as the idempotence of (from C C D conclude C D).
Herbrand's theorem can also be obtained by using cut elimination, via Gentzen's "midsequent theorem." However, the proof using the second epsilon theorem has the distinction of being the first complete and correct proof of Herbrand's theorem. Moreover, and this is seldom recognized, whereas the proof based on cutelimination provides a bound on the length of the Herbrand disjunction only as a function of the cut rank and complexity of the cut formulas in the proof, the length obtained from the proof based on the epsilon calculus provides a bound as a function of the number of applications of the transfinite axiom, and the rank and degree of the epsilonterms occurring therein. In other words, the length of the Herbrand disjunction depends only on the quantificational complexity of the substitutions involved, and, e.g., not at all on the propositional structure or the length of the proof.
The version of Herbrand's theorem stated at the beginning of this section is essentially the special case of (2) in which the formula A is existential. In light of this special case, (1) is equivalent to the assertion that a formula A is derivable in firstorder predicate logic if and only if A^{H} is. The forward direction of this equivalence is much easier to prove; in fact, for any formula A, A A^{H} is derivable in predicate logic. Proving the reverse direction involves eliminating the additional function symbols in A^{H}, and is much more difficult, especially in the presence of equality. It is here that epsilon methods play a central role.
Given a prenex formula, the Skolem normal form A^{S} is defined dually to A^{H}, i.e., by replacing existentially quantified variables by witnessing functions. If is a set of prenex sentences, let ^{S} denote the set of their Skolem normal forms. Using the deduction theorem and Herbrand's theorem, it is not hard to show that the following are pairwise equivalent:
As noted above, historically, the primary interest in the epsilon calculus was as a means to obtaining consistency proofs. Hilbert's lectures from 19171918 already note that one can easily prove the consistency of propositional logic, by taking propositional variables and formulae to range over truth values 0 and 1, and interpreting the logical connectives as the corresponding arithmetic operations. Similarly, one can prove the consistency of predicate logic (or the pure epsilon calculus), by specializing to interpretations where the universe of discourse has a single element. These considerations suggest the following more general program for proving consistency:
For example, consider the language of arithmetic, with symbols for 0, 1, +, , <. Along with quantifierfree axioms defining the basic symbols, one can specify that the epsilon terms x A(x) picks out the least value satisfying A , if there is one, with the following axiom:
(*) A(x) A(x A(x)) x A(x) x
The result is a system that is strong enough to interpret firstorder (Peano) arithmetic. Alternatively, one can take the epsilon symbol to satisfy the following axiom:
A(y) A(x A(x)) x A(x) y + 1.
In other words, if there is any witness y satisfying A(y), the epsilon term returns a value whose predecessor does not have the same property. Clearly the epsilon term described by (*) satisfies the alternative axiom; conversely, one can check that given A, a value of x (z x A(x)) satisfying the alternative axiom can be used to interpret x A(x) in (*). One can further fix the meaning of the epsilon term with the axiom
x A(x) 0 A(x A(x))
which requires that if there is no witness to A, the epsilon term return 0. For the discussion below, however, it is most convenient to focus on (*) alone.
Suppose we wish to show that the system above is consistent; in other words, we wish to show that there is no proof of the formula 0 = 1. By pushing all substitutions to the axioms and replacing free variables by the constant 0, it suffices to show that there is no propositional proof of 0 = 1 from a finite set of closed instances of the axioms. For that, it suffices to show that, given any finite set of closed instances of axioms, one can assign numerical values to terms in such a way that all the axioms are true under the interpretation. Since the arithmetical operations + and can be interpreted in the usual way, the only difficulty lies in finding appropriate values to assign to the epsilon terms.
Hilbert's epsilon substitution method can be described, roughly, as follows:
A finitistic consistency proof is obtained once it is shown in a finitistically acceptable manner that this process of successive "repairs" terminates. If it does, all critical formulas are true formulas without epsilonterms.
This basic idea (the "Hilbertsche Ansatz") was set out first by Hilbert in his 1922 talk (1923), and elaborated in lectures in 192223. The examples given there, however, only deal with proofs in which all instances of the transfinite axiom correspond to a single epsilon term x A(x). The challenge was to extend the approach to more than one epsilon term, to nested epsilon terms, and ultimately to secondorder epsilons (in order to obtain a consistency proof not just of arithmetic, but of analysis).
The difficulty in dealing with nested epsilon terms can be described as follows. Suppose one of the axioms in the proof is the transfinite axiom
B(y) B(y B(y))
y B(y) may, of course, occur in other formulae in the proof, in particular in other transfinite axioms, e.g.,
A(x, y B(y)) A(x A(x, y B(y)), y B(y))
So first, it seems necessary to find a correct interpretation for y B(y) before we attempt to find one for x A(x, y B(y)). However, there are more complicated patterns in which epsilon terms may occur in a proof. An instance of the axiom, which plays a role in determining the correct interpretation for y B(y) might be
B(x A(x, y B(y))) B(y B(y))
If B(0) is false, then in the first round of the procedure y B(y) will be interpreted by 0. A subsequent change of the interpretation of x A(x, 0) from 0 to, say, n, will result in an interpretation of this instance as B(n) B(0) which will be false if B(n) is true. So the interpretation of y B(y) will have to be corrected to n, which, in turn, might result in the interpretation of x A(x, y B(y)) to no longer be a true formula.
This is just a sketch of the difficulties involved in extending Hilbert's idea to the general case. Ackermann (1924) provided such a generalization using a procedure which "backtracks" whenever a new interpretation at a given stage results in the need to correct an interpretation already found at a previous stage.
Ackermann's procedure applied to a system of secondorder arithmetic, in which, however, second order terms were restricted so as to exclude crossbinding of secondorder epsilons. This amounts, roughly, to a restriction to arithmetic comprehension as the setforming principle available (see the discussion at the end of this section). Further difficulties with secondorder epsilon terms surfaced, and it quickly became apparent that the proof as it stood was fallacious. However, no one in Hilbert's school realized the extent of the difficulty until 1930, when Gödel announced his incompleteness results. Until then, it was believed that the proof (at least with some modifications introduced by Ackermann, some of which involved ideas from von Neumann's (1927) version of the epsilon substitution method) would go through at least for the firstorder part. Hilbert and Bernays (1939) suggest that the methods used only provides a consistency proof for firstorder arithmetic with open induction. In 1936, Gerhard Gentzen succeeded in giving a proof of the consistency of firstorder arithmetic in a formulation based on predicate logic without the epsilon symbol. This proof uses transfinite induction up to _{0}. Ackermann (1940) was later able to adapt Gentzen's ideas to give a correct consistency proof of firstorder arithmetic using the epsilonsubstitution method.
Even though Ackermann's attempts at a consistency proof for secondorder arithmetic were unsuccessful, they provided a clearer understanding of the use of secondorder epsilon terms in the formalization of mathematics. Ackermann used secondorder epsilon terms f A(f), where f is a function variable. In analogy with the firstorder case, f A(f) is a function for which A(f) is true, e.g., f (x + f(x) = 2x) is the identity function f(x) = x . Again in analogy with the firstorder case, one can use secondorder epsilons to interpret secondorder quantifiers. In particular, for any secondorder formula A(x) one can find a term t(x) such that
A(x) t(x) = 1
is derivable in the calculus (the formula A may have other free variables, in which case these appear in the term t as well). One can then use this fact to interpret comprehension principles. In a language with function symbols, these take the form
f x (A(x) f(x) = 1)
for an arbitrary formula A(x). Comprehension is more commonly expressed in terms of set variables, in which case it takes the form
Y x (A(x) x Y),
asserting that every second order formula, with parameters, defines a set.
Analysis, or secondorder arithmetic, is the extension of firstorder arithmetic with the comprehension schema for arbitrary secondorder formulae. The theory is impredicative in that it allows one to define sets of natural numbers using quantifiers that range over the entire universe of sets, including, implicitly, the set being defined. One can obtain predicative fragments of this theory by restricting the type of formulae allowed in the comprehension axiom. For example, the restriction discussed in connection with Ackermann above corresponds to the arithmetic comprehension schema, in which formulae do not involve secondorder quantifiers. There are various ways of obtaining stronger fragments of analysis that are nonetheless predicatively justified. For example, one obtains ramified analysis by associating an ordinal rank to set variables; roughly, in the definition of a set of a given rank, quantifiers range only over sets of lower rank, i.e., those whose definitions are logically prior.
In this section we discuss the development of the epsilonsubstitution method for obtaining consistency results for strong systems; these results are of a mathematical nature. We cannot, unfortunately, discuss the details of the proofs here but would like to indicate that the epsilonsubstitution method did not die with Hilbert's program, and that a significant amount of current research is carried out in epsilonformalisms.
Gentzen's consistency proofs for arithmetic launched a field of research known as ordinal analysis, and the program of measuring the strength of mathematical theories using ordinal notations is still pursued today. This is particularly relevant to the extended Hilbert's program, where the goal is to justify classical mathematics relative to constructive, or quasiconstructive, systems. Gentzen's methods of cutelimination (and extensions to infinitary logic developed by Paul Lorentzen, Petr Novikov, and Kurt Schütte) have, in large part, supplanted epsilon substitution methods in these pursuits. But epsilon calculus methods provide an alternative approach, and there is still active research on ways to extend HilbertAckermann methods to stronger theories. The general pattern remains the same:
Since the last step guarantees the consistency of the original theory, from a foundational point of view one is interested in the methods used to prove normalization. For example, one obtains an ordinal analysis by assigning ordinal notations to steps in the procedure, in such a way that the value of a notation decreases with each step.
In the 1960's, William Tait extended Ackermann's methods to obtain an ordinal analysis of extensions of arithmetic with principles of transfinite induction. More recently, Grigori Mints, Sergei Tupailo, and Wilfried Buchholz have considered stronger, yet still predicatively justifiable, fragments of analysis, including theories of arithmetic comprehension and a ^{1}_{1}comprehension rule. Toshiyasu Arai has extended the epsilon substitution method to theories that allow one to iterate arithmetic comprehension along primitive recursive well orderings. In particular, his work yields ordinal analyses for predicative fragments of analysis involving transfinite hierarchies and transfinite induction.
As this article is being written, some first steps have been taken in using epsilon substitution method in the analysis of impredicative theories. See the annotated bibliography below.
A variation on step 3 above involves showing that the normalization procedure is not sensitive to the choice of updates, which is to say, any sequence of updates terminates. This is called strong normalization. Mints has shown that many of the procedures considered have this stronger property.
In addition to the traditional, foundational branch of proof theory,
today there is a good deal of interest in structural proof
theory, a branch of the subject that focuses on logical
deductive calculi and their properties. This research is closely
linked with issues relevant to computer science, having to do with
automated deduction, functional programming, and computer aided
verification. Here, too, Gentzenstyle methods tend to dominate
(see, e.g., TroelstraSchwichtenberg (2000)). But the epsilon
calculus can also provide valuable insights; cf. for example Mints
(2002) or the discussion of Herbrand's theorem above.
Aside from the investigations of the epsilon calculus in proof theory, two applications should be mentioned. One is the use of epsilon notation in Bourbaki's Theorie des ensembles (1958). The second, of perhaps greater current interest, is the use of the epsilonoperator in the theoremproving systems HOL and Isabelle, where the expressive power of epsilonterms yields significant practical advantages.
Reading the epsilon operator as an indefinite choice operator ("an x such that A(x)") suggests that it might be a useful tool in the analysis of indefinite and definite noun phrases in formal semantics. The epsilon notation has in fact been so used, and this application has proved useful in particular in dealing with anaphoric reference.
Consider the familiar example
The generally accepted analysis of this sentence is given by the universal sentence
The drawback is that "a donkey" suggest an existential quantifier, and thus the analysis should, somehow, parallel in form the analysis of sentence 3 given by 4:
but the closest possible formalization,
contains a free occurrence of y. Evans suggests that since pronouns are referring expressions, they should be analyzed as definite descriptions; and if the pronoun occurs in the consequent of a conditional, the descriptive conditions are determined by the antecedent. This leads to the following Etype analysis of (1):
x ((Farmer(x) y (Donkey(y) Owns(x, y)) Beats(x, y ( Donkey(y) Owns(x, y)))
(x is the definite description operator). The trouble with this is that on the standard analysis, the definite description carries a uniqueness condition, and so (5) will be false if there is a farmer who owns more than one donkey. A way out of this is to introduce a new operator, whe (whoever, whatever) which works as a generalizing quantor (Neale, 1991):
x ((Farmer(x) y (Donkey(y) Owns(x, y)) Beats(x, whe y (Donkey(y) Owns(x, y)))
As pointed out by von Heusinger (1994), this suggests that Neale is committed to pronouns being ambiguous between definite descriptions (expressions) and wheexpressions. Heusinger suggests instead to use epsilon operators indexed by choice functions (which depend on the context). According to this approach, the analysis of (1) is
For every choice function i:
x (Farmer(x) Owns(x, _{i}y Donkey (y)) Beats (x, _{a*} y Donkey (y))
a* is a choice function which depends on i and the antecedent of the conditional: If i is a choice function which selects _{i}y Donkey (y) from the set of all donkeys, then _{a*} y Donkey (y) selects from the set of donkeys owned by x.
This approach to dealing with pronouns using epsilon operators indexed by choice functions enable von Heusinger to deal with a wide variety of circumstances (see Egli and von Heusinger, 1995; von Heusinger, 2000).
Applications of the epsilonoperator in formal semantics, and choice functions in general, have received significant interest in recent years. Von Heusinger and Egli (2000a) list, among others, the following: representations of questions (Reinhart, 1992), specific indefinites (Reinhart 1992; 1997; Winter 1997), Etype pronouns (Hintikka and Kulas 1985; Slater 1986; Chierchia 1992, Egli and von Heusinger 1995) and definite noun phrases (von Heusinger, 1997).
For discussion of the issues and applications of the epsilon operator in linguistics and philosophy of language, see B. H. Slater's article on epsilon calculi (cited in the Other Internet Resources section below), and the collections (available online) edited by von Heusinger et al., listed in the Bibliography.
Another application of epsilon calculus is as a general logic for reasoning about arbitrary objects. Meyer Viol (1995) provides a comparison of the epsilon calculus with Fine's (1985) theory of arbitrary objects. Indeed, the connection is not hard to see. Given the equivalence x A(x) A(x (A)), the term x (A) is an arbitrary object in the sense that it is an object of which A is true iff A is true generally.
Meyer Viol (1995, 1995a) contain further proof and modeltheoretic studies of the epsilon calculus; specifically intuitionistic epsilon calculi. Here, the epsilon theorems no longer hold, i.e., introduction of epsilon terms produces nonconservative extensions of intuitionistic logic. In fact, as was shown by Bell (1993a, 1993b; Meyer Viol, 1995), addition of the epsilon operator to intuitionistic predicate logic allows us to prove the intuitionistically nonvalid principles A A and (A B) (A B). The full principle of the excluded middle can only be proved if we also add epsilon extensionality.
x (A(x) B(x)) x A = x B
This result provides a rigorous justification of Hilbert's original conjecture that the principle of the excluded middle is, in a sense, a special case of the axiom of choice, and that only with epsilon extensionality do we get the full strength of the choice principle.
Other modeltheoretic investigations of epsilon operators in intuitionistic logic can be found in DeVidi (1995). For epsilonoperators in manyvalued logics, see Mostowski (1963), for modal epsilon calculus, Fitting (1975).
The following list of references provides a starting point for exploring the literature, but is by no means comprehensive.
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 original work:
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 nocounterexample 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 firstorder logic, is discussed in
The following contains a number of prooftheoretic results that are proved using methods similar to the ones used by Hilbert, Bernays, and Ackermann, though using Skolem functions instead of epsilon terms:
For more on ordinal analysis, see, for example:
Herbrand's theorem originally appeared in
English translations can be found in van Heijenoort (see above), and
Further historical information can be found in
The literature on Herbrand's theorem is vast. For some general overviews, in addition to the general prooftheoretic references above, see
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 modeltheoretic version of this is discussed in
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:
The following paper shows that the epsilon substitution method for firstorder arithmetic is, in fact, strongly normalizing:
A connection between cut elimination and epsilon substitution method is explored in
The epsilon substitution method has been extended to predicative fragments of secondorder arithmetic in:
The following papers address impredicative theories:
A development of set theory based on the epsiloncalculus is given by
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.
Please contact the authors with further suggestions.
Jeremy Avigad avigad@cmu.edu  Richard Zach rzach@ucalgary.ca 
A  B  C  D  E  F  G  H  I  J  K  L  M  N  O  P  Q  R  S  T  U  V  W  X  Y  Z