# The Epsilon Calculus

*First published Fri May 3, 2002; substantive revision Wed Nov 27, 2013*

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 term-forming 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.

## Overview

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 non-logical 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 set-theoretic 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 first-order 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 first-order consequences. But, conversely, quantifiers can be defined in terms of the epsilons, so first-order logic can be understood in terms of quantifier-free 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 quantifier-free calculi. Hilbert expected that it would be possible to demonstrate the consistency of such extensions.

## The Epsilon Calculus

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 epsilon-calculus can be found in Wilhelm Ackermann's dissertation (1924).

This section will describe a version of the calculus corresponding to first-order logic, while extensions to first- and second-order arithmetic will be described below.

Let *L* be a first-order 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:

- Each constant of
*L*is a term. - Each variable is a term.
- If
*s*and*t*are terms, then*s*=*t*is a formula. - If
*s*_{1}, …,*s*are terms and_{k}*F*is a*k*-ary function symbol of*L*,*F*(*s*_{1}, …,*s*) is a term._{k} - If
*s*_{1}, …,*s*are terms and_{k}*R*is a*k*-ary relation symbol of*L*,*R*(*s*_{1}, …,*s*) is a formula._{k} - If
*A*and*B*are formulae, so are*A*∧*B*,*A*∨*B*,*A*→*B*, and ¬*A*. - If
*A*is a formula and*x*is a variable, ε*x**A*is a term.

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:

- Modus ponens
- Substitution: from
*A*(*x*), conclude*A*(*t*), for any term*t.*

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 quantifier-free.
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 first-order 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 terms 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 Epsilon Theorems

The second volume of Hilbert and Bernays' *Grundlagen der
Mathematik* (1939) provides an account of results on the
epsilon-calculus that had been proved by that time. This includes a
discussion of the first and second epsilon theorems with applications
to first-order logic, the epsilon substitution method for arithmetic
with open induction, and a development of analysis (that is,
second-order arithmetic) with the epsilon calculus.

The first and second epsilon theorems are as follows:

**First epsilon theorem:** Suppose Γ ∪
{*A*} is a set of quantifier-free formulae not involving the
epsilon symbol. If *A* is derivable from Γ in the epsilon
calculus, then *A* is derivable from Γ in quantifier-free
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, “quantifier-free predicate logic” is intended to include the substitution rule above, so quantifier-free axioms behave like their universal closures. Since the epsilon calculus includes first-order logic, the first epsilon theorem implies that any detour through first-order predicate logic used to derive a quantifier-free theorem from quantifier-free 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 quantifier-free formula from other quantifier-free formulae. This is of particular importance for Hilbert's program, since the epsilons play the role of ideal elements in mathematics. If quantifier-free formulae correspond to the “real” part of the mathematical theory, the first epsilon-theorem 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 epsilon-theorem, 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
epsilon-free, 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 epsilon-free 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.

## Herbrand's Theorem

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 first-order predicate logic (without equality),
where *A* is quantifier-free, 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 first-order 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 “quasi-tautology” 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 quantifier-free. 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 first-order
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_{4}(t_{1}^{n},t_{3}^{n}))

is a quasi-tautology.

The second clause of the theorem below, in this particular instance,
says that the formula *A* above is derivable in first-order
logic if and only if there are sequences of variables
*x*_{2}^{1} ,
*x*_{4}^{1},…,
*x*_{2}* ^{n}* ,

*x*

_{4}

*and terms*

^{n}*s*

_{1}

^{1},

*s*

_{3}

^{1},…,

*s*

_{1}

*,*

^{n}*s*

_{3}

*in the*

^{n}*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 quasi-tautology, 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}xB(_{n}x_{1}, …,x),_{n}

where *B* is quantifier-free. 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*by_{i}*f*(_{i}*x*_{i}^{1}, …,*x*), where_{i}^{k(i)}*x*_{i}^{1}, …,*x*are the variables corresponding to the existential quantifiers preceding_{i}^{k(i)}**Q**in_{i}*A*(in order), and*f*is a new function symbol designated for this role._{i}

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 quasi-tautology.

