The epsilon calculus is a logical formalism developed by David Hilbertin the service of his program in the foundations of mathematics. Theepsilon operator is a term-forming operator which replaces quantifiersin ordinary predicate logic. Specifically, in the calculus, a term\(\varepsilon x A\) denotes some \(x\) satisfying \(A(x)\), if thereis one. In Hilbert’s Program, the epsilon terms play the role ofideal elements; the aim of Hilbert’s finitistic consistencyproofs is to give a procedure which removes such terms from a formalproof. The procedures by which this is to be carried out are based onHilbert’s epsilon substitution method. The epsilon calculus,however, has applications in other contexts as well. The first generalapplication of the epsilon calculus was in Hilbert’s epsilontheorems, which in turn provide the basis for the first correct proofof Herbrand’s theorem. Variants of the epsilon operator havebeen applied in linguistics, computer science, and in the philosophyof language, mathematics, and science.

• 1. Overview
• 2. The Epsilon Calculus
• 3. The Epsilon Theorems
• 4. Herbrand’s Theorem
• 5. The Epsilon Substitution Method and Arithmetic
• 6. More Recent Developments
• 7. Epsilon Operators in Linguistics, Philosophy, and Non-classical Logics
• Bibliography
• Academic Tools
• Other Internet Resources
• Related Entries

1. Overview

By the turn of the century David Hilbert and Henri Poincaréwere recognized as the two most important mathematicians of theirgeneration. Hilbert’s range of mathematical interests was broad,and included an interest in the foundations of mathematics: hisFoundations of Geometry was published in 1899, and of thelist of questions posed to the International Congress ofMathematicians in 1900, three addressed distinctly foundationalissues.

Following the publication of Russell’s paradox, Hilbertpresented an address to the Third International Congress ofMathematicians in 1904, where, for the first time, he sketched hisplan to provide a rigorous foundation for mathematics via syntacticconsistency proofs. But he did not return to the subject in earnestuntil 1917, when he began a series of lectures on the foundations ofmathematics with the assistance of Paul Bernays. Although Hilbert wasimpressed by the work of Russell and Whitehead in theirPrincipiaMathematica, he became convinced that the logicist attempt toreduce mathematics to logic could not succeed, due in particular tothe non-logical character of their axiom of reducibility. At the sametime, he judged the intuitionistic rejection of the law of theexcluded middle as unacceptable to mathematics. Therefore, in order tocounter concerns raised by the discovery of the logical andset-theoretic paradoxes, a new approach was needed to justify modernmathematical methods.

By the summer of 1920, Hilbert had formulated such an approach. First,modern mathematical methods were to be represented in formal deductivesystems. Second, these formal systems were to be proved syntacticallyconsistent, not by exhibiting a model or reducing their consistency toanother system, but by a direct metamathematical argument of anexplicit, “finitary” character. The approach became knownasHilbert’s program. The epsilon calculus was to provide the first component of thisprogram, while his epsilon substitution method was to provide thesecond.

The epsilon calculus is, in its most basic form, an extension offirst-order predicate logic with an “epsilon operation”that picks out, for any true existential formula, a witness to theexistential quantifier. The extension is conservative in the sensethat it does not add any new first-order consequences. But,conversely, quantifiers can be defined in terms of the epsilons, sofirst-order logic can be understood in terms of quantifier-freereasoning involving the epsilon operation. It is this latter featurethat makes the calculus convenient for the purpose of provingconsistency. Suitable extensions of the epsilon calculus make itpossible to embed stronger, quantificational theories of numbers andsets in quantifier-free calculi. Hilbert expected that it would bepossible to demonstrate the consistency of such extensions.

2. The Epsilon Calculus

In his Hamburg lecture in 1921 (1922), Hilbert first presented theidea of using such an operation to deal with the principle of theexcluded middle in a formal system for arithmetic. These ideas weredeveloped into the epsilon calculus and the epsilon substitutionmethod in a series of lecture courses between 1921 and 1923, and inHilbert’s (1923). The final presentation of the epsilon-calculuscan be found in Wilhelm Ackermann’s dissertation (1924).

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

Let \(L\) be a first-order language, which is to say, a list ofconstant, function, and relation symbols with specified arities. Theset of epsilon terms and the set of formulae of \(L\) are definedinductively, 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, \ldots, s_k\) are terms and \(F\) is a \(k\)-aryfunction symbol of \(L, F(s_1, \ldots, s_k)\) is a term.
• If \(s_1, \ldots, s_k\) are terms and \(R\) is a \(k\)-aryrelation symbol of \(L, R(s_1, \ldots, s_k)\) is a formula.
• If \(A\) and \(B\) are formulae, so are \((A \wedge B)\), \((A \veeB)\), \((A \rightarrow B)\), and \(\neg A\).
• If \(A\) is a formula and \(x\) is a variable, \(\varepsilon x A\)is a term.

Parentheses may be dropped when there is no ambiguity.Substitution and the notions of free and bound variable, are definedin the usual way; in particular, the variable \(x\) becomes bound inthe term \(\varepsilon x A\). The intended interpretation is that\(\varepsilon x A\) denotessome \(x\) satisfying \(A\), ifthere is one. Thus, the epsilon terms are governed by the followingaxiom (Hilbert’s “transfinite axiom”): \[ A(x)\rightarrow A(\varepsilon x A) \]In addition, the epsilon calculus includes a complete set of axiomsgoverning the classical propositional connectives, and axiomsgoverning the equality symbol. The only rules of the calculus are thefollowing:

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

Earlier forms of the epsilon calculus (such as that presented inHilbert 1923) use a dual form of the epsilon operator, in which\(\varepsilon x A\) returns a valuefalsifying \(A(x)\). Theversion above was used in Ackermann’s dissertation (1924), andhas become standard.

Note that the calculus just described is quantifier-free. Quantifierscan bedefined as follows: \[ \begin{align}\exists x A(x) &\equiv A(\varepsilon x A) \\ \forall x A(x) &\equiv A(\varepsilon x (\neg A)) \end{align} \] The usual quantifieraxioms and rules can be derived from these, so the definitions aboveserve to embed first-order logic in the epsilon calculus. The converseis, however, not true: not every formula in the epsilon calculus isthe image of an ordinary quantified formula under this embedding.Hence, the epsilon calculus is more expressive than the predicatecalculus, simply because epsilon terms can be combined in more complexways than quantifiers.

It is worth noting that epsilon terms are nondeterministic. Forexample, in a language with constant symbols \(a\) and \(b\),\(\varepsilon x (x = a \vee x = b)\) is either \(a\) or \(b\), but thecalculus leaves it entirely open as to which is the case. One can addto the calculus a schema ofextensionality, \[ \forall x (A(x) \leftrightarrow B(x)) \rightarrow \varepsilon x A = \varepsilon x B \] whichasserts that the epsilon operator assigns the same witness toequivalent formulae \(A\) and \(B\). For many applications, however,this additional schema is not necessary.

3. The Epsilon Theorems

The second volume of Hilbert and Bernays’Grundlagen derMathematik (1939) provides an account of results on theepsilon-calculus that had been proved by that time. This includes adiscussion of the first and second epsilon theorems with applicationsto first-order logic, the epsilon substitution method for arithmeticwith 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 \(\Gamma \cup \{A\}\)is a set of quantifier-free formulae not involving the epsilon symbol.If \(A\) is derivable from \(\Gamma\) in the epsilon calculus, then\(A\) is derivable from \(\Gamma\) in quantifier-free predicatelogic.

Second epsilon theorem: Suppose \(\Gamma \cup \{A\}\)is a set of formulae not involving the epsilon symbol. If \(A\) isderivable from \(\Gamma\) in the epsilon calculus, then \(A\) isderivable from \(\Gamma\) in predicate logic.

In the first epsilon theorem, “quantifier-free predicatelogic” is intended to include the substitution rule above, soquantifier-free axioms behave like their universal closures. Since theepsilon calculus includes first-order logic, the first epsilon theoremimplies that any detour through first-order predicate logic used toderive a quantifier-free theorem from quantifier-free axioms canultimately be avoided. The second epsilon theorem shows that anydetour through the epsilon calculus used to derive a theorem in thelanguage of the predicate calculus from axioms in the language of thepredicate calculus can also be avoided.

More generally, the first epsilon theorem establishes that quantifiersand epsilons can always be eliminated from a proof of aquantifier-free formula from other quantifier-free formulae. This isof particular importance for Hilbert’s program, since theepsilons play the role of ideal elements in mathematics. Ifquantifier-free formulae correspond to the “real” part ofthe mathematical theory, the first epsilon-theorem shows that idealelements can be eliminated from proofs of real statements, providedthe axioms are also real statements.

This idea is made precise in a certain general consistency theoremwhich Hilbert and Bernays derive from the first epsilon-theorem, whichsays the following: Let \(F\) be any formal system which results fromthe predicate calculus by addition of constant, function, andpredicate symbols plus true axioms which are quantifier- andepsilon-free, and suppose the truth of atomic formulae in the newlanguage is decidable. Then \(F\) is consistent in the strong sensethat every derivable quantifier- and epsilon-free formula is true.Hilbert and Bernays use this theorem to give a finitary consistencyproof of elementary geometry (1939, Sec 1.4).

The difficulty for giving consistency proofs for arithmetic andanalysis consists in extending this result to cases where the axiomsalso contain ideal elements, i.e., epsilon terms.

Further reading. The original sources on the epsilon-calculusand the epsilon theorems (Ackermann 1924, Hilbert & Bernays 1939)remain available only in German. Leisenring 1969 is a relativelymodern book-length introduction to the epsilon calculus in English.The first and second epsilon theorem are described in detail in Zach2017. Moser & Zach 2006 give a detailed analysis for the casewithout equality, and Miyamoto & Moser 2024 for the case withequality. The original proofs are given for axiomatic presentations ofthe epsilon-calculus. Maehara 1955 was the first to consider sequentcalculus with epsilon terms. He showed how to prove the second epsilontheorem using cut elimination, and then strengthened the theorem toinclude the schema of extensionality (Maehara 1957). Baaz et al. 2018give an improved version of the first epsilon theorem. Corrections toerrors in the literature (including Leisenring’s book) can befound in Flannagan 1975; Ferrari 1987; and Yasuhara 1982. A variationof the epsilon calculus based on Skolem functions, and thereforecompatible with first-order logic, is discussed in Davis & Fechter1991.

4. Herbrand’s Theorem

Hilbert and Bernays used the methods of the epsilon calculus toestablish theorems about first order logic that make no reference tothe epsilon calculus itself. One such example isHerbrand’stheorem (Herbrand 1930; see Buss 1995, Girard 1982, and section2.5 of Buss 1998). This is often formulated as the statement that ifan existential formula \[ \exists x_1 \ldots \exists x_k A(x_1, \ldots, x_k) \] is derivable in first-orderpredicate logic (without equality), where \(A\) is quantifier-free,then there are sequences of terms \(t_{1}^1, \ldots, t_{k}^1, \ldots,t_{1}^n, \ldots, t_k ^n\), such that \[ A(t_{1}^1, \ldots, t_k ^1) \vee \ldots \vee A(t_{1}^n, \ldots, t_k^n) \] is a tautology. Ifone is dealing with first-order logicwith equality, one hasto replace “tautology” by “tautological consequenceof substitution instances of the equality axioms”; we will usethe term “quasi-tautology” to describe such a formula.

The version of Herbrand’s theorem just described followsimmediately from theExtended First Epsilon Theorem ofHilbert and Bernays. Using methods associated with the proof of thesecond epsilon theorem, however, Hilbert and Bernays derived astronger result that, like Herbrand’s original formulation,provides more information. To understand the two parts of the theorembelow, it helps to consider a particular example. Let \(A\) be theformula

The first clause of the theorem below, in this particular instance,says that the formula \(A\) above is derivable in first-order logic ifand only if there is a sequence of terms \(t_{1}^1, t_{3}^1, \ldots,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)) \vee \ldots \vee 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 ifand only if there are sequences of variables \(x_{2}^1, x_{4}^1,\ldots, x_2^n, x_4 ^n\) and terms \(s_{1}^1, s_{3}^1, \ldots, s_1^n,s_3 ^n\) in theoriginal language such that \[ B(s_{1}^1, x_{2}^1, s_{3}^1, x_4 ^1 ) \vee \ldots \vee B(s_1^n, x_2^n, s_3^n, x_4^n ) \] is aquasi-tautology, and such that \(A\) is derivable from this formulausing only the quantifier and idempotency rules described below.