(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 quasi-tautology, and *A* is derivable from
∨_{j}
*B*_{j} using the following rules:

- from
*C*_{1}∨ … ∨*C*_{i}(*t*) ∨ … ∨*C*_{m}

conclude*C*_{1}∨ … ∨ ∃*x**C*_{i}(*x*) ∨ … ∨*C*_{m}and

- from
*C*_{1}∨ … ∨*C*_{i}(*x*) ∨ … ∨*C*_{m}

conclude*C*_{1}∨ … ∨ ∀*x**C*_{i}(*x*) ∨ … ∨*C*_{m}(if*x*not in*C*_{j}for*j*≠*i*),

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 cut-elimination 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 epsilon-terms 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
first-order 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:

- Γ proves
*A* - Γ proves
*A*^{H} - Γ
^{S}proves*A* - Γ
^{S}proves*A*^{H}

## The Epsilon Substitution Method and Arithmetic

As noted above, historically, the primary interest in the epsilon calculus was as a means to obtaining consistency proofs. Hilbert's lectures from 1917–1918 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:

- Extend the epsilon calculus in such a way as to represent larger portions of mathematics.
- Show, using finitary methods, that each proof in the extended system has a consistent interpretation.

For example, consider the language of arithmetic, with symbols for
0, 1, +, ×, <. Along with quantifier-free 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 first-order (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:

- Given a finite set of axioms, start by interpreting all epsilon terms as 0.
- Find an instance of the axiom (*) above that is false under the
interpretation. This can only happen if one has a term t such that
*A*(*t*) is true in the interpretation, but either*A*(ε*x A*(*x*)) is false or the value of*t*is smaller than the value of ε*x A*(*x*). - “Repair” the assignment by assigning to ε
*x A*(*x*) the value of*t*, and repeat the process.

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 epsilon-terms.

This basic idea (the “Hilbertsche Ansatz”) was set out first by
Hilbert in his 1922 talk (1923), and elaborated in lectures in 1922–23.
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 second-order 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 second-order
arithmetic, in which, however, second order terms were restricted so as
to exclude cross-binding of second-order epsilons. This amounts,
roughly, to a restriction to arithmetic comprehension as the
set-forming principle available (see the discussion at the end of this
section). Further difficulties with second-order 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 first-order part. Hilbert and Bernays
(1939) suggest that the methods used only provides a consistency proof
for first-order arithmetic with open induction. In 1936, Gerhard
Gentzen succeeded in giving a proof of the consistency of first-order
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 first-order
arithmetic using the epsilon-substitution method.

Even though Ackermann's attempts at a consistency proof for
second-order arithmetic were unsuccessful, they provided a clearer
understanding of the use of second-order epsilon terms in the
formalization of mathematics. Ackermann used second-order epsilon terms
ε*f A*(*f*), where *f* is a function
variable. In analogy with the first-order case, ε*f
A*(*f*) is a function for which *A*(*f*) is
true, e.g., ε*f* (*x* + *f*(*x*) =
2*x*) is the identity function *f*(*x*) =
*x*. Again in analogy with the first-order case, one can use
second-order epsilons to interpret second-order quantifiers. In
particular, for any second-order 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 *second-order arithmetic*, is the
extension of first-order arithmetic with the comprehension schema for
arbitrary second-order 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
second-order 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.

## More Recent Developments

In this section we discuss the development of the epsilon-substitution 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 epsilon-substitution method did not die with Hilbert's program, and that a significant amount of current research is carried out in epsilon-formalisms.

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 quasi-constructive,
systems. Gentzen's methods of cut-elimination (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 Hilbert-Ackermann methods to stronger theories. The general
pattern remains the same:

- Embed the theory under investigation in an appropriate epsilon calculus.
- Describe a process for updating assignments to the epsilon terms.
- Show that the procedure is normalizing, i.e., given any set of terms, there is a sequence of updates that results in an assignment that satisfies the axioms.

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.

Some first steps have been taken by Arai and Mints
in using the 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, Gentzen-style methods tend to dominate (see, e.g.,
Troelstra-Schwichtenberg (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
epsilon-operator in the theorem-proving systems
HOL
and
Isabelle,
where the expressive power of
epsilon-terms yields significant practical advantages.

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

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

- Every farmer who owns a donkey beats it.

The generally accepted analysis of this sentence is given by the universal sentence

- ∀
*x*∀*y*(*Farmer*(*x*) ∧*Donkey*(*y*) ∧*Owns*(*x*,*y*)) →*Beats*(*x*,*y*))

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:

- Every farmer who owns a donkey is happy,
- ∀
*x*(*Farmer*(*x*) ∧ ∃*y*(*Donkey*(*y*) ∧*Owns*(*x*,*y*)) →*Happy*(*x*)),

but the closest possible formalization,

- ∀
*x*((*Farmer*(*x*) ∧ ∃*y*(*Donkey*(*y*) ∧*Owns*(*x*,*y*)) →*Beats*(*x*,*y*))

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 E-type 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, whey(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 whe-expressions. 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}yDonkey(y)) →Beats(x, ε_{a*}yDonkey(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 epsilon-operator 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), E-type pronouns (Hintikka and Kulas 1985; Slater 1986; Chierchia 1992, Egli and von Heusinger 1995) and definite noun phrases (von Heusinger, 1997, 2004).

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 model-theoretic studies of the epsilon calculus; specifically intuitionistic epsilon calculi. Here, the epsilon theorems no longer hold, i.e., introduction of epsilon terms produces non-conservative extensions of intuitionistic logic. Other investigations of epsilon operators in intuitionistic logic can be found in Bell (1993a, 1993b) and DeVidi (1995). For epsilon-operators in many-valued logics, see Mostowski (1963), for modal epsilon calculus, Fitting (1975).

## Bibliography

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. - Ewald, W. B. (ed.), 1996,
*From Kant to Hilbert. A Source Book in the Foundations of Mathematics*, Vol. 2, Oxford: Oxford University Press. - Mancosu, P. (ed.), 1998,
*From Brouwer to Hilbert. The Debate on the Foundations of Mathematics in the 1920s*, Oxford: Oxford University Press. - van Heijenoort, J. (ed.), 1967,
*From Frege to G*ö*del. A Source Book in Mathematical Logic*, Cambridge, Mass.: Harvard University Press.

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].
- 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.
- Mancosu, P., 1998a, ‘Hilbert and Bernays on metamathematics’, in Mancosu, 1998, 149–188.
- Moore, G. H., 1997, ‘Hilbert and the emergence of modern
mathematical logic’,
*Theoria*(Segunda Epoca), 12: 65–90. - Peckhaus, V., 1990,
*Hilbertprogramm und Kritische Philosophie*, Göttingen: Vandenhoek & Ruprecht. - Sieg, W., 1988, ‘Hilbert's program sixty years later’,
*Journal of Symbolic Logic*, 53: 338–348. - Sieg, W., 1990, ‘Reflections on Hilbert's program’, W.
Sieg (ed.),
*Acting and Reflecting*, Dordrecht: Kluwer. - Sieg, W., 1999, ‘Hilbert's Programs: 1917–1922’,
*Bulletin of Symbolic Logic*, 5: 1–44 [Available online in Postscript]. - 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]. - Zach, R., 2003, ‘The practice of finitism. Epsilon calculus
and consistency proofs in Hilbert's Program’,
*Synthese*, 137: 211–259. [Preprint available online].

### 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. - Ackermann, W., 1937–38, ‘Mengentheoretische Begründung
der Logik’,
*Mathematische Annalen*, 115: 1–22. - Ackermann, W., 1940, ‘Zur Widerspruchsfreiheit der
Zahlentheorie’,
*Mathematische Annalen*, 117: 162–194. - 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. - Hilbert, D., ‘Die logischen Grundlagen der Mathematik’,
*Mathematische Annalen*, 88: 151–165, English translation in Ewald, 1996, 1134–1148. - Hilbert, D., Bernays, P., 1934,
*Grundlagen der Mathematik*, Vol. 1, Berlin: Springer. - Hilbert, D., Bernays, P., 1939,
*Grundlagen der Mathematik*, Vol. 2, Berlin: Springer. - von Neumann, J., 1927, ‘Zur Hilbertschen
Beweistheorie’,
*Mathematische Zeitschrift*, 26: 1–46.

Ackermann's 1940 proof is discussed in

- Hilbert, D., Bernays, P., 1970, ‘Grundlagen der Mathematik’, Vol. 2, 2nd, edition, Berlin: Springer, Supplement V.
- Wang, H., 1963,
*A Survey of Mathematical Logic*, Peking: Science Press.

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. - Maehara, S., 1957, ‘Equality axiom on Hilbert's
ε-symbol’,
*Journal of the Faculty of Science*, University of Tokyo, Section 1, 7: 419–435.

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.

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. - Mints, G., 1996, ‘Thoralf Skolem and the epsilon substitution
method for predicate logic’,
*Nordic Journal of Philosophical Logic*, 1: 133–146 [Available online]. - Moser, G., 2000,
*The Epsilon Substitution Method*, Master's Thesis, University of Leeds. - Moser, G., 2006, ‘Ackermann's substitution method
(remixed)’,
*Annals of Pure and Applied Logic*, 142 (1–3): 1–18. [Available online]. - Moser, G., Zach, R., 2006, ‘The epsilon calculus and
Herbrand complexity’,
*Studia Logica*, 82(1): 133–155. [Preprint available online in PDF].

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. - Ferrari, P. L., 1987, ‘A note on a proof of Hilbert's second
ε-theorem’,
*Journal of Symbolic Logic*, 52: 214–215. - Yashahura, M., 1982, ‘Cut elimination in
ε-calculi’,
*Zeitschrift für mathematische Logik und Grundlagen der Mathematik*, 28: 311–316.

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. - Takeuti, G., 1987,
*Proof Theory*, second edition. Amsterdam: North-Holland, Amsterdam. - Troelstra, A. S., Schwichtenberg, H., 2000,
*Basic Proof Theory*, second edition. Cambridge: Cambridge University Press.

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.

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.

### 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.

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

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

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.

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 [Available online in PDF]. - Girard, J.-Y., 1982, ‘Herbrand's theorem and proof
theory’,
*Proceedings of the Herbrand Symposium*, Amsterdam: North-Holland, 29-38. - Statman, R., 1979, ‘Lower bounds on Herbrand's
theorem’,
*Proceedings of the American Mathematical Society*, 75: 104–107. - Voronkov, A., 1999, ‘Simultaneous rigid E-unification and
other decision problems related to the Herbrand theorem’,
*Theoretical Computer Science*, 224: 319–352.

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.

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

- Sieg, W., 1991, ‘Herbrand analyses’,
*Archive for Mathematical Logic*, 30: 409–441.

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*.

### 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. - Tait, W. W., 1965, ‘Functionals defined by transfinite
recursion,’
*Journal of Symbolic Logic*, 30: 155–174.

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. - 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.

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.

Connections between cut elimination and epsilon substitution method are 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. - Mints, G., 2008, ‘Cut Elimination for a Simple Formulation
of Epsilon Calculus’,
*Annals of Pure and Applied Logic*,152 (1–3): 148–160.

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. - Mints, G., Tupailo, S., 1999, ‘Epsilon-substitution method
for the ramified language and
Δ
^{1}_{1}-comprehension rule’, in A. Cantini*et al*. (eds.),*Logic and Foundations of Mathematics*(Florence, 1995), Dordrecht: Kluwer, 107–130. - Arai, T., 2002, ‘Epsilon substitution method for theories of
jump hierarchies’,
*Archive for Mathematical Logic*, 2: 123–153.

The following papers address impredicative theories:

- Arai, T., 2003, ‘Epsilon substitution method for
ID
_{1}(Π^{0}_{1}∨ Σ^{0}_{1})’,*Annals of Pure and Applied Logic*, 121: 163–208. - Mints, G., 2001, ‘An approach to an epsilon-substitution method for ID1’, preprint, Institute Mittag Leffler, 45, MLI, Stockholm.

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

- Bourbaki, N., 1958,
*Theorie des ensembles*, Paris: Hermann.

### 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. - Bell, J. L., 1993b. ‘Hilbert's epsilon operator in
intuitionistic type theories’,
*Mathematical Logic Quarterly*, 39: 323–337. - Chierchia, G., 1992. ‘Anaphora and dynamic logic’.
*Linguistics and Philosophy*, 15: 111–183. - DeVidi, D., 1995. ‘Intuitionistic epsilon- and
tau-calculi’,
*Mathematical Logic Quarterly*41: 523–546. - Evans, G., 1980, ‘Pronouns’,
*Linguistic Inquiry*, , 11: 337–362. - 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). - Fine, K., 1985.
*Reasoning with Arbitrary Objects*, Oxford: Blackwell. - 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. - Kempson, R., Meyer Viol, W., and Gabbay, D., 2001.
*Dynamic Syntax: The Flow of Language Understanding*, Oxford: Blackwell. - 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. - 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. - 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. - Reinhart, T., 1997. ‘Quantifier scope: How labor is divided
between QR and choice functions’.
*Linguistics and Philosophy*, 20: 335–397. - 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. - Slater, B. H. 1994, ‘The epsilon calculus’
problematic’,
*Philosophical Papers*, 23: 217–42. - Slater, B.H. 2000, ‘Quantifier/variable-binding’,
*Linguistics and Philosophy*, 23: 309–21. - von Heusinger, K., 1997. ‘Definite descriptions and choice
functions’. In: S. Akama (ed.).
*Logic, Language and Computation*, Dordrecht: Kluwer, 61–91. - von Heusinger, K., 2000, ‘The Reference of Indefinites’, in von Heusinger and Egli, (2000), 265–284.
- von Heusinger, K., 2004, ‘Choice functions and the anaphoric
semantics of definite NPs’,
*Research in Language and Computation*, 2: 309–329. - von Heusinger, K., Egli, U., (eds.), 2000.
*Reference and Anaphoric Relations*, Dordrecht: Kluwer, 265–284. - von Heusinger, K., Egli, U., 2000a. ‘ Introduction: Reference and the Semantics of Anaphora’, in von Heusinger and Egli (2000), 1–13.
- 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. - Winter, Y., 1997. ‘Choice functions and the scopal semantics
of indefinites’.
*Linguistics and Philosophy*, 20: 399–467.

## Academic Tools

How to cite this entry. Preview the PDF version of this entry at the Friends of the SEP Society. Look up this entry topic at the Indiana Philosophy Ontology Project (InPhO). Enhanced bibliography for this entry at PhilPapers, with links to its database.

## Other Internet Resources

- Epsilon Calculi by B. Hartley Slater (Internet Encyclopedia of Philosophy).

Please contact the authors with further suggestions.

## Related Entries

anaphora | finitism | Hilbert, David | Hilbert, David: program in the foundations of mathematics | logic: classical | mathematics, philosophy of | proof theory | quantifiers and quantification