More generally, suppose \(A\) is any prenex formula, of the form\[ \mathbf{Q}_1 x_1 \ldots \mathbf{Q}_n x_n B(x_1, \ldots, x_n), \] where \(B\) is quantifier-free. Then \(B\) is said to bethematrix of \(A\), and aninstance of \(B\) isobtained by substituting terms in the language of \(B\) for some ofits variables. TheHerbrand normal form \(A^H\) of \(A\) isobtained by

• deleting each universal quantifier, and
• replacing each universally quantified variable \(x_i\) by \(f_i(x_{i}^1,\ldots, x_{i}^{k(i)})\), where \(x_{i}^1,\ldots,x_{i}^{k(i)}\) are the variables corresponding to the existentialquantifiers preceding \(\mathbf{Q}_i\) in \(A\) (in order), and\(f_i\) is a new function symbol designated for this role.

When we refer to aninstance of the matrix of \(A^H\), wemean a formula that is obtained by substituting terms in the expandedlanguage in the matrix of \(A^H\). We can now state Hilbert andBernays’s formulation of

Herbrand’s theorem can also be obtained by using cutelimination, via Gentzen’s “midsequent theorem.”However, the proof using the second epsilon theorem has thedistinction of being the first complete and correct proof ofHerbrand’s theorem. Moreover, and this is seldom recognized,whereas the proof based on cut-elimination provides a bound on thelength of the Herbrand disjunction only as a function of the cut rankand complexity of the cut formulas in the proof, the length obtainedfrom the proof based on the epsilon calculus provides a bound as afunction of the number of applications of the transfinite axiom, andthe rank and degree of the epsilon-terms occurring therein. In otherwords, the length of the Herbrand disjunction depends only on thequantificational complexity of the substitutions involved, and, e.g.,not at all on the propositional structure or the length of theproof.

The version of Herbrand’s theorem stated at the beginning ofthis section is essentially the special case of (2) in which theformula \(A\) is existential. In light of this special case, (1) isequivalent to the assertion that a formula \(A\) is derivable infirst-order predicate logic if and only if \(A^H\) is. The forwarddirection of this equivalence is much easier to prove; in fact, forany formula \(A, A \rightarrow A^H\) is derivable in predicate logic.Proving the reverse direction involves eliminating the additionalfunction symbols in \(A^H\), and is much more difficult, especially inthe presence of equality. It is here that epsilon methods play acentral role.

Given a prenex formula, theSkolem normal form \(A^S\) isdefined dually to \(A^H\), i.e., by replacing existentially quantifiedvariables by witnessing functions. If \(\Gamma\) is a set of prenexsentences, let \(\Gamma^S\) denote the set of their Skolem normalforms. Using the deduction theorem and Herbrand’s theorem, it isnot hard to show that the following are pairwise equivalent:\[ \begin{align}\Gamma &\text{ proves } A \\ \Gamma &\text{ proves } A^H \\ \Gamma^S &\text{ proves }A \\ \Gamma^S &\text{ proves } A^H \end{align} \]

A striking application of Herbrand’s theorem and related methodsis found in Luckhardt’s (1989) analysis of Roth’s theorem.For a discussion of useful extensions of Herbrand’s methods, seeSieg 1991. A model-theoretic version of this is discussed in Avigad2002a.

5. The Epsilon Substitution Method and Arithmetic

As noted above, historically, the primary interest in the epsiloncalculus was as a means to obtaining consistency proofs.Hilbert’s lectures from 1917–1918 already note that onecan easily prove the consistency of propositional logic, by takingpropositional variables and formulae to range over truth values 0 and1, and interpreting the logical connectives as the correspondingarithmetic operations. Similarly, one can prove the consistency ofpredicate logic (or the pure epsilon calculus), by specializing tointerpretations where the universe of discourse has a single element.These considerations suggest the following more general program forproving consistency:

• Extend the epsilon calculus in such a way as to represent largerportions of mathematics.
• Show, using finitary methods, that each proof in the extendedsystem has a consistent interpretation.

For example, consider the language of arithmetic, with symbols for\(0\), \(1\), \(+\), \(\times\), \(\lt\). Along with quantifier-freeaxioms defining the basic symbols, one can specify that the epsilonterms \(\varepsilon x A(x)\) picks out the least value satisfying\(A\), if there is one, with the following axiom: \[ \tag{*} A(x) \rightarrow A(\varepsilon x A(x)) \wedge \varepsilon x A(x) \le x \] Theresult is a system that is strong enough to interpret first-order(Peano) arithmetic. Alternatively, one can take the epsilon symbol tosatisfy the following axiom: \[ A(y) \rightarrow A(\varepsilon x A(x)) \wedge \varepsilon x A(x) \ne y + 1. \]

In other words, if there is any witness \(y\) satisfying \(A(y)\), theepsilon term returns a value whose predecessor does not have the sameproperty. Clearly the epsilon term described by (*) satisfies thealternative axiom; conversely, one can check that given \(A\), a valueof \(\varepsilon x (\exists z \le x A(x))\) satisfying the alternativeaxiom can be used to interpret \(\varepsilon x A(x)\) in (*). One canfurther fix the meaning of the epsilon term with the axiom\[ \varepsilon x A(x) \ne 0 \rightarrow A(\varepsilon x A(x)) \] which requires that if there is no witness to \(A\), theepsilon term return 0. For the discussion below, however, it is mostconvenient to focus on (*) alone.

Suppose we wish to show that the system above is consistent; in otherwords, we wish to show that there is no proof of the formula \(0 =1\). By pushing all substitutions to the axioms and replacing freevariables by the constant 0, it suffices to show that there is nopropositional proof of \(0 = 1\) from a finite set of closed instancesof the axioms. For that, it suffices to show that, given any finiteset of closed instances of axioms, one can assign numerical values toterms in such a way that all the axioms are true under theinterpretation. Since the arithmetical operations \(+\) and \(\times\)can be interpreted in the usual way, the only difficulty lies infinding appropriate values to assign to the epsilon terms.

Hilbert’sepsilon substitution method can be described,roughly, as follows:

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

A finitary consistency proof is obtained once it is shown in afinitarily acceptable manner that this process of successive“repairs” terminates. If it does, all critical formulasare true formulas without epsilon-terms.

This basic idea (the “Hilbertsche Ansatz”) was set outfirst by Hilbert in his 1922 talk (1923), and elaborated in lecturesin 1922–23. The examples given there, however, only deal withproofs in which all instances of the transfinite axiom correspond to asingle epsilon term \(\varepsilon x A(x)\). The challenge was toextend the approach to more than one epsilon term, to nested epsilonterms, and ultimately to second-order epsilons (in order to obtain aconsistency proof not just of arithmetic, but of analysis).

The difficulty in dealing with nested epsilon terms can be describedas follows. Suppose one of the axioms in the proof is the transfiniteaxiom \[ B(y) \rightarrow B(\varepsilon y B(y)) \] \(\varepsilon y B(y)\) may, of course, occur inother formulae in the proof, in particular in other transfiniteaxioms, e.g., \[ A(x, \varepsilon y B(y)) \rightarrow A(\varepsilon x A(x, \varepsilon y B(y)), \varepsilon y B(y)) \] So first, it seems necessary to find acorrect interpretation for \(\varepsilon y B(y)\) before we attempt tofind one for \(\varepsilon x A(x, \varepsilon y B(y))\). However,there are more complicated patterns in which epsilon terms may occurin a proof. An instance of the axiom, which plays a role indetermining the correct interpretation for \(\varepsilon y B(y)\)might be \[ B(\varepsilon x A(x, \varepsilon y B(y))) \rightarrow B(\varepsilon y B(y)) \] If \(B\)(0) is false, then in the first round ofthe procedure \(\varepsilon y B(y)\) will be interpreted by 0. Asubsequent change of the interpretation of \(\varepsilon x A(x, 0)\)from 0 to, say, \(n\), will result in an interpretation of thisinstance as \(B(n) \rightarrow B\)(0) which will be false if \(B(n)\)is true. So the interpretation of \(\varepsilon y B(y)\) will have tobe corrected to \(n\), which, in turn, might result in theinterpretation of \(\varepsilon x A(x, \varepsilon y B(y))\) to nolonger be a true formula.

This is just a sketch of the difficulties involved in extendingHilbert’s idea to the general case. Ackermann (1924) providedsuch a generalization using a procedure which “backtracks”whenever a new interpretation at a given stage results in the need tocorrect an interpretation already found at a previous stage.

Ackermann’s procedure applied to a system of second-orderarithmetic, in which, however, second order terms were restricted soas to exclude cross-binding of second-order epsilons. This amounts,roughly, to a restriction to arithmetic comprehension as theset-forming principle available (see the discussion at the end of thissection). Further difficulties with second-order epsilon termssurfaced, and it quickly became apparent that the proof as it stoodwas fallacious. However, no one in Hilbert’s school realized theextent of the difficulty until 1930, when Gödel announced hisincompleteness results. Until then, it was believed that the proof (atleast with some modifications introduced by Ackermann, some of whichinvolved ideas from von Neumann’s (1927) version of the epsilonsubstitution method) would go through at least for the first-orderpart. Hilbert and Bernays (1939) suggest that the methods used onlyprovides a consistency proof for first-order arithmetic with openinduction. In 1936, Gerhard Gentzen succeeded in giving a proof of theconsistency of first-order arithmetic in a formulation based onpredicate logic without the epsilon symbol. This proof usestransfinite induction up to \(\varepsilon_0\). Ackermann (1940) waslater able to adapt Gentzen’s ideas to give a correctconsistency proof of first-order arithmetic using theepsilon-substitution method.

Even though Ackermann’s attempts at a consistency proof forsecond-order arithmetic were unsuccessful, they provided a clearerunderstanding of the use of second-order epsilon terms in theformalization of mathematics. Ackermann used second-order epsilonterms \(\varepsilon f\ A(f)\), where \(f\) is a function variable. Inanalogy with the first-order case, \(\varepsilon f\ A(f)\) is afunction for which \(A(f)\) is true, e.g., \(\varepsilon f (x + f(x) =2x)\) is the identity function \(f(x) = x\). Again in analogy with thefirst-order case, one can use second-order epsilons to interpretsecond-order quantifiers. In particular, for any second-order formula\(A(x)\) one can find a term \(t(x)\) such that \[ A(x) \leftrightarrow t(x) = 1 \] isderivable in the calculus (the formula \(A\) may have other freevariables, in which case these appear in the term \(t\) as well). Onecan then use this fact to interpretcomprehension principles.In a language with function symbols, these take the form \[ \exists f \forall x (A(x) \leftrightarrow f(x) = 1) \]for an arbitrary formula \(A(x)\). Comprehension is more commonlyexpressed in terms of set variables, in which case it takes the form\[ \exists Y \forall x (A(x) \leftrightarrow x \in Y), \] asserting that every second order formula, withparameters, defines a set.

Analysis, orsecond-order arithmetic, is the extension of first-orderarithmetic with the comprehension schema for arbitrary second-orderformulae. The theory isimpredicative in that it allows oneto define sets of natural numbers using quantifiers that range overthe entire universe of sets, including, implicitly, the set beingdefined. One can obtainpredicative fragments of this theoryby restricting the type of formulae allowed in the comprehensionaxiom. For example, the restriction discussed in connection withAckermann above corresponds to thearithmetic comprehensionschema, in which formulae do not involve second-orderquantifiers. There are various ways of obtaining stronger fragments ofanalysis that are nonetheless predicatively justified. For example,one obtainsramified analysis by associating an ordinal rankto set variables; roughly, in the definition of a set of a given rank,quantifiers range only over sets of lower rank, i.e., those whosedefinitions are logically prior.

Further Reading. Hilbert’s and Ackermann’s earlyproofs are discussed in Zach 2003; 2004. Von Neumann’s proof isthe topic of Bellotti 2016. Ackermann’s 1940 proof is discussedin Hilbert & Bernays 1970, and Wang 1963. A modern presentation isgiven by Moser 2006. An early application of epsilon substitution isthe no-counterexample interpretation (Kreisel 1951).

6. More Recent Developments

In this section we discuss the development of the epsilon-substitutionmethod for obtaining consistency results for strong systems; theseresults are of a mathematical nature. We cannot, unfortunately,discuss the details of the proofs here but would like to indicate thatthe epsilon-substitution method did not die with Hilbert’sprogram, and that a significant amount of current research is carriedout in epsilon-formalisms.

Gentzen’s consistency proofs for arithmetic launched a field of research known asordinal analysis, andthe program of measuring the strength of mathematical theories usingordinal notations is still pursued today. This is particularlyrelevant to theextended Hilbert’s program, where thegoal is to justify classical mathematics relative to constructive, orquasi-constructive, systems. Gentzen’s methods ofcut-elimination (and extensions to infinitary logic developed by PaulLorentzen, Petr Novikov, and Kurt Schütte) have, in large part,supplanted epsilon substitution methods in these pursuits. But epsiloncalculus methods provide an alternative approach, and there is stillactive research on ways to extend Hilbert-Ackermann methods tostronger theories. The general pattern remains the same:

1. Embed the theory under investigation in an appropriate epsiloncalculus.
2. Describe a process for updating assignments to the epsilonterms.
3. Show that the procedure is normalizing, i.e., given any set ofterms, there is a sequence of updates that results in an assignmentthat 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 methodsused to prove normalization. For example, one obtains anordinalanalysis by assigning ordinal notations to steps in theprocedure, in such a way that the value of a notation decreases witheach step.

In the 1960’s, Tait (1960, 1965, 2010) extendedAckermann’s methods to obtain an ordinal analysis of extensionsof arithmetic with principles of transfinite induction. Morestreamlined and modern versions of this approach can be found in Mints2001 and Avigad 2002b. More recently, Mints, Tupailo, and Buchholzhave considered stronger, yet still predicatively justifiable,fragments of analysis, including theories of arithmetic comprehensionand a \(\Delta^{1}_1\)-comprehension rule (Mints, Tupailo &Buchholz 1996; Mints & Tupailo 1999; see also Mints 2016). Arai2002 has extended the epsilon substitution method to theories thatallow one to iterate arithmetic comprehension along primitiverecursive well orderings. In particular, his work yields ordinalanalyses for predicative fragments of analysis involving transfinitehierarchies and transfinite induction.

Some first steps have been taken in using the epsilon substitutionmethod in the analysis ofimpredicative theories (see Arai2003, 2006 and Mints 2015).

A variation on step 3 above involves showing that the normalizationprocedure is not sensitive to the choice of updates, which is to say,any sequence of updates terminates. This is calledstrongnormalization. Mints 1996 has shown that many of the proceduresconsidered have this stronger property.

In addition to the traditional, foundational branch of proof theory,today there is a good deal of interest instructural prooftheory, a branch of the subject that focuses on logical deductivecalculi and their properties. This research is closely linked withissues relevant to computer science, having to do with automateddeduction, functional programming, and computer aided verification.Here, too, Gentzen-style methods tend to dominate (see again theentry on proof theory). But the epsilon calculus can also provide valuable insights; cf. forexample Aguilera & Baaz 2019, or the discussion ofHerbrand’s theorem above.

Aside from the investigations of the epsilon calculus in proof theory,two applications should be mentioned. One is the use of epsilonnotation in Bourbaki’sTheorie des ensembles (1958).The second, of perhaps greater current interest, is the use of theepsilon-operator in the theorem-proving systemsHOL andIsabelle, where the expressive power of epsilon-terms yields significantpractical advantages.

7. 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 bea useful tool in the analysis of indefinite and definite noun phrasesin formal semantics. The epsilon notation has in fact been so used,and this application has proved useful in particular in dealing withanaphoric reference.

Consider the familiar example

1. Every farmer who owns a donkey beats it.

The generally accepted analysis of this sentence is given by theuniversal sentence

2. \(\forall x \forall y (\mathrm{Farmer}(x) \wedge\mathrm{Donkey}(y) \wedge \mathrm{Owns}(x, y)) \rightarrow\mathrm{Beats}(x, y))\)

The drawback is that “a donkey” suggest an existentialquantifier, and thus the analysis should, somehow, parallel in formthe analysis of sentence 3 given by 4:

3. Every farmer who owns a donkey is happy,
4. \(\forall x (\mathrm{Farmer}(x) \wedge \exists y(\mathrm{Donkey}(y) \wedge \mathrm{Owns}(x, y)) \rightarrow\mathrm{Happy}(x))\),

but the closest possible formalization,

5. \(\forall x ((\mathrm{Farmer}(x) \wedge \exists y(\mathrm{Donkey}(y) \wedge \mathrm{Owns}(x, y)) \rightarrow\mathrm{Beats}(x, y))\)

contains a free occurrence of \(y\). Evans 1980 suggests that sincepronouns are referring expressions, they should be analyzed asdefinite descriptions; and if the pronoun occurs in the consequent ofa conditional, the descriptive conditions are determined by theantecedent. This leads to the following E-type analysis of (1):\[ \begin{align*}& &\forall x ((\mathrm{Farmer}(x) \wedge \exists y (\mathrm{Donkey}(y) \wedge \mathrm{Owns}(x, y)) \rightarrow\\ & &(\mathrm{Beats}(x, \iota y (\mathrm{Donkey}(y) \wedge \mathrm{Owns}(x, y))) \end{align*} \] Here, \(\iota x\) is the definite description operator,so \(\iota y (\mathrm{Donkey}(y) \wedge \mathrm{Owns}(x, y))\) is“the donkey owned by \(x\);”. The trouble with this isthat on the standard analysis, the definite description carries auniqueness condition, and so (5) will be false if there is a farmerwho owns more than one donkey. A way out of this is to introduce a newoperator, whe (whoever, whatever) which works as a generalizedquantifier (Neale, 1990):

As pointed out by von Heusinger (1994), this suggests that Neale iscommitted to pronouns being ambiguous between definite descriptions\((\iota\)-expressions) and whe-expressions. Heusinger suggestsinstead to use epsilon operators indexed by choice functions (whichdepend on the context). According to this approach, the analysis of(1) is

For every choice function \(i\): \[\begin{align*}& &\forall x ((\mathrm{Farmer}(x) \wedge \mathrm{Owns}(x, \varepsilon_i y \mathrm{Donkey} (y)) \rightarrow \\ & &\mathrm{Beats} (x, \varepsilon_{a^*}y \mathrm{Donkey} (y)) \end{align*} \]

Here \(a^*\) is a choice function which depends on \(i\) and theantecedent of the conditional: If \(i\) is a choice function whichselects \(\varepsilon_i y \mathrm{Donkey}(y)\) from the set of alldonkeys, then \(\varepsilon_{a^*}y \mathrm{Donkey} (y)\) selects fromthe set of donkeys owned by \(x\).

This approach to dealing with pronouns using epsilon operators indexedby choice functions enable von Heusinger to deal with a wide varietyof circumstances (see Egli & von Heusinger 1995; von Heusinger2000).

Applications of the epsilon-operator in formal semantics, and choicefunctions in general, have received significant interest fromlinguists. Von Heusinger & Egli 2000a list, among others, thefollowing: representations of questions (Reinhart 1992), specificindefinites (Reinhart 1992; 1997; Winter 1997), E-type pronouns(Hintikka & Kulas 1985; Slater 1986; Chierchia 1992, Egli &von Heusinger 1995) and definite noun phrases (von Heusinger 1997,2004). Gratzl & Schiemer 2017 provide a comparison betweenRussell’s and Hilbert’s approaches to dealing withindefinites.

For discussion of the issues and applications of the epsilon operatorin linguistics and philosophy of language, see B. H. Slater’sarticle on epsilon calculi (cited in the Other Internet Resourcessection below), and the collections von Heusinger & Egli 2000 andvon Heusinger & Kempson 2004.

Another application of epsilon calculus is as a general logic forreasoning about arbitrary objects. Meyer Viol 1995a provides acomparison of the epsilon calculus with Fine’s 1985 theory ofarbitrary objects. Indeed, the connection is not hard to see. Giventhe equivalence \(\forall x A(x) \equiv\) A\((\varepsilon x (\negA))\), the term \(\varepsilon x (\neg A)\) is an arbitrary object inthe sense that it is an object of which \(A\) is true iff \(A\) istrue generally. The connection between \(\varepsilon\)-terms andFine’s arbitrary object theory is exploited for philosophicalpurposes by Bonatti 2022 (abstraction in mathematics), Genco et al2021 (grounding), and Sandu 2020 (indefinites).)

In his 1961, Carnap proposed to use the \(\varepsilon\)-operator toreconstruct the theoretical part of scientific theories (a proposalsimilar to Ramseyfication; see the entry ontheoretical terms in science andSupplement E to the entry on Carnap). This proposal is discussed by Schiemer & Gratzl 2016. Leitgeb2023 considers an \(\varepsilon\)-version of Ramsey sentences in thecontext of a semantics of indeterminacy.

Meyer Viol’s papers 1995a, 1995b contain further proof- andmodel-theoretic studies of the epsilon calculus; specificallyintuitionistic epsilon calculi. Here, the epsilon theorems no longerhold, i.e., introduction of epsilon terms produces non-conservativeextensions of intuitionistic logic. Other investigations of epsilonoperators in intuitionistic logic can be found in Shirai 1971, Bell1993a, 1993b, DeVidi 1995, and Baaz & Zach 2022. Forepsilon-operators in many-valued logics, see Mostowski 1963, for modalepsilon calculus, Fitting 1975.

Bibliography

• Aguilera, J.P., and M. Baaz, 2019, ‘Unsound inferences makeproofs shorter’.Journal of Symbolic Logic, 84:102–122.
• Ackermann, W., 1924, ‘Begründung des’’tertium non datur’’ mittels der HilbertschenTheorie der Widerspruchsfreiheit’,MathematischeAnnalen, 93: 1–36.
• –––, 1937–38, ‘MengentheoretischeBegründung der Logik’,Mathematische Annalen, 115:1–22.
• –––, 1940, ‘Zur Widerspruchsfreiheitder Zahlentheorie’,Mathematische Annalen, 117:162–194.
• Arai, T., 2002, ‘Epsilon substitution method for theoriesof jump hierarchies’,Archive for Mathematical Logic,2: 123–153.
• –––, 2003, ‘Epsilon substitution methodfor ID\(_1 (\Pi^{0}_1 \vee \Sigma^{0}_1)\)’,Annals of Pureand Applied Logic, 121: 163–208.
• –––, 2006, ‘Epsilon substitution methodfor \(\Pi^{0}_2\)-FIX.Journal of Symbolic Logic, 71:1155–1188
• Avigad, J., 2002a, ‘Saturated models of universaltheories’,Annals of Pure and Applied Logic, 118:219–234.
• –––, 2002b, ‘Update procedures and the1-consistency of arithmetic’,Mathematical LogicQuarterly, 48: 3–13.
• Baaz, M., A. Leitsch, and A. Lolic, 2018, ‘Asequent-calculus based formulation of the extended first epsilontheorem’, in: Artemov, S., Nerode, A. (eds.),LogicalFoundations of Computer Science, Berlin: Springer, 55–71.
• Baaz, M., and R. Zach, 2022, ‘Epsilon theorems inintermediate logics’,The Journal of Symbolic Logic,87(2): 682–720.
• Bell, J. L., 1993a. ‘Hilbert’s epsilon-operator andclassical logic’,Journal of Philosophical Logic, 22:1–18.
• –––, 1993b. ‘Hilbert’s epsilonoperator in intuitionistic type theories’,MathematicalLogic Quarterly, 39: 323–337.
• Bellotti, L., 2016, ‘Von Neumann’s consistencyproof’,Review of Symbolic Logic, 9:429–455.
• Bonatti, N., 2022, ‘A reassessment of cantorianabstraction based on the ε-operator’,Synthese, 200(5): 396.
• Bourbaki, N., 1958,Theorie des ensembles, Paris:Hermann.
• Buss, S., 1995, ‘On Herbrand’s theorem’,Logic and Computational Complexity (Lecture Notes in ComputerScience 960), Berlin: Springer, 195–209.
• ––– 1998, ‘Introduction to prooftheory’, in: Buss (ed.),The Handbook of Proof Theory,Amsterdam: North-Holland, 1–78.
• Chierchia, G., 1992, ‘Anaphora and dynamic logic’.Linguistics and Philosophy, 15: 111–183.
• Davis, M., and R. Fechter, 1991, ‘A free variable version ofthe first-order predicate calculus’,Journal of Logic andComputation, 1: 431–451.
• DeVidi, D., 1995, ‘Intuitionistic \(\varepsilon\)- and\(\tau\)-calculi’,Mathematical Logic Quarterly, 41:523–546.
• Egli, U., and K. von Heusinger, 1995, ‘The epsilon operatorand E-type pronouns’, in U. Egliet al. (eds.),Lexical Knowledge in the Organization of Language, Amsterdam:Benjamins, 121–141 (Current Issues in Linguistic Theory114).
• Evans, G., 1980, ‘Pronouns’,LinguisticInquiry, 11: 337–362.
• Ewald, W. B. (ed.), 1996,From Kant to Hilbert. A SourceBook in the Foundations of Mathematics, Vol. 2, Oxford: OxfordUniversity Press.
• Ferrari, P. L., 1987, ‘A note on a proof ofHilbert’s second \(\varepsilon\)-theorem’,Journal ofSymbolic Logic, 52: 214–215.
• Fine, K., 1985,Reasoning with Arbitrary Objects,Oxford: Blackwell.
• Fitting, M., 1975, ‘A modal logicepsilon-calculus’,Notre Dame Journal of Formal Logic,16: 1–16.
• Flannagan, T. B., 1975, ‘On an extension ofHilbert’s second \(\varepsilon\)-theorem’,Journal ofSymbolic Logic, 40: 393–397.
• Genco, F. A., F. Poggiolesi, and L. Rossi, 2021,‘Grounding, quantifiers, and paradoxes’,Journal of Philosophical Logic, 50(6): 1417–1448.
• Girard, J.-Y., 1982, ‘Herbrand’s theorem and prooftheory’,Proceedings of the Herbrand Symposium,Amsterdam: North-Holland, 29-38.
• Gratzl, N., and G. Schiemer, 2017, ‘Two types ofindefinites: Hilbert & Russell’,IfCoLog Journalof Logics and Their Applications, 4(2): 333–348.
• Herbrand, J., 1930,Recherches sur la thèorie de ladèmonstration,Dissertation, University of Paris.English translation in Herbrand 1971, pp. 44–202.
• –––, 1971,Logical Writings, W.Goldfarb (ed.), Cambridge, Mass.: Harvard University Press.
• Hilbert, D., 1922, ‘Neubegründung der Mathematik:Erste Mitteilung’,Abhandlungen aus dem Seminar derHamburgischen Universität, 1: 157–177, Englishtranslation in Mancosu, 1998, 198–214 and Ewald, 1996,1115–1134.
• –––, 1923, ‘Die logischen Grundlagender Mathematik’,Mathematische Annalen, 88:151–165; English translation in Ewald, 1996,1134–1148.
• Hilbert, D., and P. Bernays, 1934,Grundlagen derMathematik (Volume 1), Berlin: Springer.
• –––, 1939,Grundlagen derMathematik (Volume 2), Berlin: Springer.
• –––, 1970, ‘Grundlagen derMathematik’ (Volume 2), 2nd, edition, Berlin: Springer,Supplement V.
• Hintikka, J., and J. Kulas, 1985,Anaphora and DefiniteDescriptions: Two Applications of Game-Theoretical Semantics,Dordrecht: Reidel.
• Kempson, R., W. Meyer Viol, and D. Gabbay, 2001,DynamicSyntax: The Flow of Language Understanding, Oxford:Blackwell.
• Kreisel, G, 1951, ‘On the interpretation of non-finitistproofs – part I’,Journal of Symbolic Logic, 16:241–267.
• Leisenring, A. C., 1969,Mathematical Logic andHilbert’s Epsilon-Symbol, London: Macdonald.
• Leitgeb, H., 2023, ‘Ramsification and semanticindeterminacy’,The Review of Symbolic Logic,16(3): 900–950.
• Luckhardt, H., 1989, ‘Herbrand-Analysen zweier Beweisedes Satzes von Roth: Polynomiale Anzahlschranken’,Journalof Symbolic Logic, 54: 234–263.
• Maehara, S., 1955, ‘The predicate calculus with\(\varepsilon\)-symbol’,Journal of the Mathematical Societyof Japan, 7: 323–344.
• –––, 1957, ‘Equality axiom onHilbert’s \(\varepsilon\)-symbol’,Journal of theFaculty of Science, University of Tokyo, Section 1, 7:419–435.
• Mancosu, P. (ed.), 1998,From Brouwer to Hilbert. TheDebate on the Foundations of Mathematics in the 1920s, Oxford:Oxford University Press.
• Meyer Viol, W. P. M., 1995a,Instantial Logic. AnInvestigation into Reasoning with Instances, Ph.D. thesis,University of Utrecht. ILLC Dissertation Series1995–11.
• –––, 1995b. ‘A proof-theoretictreatment of assignments’,Bulletin of the IGPL, 3:223–243.
• Mints, G., 1994, ‘Gentzen-type systems andHilbert’s epsilon substitution method. I’,Logic,Methodology and Philosophy of Science, IX (Uppsala, 1991),Amsterdam: North-Holland, 91-122.
• –––, 1996, ‘Strong termination for theepsilon substitution method’,Journal of SymbolicLogic, 61: 1193–1205.
• –––, 2001, ‘The epsilon substitutionmethod and continuity’, in W. Sieget al. (eds.),Reflections on the Foundations of Mathematics: Essays in Honor ofSolomon Feferman, Lecture Notes in Logic 15, Association forSymbolic Logic.
• –––, 2008, ‘Cut Elimination for asimple formulation of epsilon calculus’,Annals of Pure andApplied Logic,152 (1–3): 148–160.
• –––, 2013, ‘Epsilon substitution forfirst- and second-order predicate logic’,Annals of Pure andApplied Logic, 164: 733–739.
• –––, 2015, ‘Non-deterministic epsilonsubstitution method for PA and ID\(_1\)’, in: Kahle, R.,Rathjen, M. (Eds.),Gentzen’s Centenary: The Quest forConsistency, Berlin: Springer, pp. 479–500.
• Mints, G., and S. Tupailo, 1999, ‘Epsilon-substitutionmethod for the ramified language and \(\Delta^{1}_1\)-comprehensionrule’, in A. Cantiniet al. (eds.),Logic andFoundations of Mathematics (Florence, 1995), Dordrecht: Kluwer,107–130.
• Mints, G., S. Tupailo, and W. Buchholz, 1996, ‘Epsilonsubstitution method for elementary analysis’,Archive forMathematical Logic, 35: 103–130.
• Miyamoto, K., and G. Moser, 2024, ‘Herbrand complexity andthe epsilon calculus with equality’,Archive forMathematical Logic, 63(1): 89–118.
• Moser, G., 2006, ‘Ackermann’s substitution method(remixed)’,Annals of Pure and Applied Logic,142(1–3): 1–18.
• Moser, G., and R. Zach, 2006, ‘The epsilon calculus andHerbrand complexity’,Studia Logica, 82(1):133–155.
• Mostowski, A., 1963, ‘The Hilbert epsilon function inmany-valued logics’,Acta Philosophica Fennica, 16:169–188.
• Neale, S., 1990,Descriptions, Cambridge, MA: MITPress.
• Reinhart, T., 1992, ‘Wh-in-situ: An apparentparadox’, in P. Dekker and M. Stokhof (eds.).Proceedingsof the Eighth Amsterdam Colloquium, December 17–20, 1991,ILLC, University of Amsterdam, 483–491.
• –––, 1997, ‘Quantifier scope: How laboris divided between QR and choice functions’.Linguistics andPhilosophy, 20: 335–397.
• Sandu, G., 2020, ‘Indefinites, Skolem functions, andarbitrary objects’, in M. Dumitru (ed.),Metaphysics, Meaning, and Modality: Themes from Kit Fine,Oxford: Oxford University Press, 98–112.
• Schiemer, G., and N. Gratzl, 2016, ‘Theepsilon-reconstruction of theories and scientificstructuralism’,Erkenntnis, 81(2): 407–432.
• Shirai, K., 1971, ‘Intuitionistic predicate calculus with\(\varepsilon\)-symbol’,Annals of the Japan Association forPhilosophy of Science, 4: 49–67.
• Sieg, W., 1991, ‘Herbrand analyses’,Archivefor Mathematical Logic, 30: 409–441.
• Slater, B. H., 1986, ‘E-type pronouns and\(\varepsilon\)-terms’,Canadian Journal of Philosophy,16: 27–38.
• –––, 1988, ‘Hilbertianreference’,Noûs, 22: 283–97.
• –––, 1994, ‘The epsilon calculus’problematic’,Philosophical Papers, 23:217–42.
• –––, 2000,‘Quantifier/variable-binding’,Linguistics andPhilosophy, 23: 309–21.
• Tait, W. W., 1960, ‘The substitution method.’Journal of Symbolic Logic, 30: 175–192.
• –––, 1965, ‘Functionals defined bytransfinite recursion,’Journal of Symbolic Logic, 30:155–174.
• –––, 2010, ‘The substitution methodrevisited.’ in: S. Feferman and W. Sieg (eds.),Proofs,Categories and Computations: Essays in Honor of Grigori Mints,London: College Publications, pp. 131–14.
• von Heusinger, K., 1994, Review of Neale (1990).Linguistics, 32: 378–385.
• –––, 1997, ‘Definite descriptions andchoice functions’, in S. Akama (ed.).Logic, Language andComputation, Dordrecht: Kluwer, 61–91.
• –––, 2000, ‘The Reference ofIndefinites’, in von Heusinger and Egli, (2000),265–284.
• –––, 2004, ‘Choice functions and theanaphoric semantics of definite NPs’,Research in Languageand Computation, 2: 309–329.
• von Heusinger, K., and U. Egli (eds.), 2000,Reference andAnaphoric Relations, Dordrecht: Kluwer.
• –––, 2000a. ‘Introduction: Referenceand the Semantics of Anaphora’, in von Heusinger and Egli(2000), 1–13.
• von Heusinger, K., and R. Kempson (eds.), 2004,ChoiceFunctions in Semantics, Special Issue ofResearch on Languageand Computation, 2(3).
• von Neumann, J., 1927, ‘Zur HilbertschenBeweistheorie’,Mathematische Zeitschrift, 26:1–46.
• Wang, H., 1963,A Survey of Mathematical Logic,Peking: Science Press.
• Winter, Y., 1997, ‘Choice functions and the scopalsemantics of indefinites’.Linguistics and Philosophy,20: 399–467.
• Yasuhara, M., 1982, ‘Cut elimination in\(\varepsilon\)-calculi’,Zeitschrift für mathematischeLogik und Grundlagen der Mathematik, 28: 311–316.
• Zach, R., 2003, ‘The practice of finitism. Epsiloncalculus and consistency proofs in Hilbert’s Program’,Synthese, 137: 211–259.
• –––, 2004, ‘Hilbert’s“Verunglückter Beweis”, the first epsilontheorem, and consistency proofs’.History and Philosophy ofLogic, 25: 79–94.
• –––, 2017, ‘Semantics and proof theoryof the epsilon calculus’, in: Ghosh, S., Prasad, S. (Eds.),Logic and Its Applications. ICLA 2017, LNCS. Springer,Berlin, Heidelberg, pp. 27–47.

Academic Tools

	How to cite this entry.
	Preview the PDF version of this entry at theFriends of the SEP Society.
	Look up topics and thinkers related to this entry at the Internet Philosophy Ontology Project (InPhO).
	Enhanced bibliography for this entryatPhilPapers, 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 |theoretical terms in science