The Epsilon Calculus (Stanford Encyclopedia of Philosophy) Cite this entry Search the SEP • Advanced Search • Tools • RSS FeedTable of Contents• What's New• Archives• Projected ContentsEditorial Information• About the SEP• Editorial Board• How to Cite the SEP• Special CharactersSupport the SEPContact the SEP ©Metaphysics Research Lab,CSLI,Stanford University  Open access to the SEP is made possible by a world-wide funding initiative. Please Read How You Can Help Keep the Encyclopedia FreeThe Epsilon CalculusFirst published Fri May 3, 2002; substantive revision Mon Jul 2, 2007The epsilon calculus is a logical formalism developed by DavidHilbert in the service of his program in the foundations ofmathematics. The epsilon operator is a term-forming operator whichreplaces quantifiers in ordinary predicate logic. Specifically, in thecalculus, a term εx A denotes some xsatisfying A(x), if there is one. In Hilbert'sProgram, the epsilon terms play the role of ideal elements; the aim ofHilbert's finitistic consistency proofs is to give a procedure whichremoves such terms from a formal proof. The procedures by which this isto be carried out are based on Hilbert's epsilon substitution method.The epsilon calculus, however, has applications in other contexts aswell. The first general application of the epsilon calculus was inHilbert's epsilon theorems, which in turn provide the basis for thefirst correct proof of Herbrand's theorem. More recently, variants ofthe epsilon operator have been applied in linguistics and linguisticphilosophy to deal with anaphoric pronouns.OverviewThe Epsilon CalculusThe Epsilon TheoremsHerbrand's TheoremThe Epsilon Substitution Method and ArithmeticMore Recent DevelopmentsEpsilon Operators in Linguistics, Philosophy, and Non-classical LogicsBibliographyOther Internet ResourcesRelated EntriesOverviewBy 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, andincluded an interest in the foundations of mathematics: hisFoundations of Geometry was published in 1899, and of the listof questions posed to the International Congress of Mathematicians in1900, three addressed distinctly foundational issues.Following the publication of Russell's paradox, Hilbert presented anaddress to the Third International Congress of Mathematicians in 1904,where, for the first time, he sketched his plan to provide a rigorousfoundation for mathematics via syntactic consistency proofs. But he didnot return to the subject in earnest until 1917, when he began a seriesof lectures on the foundations of mathematics with the assistance ofPaul Bernays. Although Hilbert was impressed by the work of Russell andWhitehead in their Principia Mathematica, he became convincedthat the logicist attempt to reduce mathematics to logic could notsucceed, due in particular to the non-logical character of their axiomof reducibility. At the same time, he judged the intuitionisticrejection of the law of the excluded middle as unacceptable tomathematics. Therefore, in order to counter concerns raised by thediscovery of the logical and set-theoretic paradoxes, a new approachwas 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 formaldeductive systems. Second, these formal systems were to be provedsyntactically consistent, not by exhibiting a model or reducing theirconsistency to another system, but by a direct metamathematicalargument of an explicit, "finitary" character. The epsilon calculus wasto provide the first component of this program, while his epsilonsubstitution method was to provide the second.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 the existentialquantifier. The extension is conservative in the sense that it does notadd any new first-order consequences. But, conversely, quantifiers canbe defined in terms of the epsilons, so first-order logic can beunderstood in terms of quantifier-free reasoning involving the epsilonoperation. It is this latter feature that makes the calculus convenientfor the purpose of proving consistency. Suitable extensions of theepsilon calculus make it possible to embed stronger, quantificationaltheories of numbers and sets in quantifier-free calculi. Hilbertexpected that it would be possible to demonstrate the consistency ofsuch extensions.The Epsilon CalculusIn his Hamburg lecture in 1921 (1922), Hilbert first presented theidea of using choice functions to deal with the principle of theexcluded middle in a formal system for arithmetic. These ideas weredeveloped into the epsilon calculus and the epsilon substitution methodin a series of lecture courses between 1921 and 1923, and in Hilbert's(1923). The final presentation of the epsilon-calculus can be found inWilhelm Ackermann's dissertation (1924).This section will describe a version of the calculus correspondingto first-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 s1, …, sk areterms and F is a k-ary function symbol of L,F(s1, …, sk) isa term.If s1, …, sk areterms and R is a k-ary relation symbol of L,R(s1, …, sk) isa formula.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 definedin the usual way; in particular, the variable x becomes boundin the term εx A. The intended interpretation is thatεx A denotes some x satisfyingA, if there is one. Thus, the epsilon terms are governed bythe following axiom (Hilbert's "transfinite axiom"):A(x) → A(εx A)In addition, the epsilon calculus includes a complete set of axiomsgoverning the classical propositional connectives, and axioms governingthe equality symbol. The only rules of the calculus are thefollowing:Modus ponensSubstitution: from A(x), concludeA(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 falsifyingA(x). The version above was used in Ackermann'sdissertation, and has become standard.Note that the calculus just described is quantifier-free.Quantifiers can be defined as follows:∃x A(x) ≡ A(εxA)∀x A(x) ≡ A(εx(¬A))The usual quantifier axioms and rules can be derived from these, sothe definitions above serve to embed first-order logic in the epsiloncalculus. The converse is, however, not true: not every formula in theepsilon calculus is the image of an ordinary quantified formula underthis embedding. Hence, the epsilon calculus is more expressive than thepredicate calculus, simply because epsilon term can be combined in morecomplex ways than quantifiers.It is worth noting that epsilon terms are nondeterministic, therebyrepresenting a form of the axiom of choice. For example, in a languagewith constant symbols a and b, εx(x = a ∨ x= b) is either a or b, but the calculusleaves it entirely open as to which is the case. One can add to thecalculus a schema of extensionality,∀x(A(x) ↔ B(x)) →εx A = εx Bwhich asserts that the epsilon operator assigns the same witness toequivalent formulae A and B. For many applications,however, this additional schema is not necessary.The Epsilon TheoremsThe 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 Γ ∪{A} is a set of quantifier-free formulae not involving theepsilon symbol. If A is derivable from Γ in the epsiloncalculus, then A is derivable from Γ in quantifier-freepredicate logic.Second epsilon theorem: Suppose Γ ∪{A} is a set of formulae not involving the epsilon symbol. IfA is derivable from Γ in the epsilon calculus, thenA is derivable from Γ in predicate logic.In the first epsilon theorem, "quantifier-free predicate logic" isintended to include the substitution rule above, so quantifier-freeaxioms behave like their universal closures. Since the epsilon calculusincludes first-order logic, the first epsilon theorem implies that anydetour through first-order predicate logic used to derive aquantifier-free theorem from quantifier-free axioms can ultimately beavoided. The second epsilon theorem shows that any detour through theepsilon calculus used to derive a theorem in the language of thepredicate calculus from axioms in the language of the predicatecalculus can also be avoided.More generally, the first epsilon theorem establishes thatquantifiers and epsilons can always be eliminated from a proof of aquantifier-free formula from other quantifier-free formulae. This is ofparticular importance for Hilbert's program, since the epsilons playthe role of ideal elements in mathematics. If quantifier-free formulaecorrespond to the "real" part of the mathematical theory, the firstepsilon-theorem shows that ideal elements can be eliminated from proofsof real statements, provided the 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 resultsfrom the 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 strongsense that every derivable quantifier- and epsilon-free formula istrue. Hilbert and Bernays use this theorem to give a finitisticconsistency proof 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., epsilons.Herbrand's TheoremHilbert 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 is Herbrand'stheorem . This is often formulated as the statement that if anexistential formula∃x1 …∃xkA(x1,…,xk)is derivable in first-order predicate logic (without equality),where A is quantifier-free, then there are sequences of termst11, …,tk1, …,t1n, …,tkn, such thatA(t11,…,tk1) ∨ … ∨ A(t1n, …,tkn)is a tautology. If one is dealing with first-order logicwith equality, one has to replace "tautology" by "tautologicalconsequence of substitution instances of the equality axioms";following Shoenfield we will use the term "quasi-tautology" to describesuch a formula.The version of Herbrand's theorem just described follows immediatelyfrom the Extended First Epsilon Theorem of Hilbert andBernays. Using methods associated with the proof of the second epsilontheorem, however, Hilbert and Bernays derived a stronger result that,like Herbrand's original formulation, provides more information. Tounderstand the two parts of the theorem below, it helps to consider aparticular example. Let A be the formula∃x1 ∀x2∃x3 ∀x4B(x1, x2 ,x3, x4)where B is quantifier-free. The negation of A isequivalent to∀x1 ∃x2∀x3 ∃x4¬B(x1, x2,x 3, x4).By Skolemizing, i.e., using function symbols to witness theexistential quantifiers, we obtain∃f2, f4∀x1, x3¬B(x1,f2(x1), x3,f4(x1,x3)).Taking the negation of this, we see that the original formula is"equivalent" to∀f2, f4∃x1, x3B(x1,f2(x1), x3,f4(x1,x3)).The first clause of the theorem below, in this particular instance,says that the formula A above is derivable in first-orderlogic if and only if there is a sequence of termst11, t31,…, t1n,t3n in the expanded languagewith f2 and f4 such thatB(t11, f2(t11),t3 1,f4(t11, t31)) ∨ … ∨ B(t1n,f2(t1n),t3n,f2(t1n,t3n))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-orderlogic if and only if there are sequences of variablesx21 ,x41,…,x2n ,x4n and termss11,s31,…,s1n,s3n in the originallanguage such thatB(s11,x21, s31,x41) ∨ … ∨ B(s1n,x2n,s3n,x4n)is a quasi-tautology, and such that A is derivable fromthis formula using only the quantifier and idempotency rules describedbelow.More generally, suppose A is any prenex formula, of theformQ1x1 …QnxnB(x1, …, xn),where B is quantifier-free. Then B is said to bethe matrix of A, and an instance of B isobtained by substituting terms in the language of B for someof its variables. The Herbrand normal formAH of A is obtained bydeleting each universal quantifier, andreplacing each universally quantified variablexi byfi(xi1, …,xik(i)), wherexi1, …,xik(i) are the variables correspondingto the existential quantifiers precedingQi in A (in order), andfi is a new function symbol designated for thisrole.When we refer to an instance of the matrix ofAH, we mean a formula that is obtained bysubstituting terms in the expanded language in the matrix ofAH. We can now state Hilbert and Bernays'sformulation ofHerbrand's theorem. (1) A prenex formula Ais derivable in the predicate calculus if and only if there is adisjunction of instances of the matrix of AH whichis a quasi-tautology.(2) A prenex formula A is derivable in the predicatecalculus if and only if there is a disjunction  jBj of instances of the matrix ofA, such that j Bj isa quasi-tautology, and A is derivable from jBj using the following rules:from C1 ∨ … ∨ Ci(t) ∨ … ∨ Cm conclude C1 ∨ … ∨ ∃x Ci(x) ∨ … ∨ Cm andfrom C1 ∨ … ∨ Ci(x) ∨ … ∨ Cm conclude C1 ∨ … ∨ ∀xCi(x) ∨ … ∨ Cm (if x not inCj for j ≠ i),as well as the idempotence of ∨ (fromC ∨ C ∨ Dconclude C ∨ D).Herbrand's theorem can also be obtained by using cut elimination,via Gentzen's "midsequent theorem." However, the proof using the secondepsilon theorem has the distinction of being the first complete andcorrect proof of Herbrand's theorem. Moreover, and this is seldomrecognized, whereas the proof based on cut-elimination provides a boundon the length of the Herbrand disjunction only as a function of the cutrank and complexity of the cut formulas in the proof, the lengthobtained from the proof based on the epsilon calculus provides a boundas a function of the number of applications of the transfinite axiom,and the rank and degree of the epsilon-terms occurring therein. Inother words, 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 of thissection is essentially the special case of (2) in which the formulaA 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 AH is.The forward direction of this equivalence is much easier to prove; infact, for any formula A, A →AH is derivable in predicate logic. Proving thereverse direction involves eliminating the additional function symbolsin AH, and is much more difficult, especially inthe presence of equality. It is here that epsilon methods play acentral role.Given a prenex formula, the Skolem normal formAS is defined dually to AH,i.e., by replacing existentially quantified variables by witnessingfunctions. If Γ is a set of prenex sentences, letΓS denote the set of their Skolem normal forms. Usingthe deduction theorem and Herbrand's theorem, it is not hard to showthat the following are pairwise equivalent:Γ proves AΓ proves AHΓS proves AΓS proves AHThe Epsilon Substitution Method and ArithmeticAs noted above, historically, the primary interest in the epsiloncalculus was as a means to obtaining consistency proofs. Hilbert'slectures from 1917-1918 already note that one can easily prove theconsistency of propositional logic, by taking propositional variablesand formulae to range over truth values 0 and 1, and interpreting thelogical connectives as the corresponding arithmetic operations.Similarly, one can prove the consistency of predicate logic (or thepure epsilon calculus), by specializing to interpretations where theuniverse of discourse has a single element. These considerationssuggest the following more general program for proving 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 for0, 1, +, ×, <. Along with quantifier-free axioms defining thebasic symbols, one can specify that the epsilon terms ε xA(x) picks out the least value satisfying A , ifthere is one, with the following axiom:(*) A(x) → A(εxA(x)) εxA(x) ≤ xThe result is a system that is strong enough to interpretfirst-order (Peano) arithmetic. Alternatively, one can take the epsilonsymbol to satisfy the following axiom:A(y) → A(εxA(x)) εxA(x) ≠ y + 1.In other words, if there is any witness y satisfyingA(y), the epsilon term returns a value whosepredecessor does not have the same property. Clearly the epsilon termdescribed by (*) satisfies the alternative axiom; conversely, one cancheck that given A, a value of εx(∃z ≤ x A(x)) satisfying thealternative axiom can be used to interpret εxA(x) in (*). One can further fix the meaning of theepsilon term with the axiomεx A(x) ≠ 0 →A(ε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; inother words, 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 instances ofthe axioms. For that, it suffices to show that, given any finite set ofclosed instances of axioms, one can assign numerical values to terms insuch a way that all the axioms are true under the interpretation. Sincethe arithmetical operations + and × can be interpreted in theusual way, the only difficulty lies in finding appropriate values toassign 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 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 thatA(t) is true in the interpretation, but eitherA(εx A(x)) is false or the value oft is smaller than the value of εxA(x)."Repair" the assignment by assigning to εxA(x) the value of t, and repeat theprocess.A finitistic consistency proof is obtained once it is shown in afinitistically acceptable manner that this process of successive"repairs" terminates. If it does, all critical formulas are trueformulas without epsilon-terms.This basic idea (the "Hilbertsche Ansatz") was set out first byHilbert in his 1922 talk (1923), and elaborated in lectures in 1922-23.The examples given there, however, only deal with proofs in which allinstances of the transfinite axiom correspond to a single epsilon termεx A(x). The challenge was to extend theapproach to more than one epsilon term, to nested epsilon terms, andultimately to second-order epsilons (in order to obtain a consistencyproof 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 transfiniteaxiomB(y) → B(εyB(y))εy B(y) may, of course, occur in otherformulae in the proof, in particular in other transfinite axioms,e.g.,A(x, εy B(y)) →A(εx A(x, εyB(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 mayoccur in a proof. An instance of the axiom, which plays a role indetermining the correct interpretation for εyB(y) might beB(εx A(x, εyB(y))) → B(εyB(y))If B(0) is false, then in the first round of the procedureεy B(y) will be interpreted by 0. Asubsequent change of the interpretation of εxA(x, 0) from 0 to, say, n, will result in aninterpretation of this instance as B(n) →B(0) which will be false if B(n) is true. Sothe interpretation of εy B(y) will have to becorrected to n, which, in turn, might result in theinterpretation of εx A(x, εyB(y)) to no longer be a true formula.This is just a sketch of the difficulties involved in extendingHilbert's idea to the general case. Ackermann (1924) provided such ageneralization using a procedure which "backtracks" whenever a newinterpretation at a given stage results in the need to correct aninterpretation already found at a previous stage.Ackermann's procedure applied to a system of second-orderarithmetic, in which, however, second order terms were restricted so asto 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 stood wasfallacious. However, no one in Hilbert's school realized the extent ofthe difficulty until 1930, when Gödel announced his incompletenessresults. Until then, it was believed that the proof (at least with somemodifications introduced by Ackermann, some of which involved ideasfrom 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 prooffor first-order arithmetic with open induction. In 1936, GerhardGentzen succeeded in giving a proof of the consistency of first-orderarithmetic in a formulation based on predicate logic without theepsilon symbol. This proof uses transfinite induction up toε0. Ackermann (1940) was later able to adaptGentzen's ideas to give a correct consistency proof of first-orderarithmetic using the epsilon-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 epsilon termsεf A(f), where f is a functionvariable. In analogy with the first-order case, εfA(f) is a function for which A(f) istrue, e.g., εf (x + f(x) =2x) is the identity function f(x) =x . Again in analogy with the first-order case, one can usesecond-order epsilons to interpret second-order quantifiers. Inparticular, for any second-order formula A(x) one canfind a term t(x) such thatA(x) ↔ t(x) =1is derivable in the calculus (the formula A may have otherfree variables, in which case these appear in the term t aswell). One can then use this fact to interpret comprehensionprinciples. In a language with function symbols, these take theform∃f ∀x(A(x) ↔ f(x) = 1)for an arbitrary formula A(x). Comprehension ismore commonly expressed in terms of set variables, in which case ittakes the form∃Y ∀x(A(x) ↔ x ∈Y),asserting that every second order formula, with parameters, definesa set.Analysis, or second-order arithmetic, is theextension of first-order arithmetic with the comprehension schema forarbitrary second-order formulae. The theory is impredicativein that it allows one to define sets of natural numbers usingquantifiers that range over the entire universe of sets, including,implicitly, the set being defined. One can obtain predicativefragments of this theory by restricting the type of formulae allowed inthe comprehension axiom. For example, the restriction discussed inconnection with Ackermann above corresponds to the arithmeticcomprehension schema, in which formulae do not involvesecond-order quantifiers. There are various ways of obtaining strongerfragments of analysis that are nonetheless predicatively justified. Forexample, one obtains ramified analysis by associating anordinal rank to set variables; roughly, in the definition of a set of agiven rank, quantifiers range only over sets of lower rank, i.e., thosewhose definitions are logically prior.More Recent DevelopmentsIn this section we discuss the development of theepsilon-substitution method for obtaining consistency results forstrong systems; these results are of a mathematical nature. We cannot,unfortunately, discuss the details of the proofs here but would like toindicate that the epsilon-substitution method did not die withHilbert's program, and that a significant amount of current research iscarried out in epsilon-formalisms.Gentzen's consistency proofs for arithmetic launched a field ofresearch known as ordinal analysis, and the program ofmeasuring the strength of mathematical theories using ordinal notationsis still pursued today. This is particularly relevant to theextended Hilbert's program, where the goal is to justifyclassical mathematics relative to constructive, or quasi-constructive,systems. Gentzen's methods of cut-elimination (and extensions toinfinitary logic developed by Paul Lorentzen, Petr Novikov, and KurtSchütte) have, in large part, supplanted epsilon substitutionmethods in these pursuits. But epsilon calculus methods provide analternative approach, and there is still active research on ways toextend Hilbert-Ackermann methods to stronger theories. The generalpattern remains the same:Embed the theory under investigation in an appropriate epsiloncalculus.Describe a process for updating assignments to the epsilonterms.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 originaltheory, from a foundational point of view one is interested in themethods used to prove normalization. For example, one obtains anordinal analysis by assigning ordinal notations to steps inthe procedure, in such a way that the value of a notation decreaseswith each step.In the 1960's, William Tait extended Ackermann's methods to obtainan ordinal analysis of extensions of arithmetic with principles oftransfinite induction. More recently, Grigori Mints, Sergei Tupailo,and Wilfried Buchholz have considered stronger, yet still predicativelyjustifiable, fragments of analysis, including theories of arithmeticcomprehension and a Δ11-comprehensionrule. Toshiyasu Arai has extended the epsilon substitution method totheories that allow one to iterate arithmetic comprehension alongprimitive recursive well orderings. In particular, his work yieldsordinal analyses for predicative fragments of analysis involvingtransfinite hierarchies and transfinite induction.Some first steps have been taken by Arai and Mintsin using the epsilon substitution method in the analysis ofimpredicative theories. See the annotated bibliographybelow.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 calledstrong normalization. Mints has shown that many ofthe 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 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, e.g.,Troelstra-Schwichtenberg (2000)). But the epsilon calculus can alsoprovide valuable insights; cf. for example Mints (2002) or thediscussion of Herbrand's theorem above.Aside from the investigations of the epsilon calculus in prooftheory, two applications should be mentioned. One is the use of epsilonnotation in Bourbaki's Theorie des ensembles (1958). Thesecond, of perhaps greater current interest, is the use of theepsilon-operator in the theorem-proving systems HOLand Isabelle, where the expressive power ofepsilon-terms yields significant practical advantages.Epsilon Operators in Linguistics, Philosophy, and Non-classical LogicsReading the epsilon operator as an indefinite choice operator ("an xsuch that A(x)") suggests that it might be a useful tool in theanalysis of indefinite and definite noun phrases in formal semantics.The epsilon notation has in fact been so used, and this application hasproved useful in particular in dealing with anaphoric reference.Consider the familiar exampleEvery farmer who owns a donkey beats it.The generally accepted analysis of this sentence is given by theuniversal 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 ofsentence 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 sincepronouns are referring expressions, they should be analyzed as definitedescriptions; and if the pronoun occurs in the consequent of aconditional, the descriptive conditions are determined by theantecedent. 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 troublewith this is that on the standard analysis, the definite descriptioncarries a uniqueness condition, and so (5) will be false if there is afarmer who owns more than one donkey. A way out of this is to introducea new operator, whe (whoever, whatever) which works as a generalizingquantor (Neale, 1991):∀x ((Farmer(x) ∃y(Donkey(y) Owns(x, y)) →Beats(x, whe y (Donkey(y) Owns(x,y)))As pointed out by von Heusinger (1994), this suggests that Neale iscommitted to pronouns being ambiguous between definite descriptions(ι-expressions) and whe-expressions. Heusinger suggests instead touse epsilon operators indexed by choice functions (which depend on thecontext). According to this approach, the analysis of (1) isFor every choice function i: ∀x (Farmer(x) Owns(x,εiy Donkey (y))→ Beats (x, εa*y Donkey (y))a* is a choice function which depends on i and theantecedent of the conditional: If i is a choice function whichselects εiy Donkey (y)from the set of all donkeys, then εa*yDonkey (y) selects from the set of donkeys owned byx.This approach to dealing with pronouns using epsilon operatorsindexed by choice functions enable von Heusinger to deal with a widevariety of circumstances (see Egli and von Heusinger, 1995; vonHeusinger, 2000).Applications of the epsilon-operator in formal semantics, and choicefunctions in general, have received significant interest in recentyears. Von Heusinger and Egli (2000a) list, among others, thefollowing: representations of questions (Reinhart, 1992), specificindefinites (Reinhart 1992; 1997; Winter 1997), E-type pronouns(Hintikka and Kulas 1985; Slater 1986; Chierchia 1992, Egli and vonHeusinger 1995) and definite noun phrases (von Heusinger,1997, 2004). For discussion of the issues and applications of the epsilonoperator in linguistics and philosophy of language, see B. H. Slater'sarticle on epsilon calculi (cited in the Other Internet Resourcessection below), and the collections (available online) edited by vonHeusinger et al., listed in the Bibliography.Another application of epsilon calculus is as a general logic forreasoning about arbitrary objects. Meyer Viol (1995) provides acomparison of the epsilon calculus with Fine's (1985) theory ofarbitrary objects. Indeed, the connection is not hard to see. Given theequivalence ∀x A(x) ≡A(εx (¬A)), the term εx(¬A) is an arbitrary object in the sense that it is anobject of which A is true iff A is truegenerally.Meyer Viol (1995, 1995a) contain further proof- and model-theoreticstudies of the epsilon calculus; specifically intuitionistic epsiloncalculi. Here, the epsilon theorems no longer hold, i.e.,introduction of epsilon terms produces non-conservative extensions ofintuitionistic logic. In fact, as was shown by Bell (1993a, 1993b;Meyer Viol, 1995), addition of the epsilon operator to intuitionisticpredicate logic allows us to prove the intuitionistically non-validprinciples ¬A ∨¬¬A and (A → B) ∨ (A→ B). The full principle of the excluded middle can only be provedif we also add epsilon extensionality.∀x (A(x) ↔ B(x)) → εx A =εx BThis result provides a rigorous justification of Hilbert's originalconjecture that the principle of the excluded middle is, in a sense, aspecial case of the axiom of choice, and that only with epsilonextensionality do we get the full strength of the choice principle.Other model-theoretic investigations of epsilon operators inintuitionistic logic can be found in DeVidi (1995). Forepsilon-operators in many-valued logics, see Mostowski (1963), formodal epsilon calculus, Fitting (1975).BibliographyThe following list of references provides a starting point forexploring the literature, but is by no means comprehensive.Hilbert's ProgramThe following source books have many of the original papers:Bennacerraf, P., Putnam, H. (eds.), 1983, Philosophy ofMathematics , 2nd ed., Cambridge: Cambridge University PressEwald, W. B. (ed.), 1996, From Kant to Hilbert. A Source Bookin the Foundations of Mathematics, Vol. 2, Oxford: OxfordUniversity PressMancosu, P. (ed.), 1998, From Brouwer to Hilbert. The Debate onthe Foundations of Mathematics in the 1920s, Oxford: OxfordUniversity Pressvan Heijenoort, J. (ed.), 1967, From Frege toGödel. A Source Book in Mathematical Logic.Cambridge, Mass.: Harvard University PressOverviews of the historical development of logic and proof theory inthe Hilbert school can be found inAvigad J. and Reck, E., 2001, ‘Clarifying the nature of theinfinite": 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 andR. S. Cohen, Quebec Studies in the Philosophy of Science, Vol. 1,Dordrecht: Kluwer, 135-187Mancosu, P., 1998a, ‘Hilbert and Bernays onmetamathematics’, in Mancosu, 1998, 149-188Moore, G. H., 1997, ‘Hilbert and the emergence of modernmathematical logic’, Theoria (Segunda Epoca),12:65-90Peckhaus, V., 1990, Hilbertprogramm und KritischePhilosophie, Göttingen: Vandenhoek & RuprechtSieg, W., 1988, ‘Hilbert's program sixty years later’,Journal of Symbolic Logic, 53: 338-348Sieg, W., 1990, ‘Reflections on Hilbert's program’, W.Sieg (ed.), Acting and Reflecting, Dordrecht: KluwerSieg, 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 ofSymbolic Logic, 5: 331--366 [Available online in Postscript]Zach, R., 2003, ‘The practice of finitism. Epsilon calculusand consistency proofs in Hilbert's Program’, Synthese 137:211-259. [Preprint available online]The Early History of the Epsilon Calculus and Epsilon SubstitutionMethodThe original work:Ackermann, W., 1924, ‘Begründung des’’tertium non datur’’ mittels der HilbertschenTheorie der Widerspruchsfreiheit’, MathematischeAnnalen, 93:1-36Ackermann, W., 1937-38, ‘Mengentheoretische Begründungder Logik’, Mathematische Annalen, 115:1-22Ackermann, W., 1940, ‘Zur Widerspruchsfreiheit derZahlentheorie’, Mathematische Annalen, 117:162-194Hilbert, D., 1922, ‘Neubegründung der Mathematik: ErsteMitteilung’, Abhandlungen aus dem Seminar der HamburgischenUniversität , 1:157-177, English translation in Mancosu,1998, 198-214 and Ewald, 1996, 1115-1134Hilbert, D., ‘Die logischen Grundlagen der Mathematik’,Mathematische Annalen, 88:151-165, English translation inEwald, 1996, 1134--1148Hilbert, D., Bernays, P., 1934, Grundlagen der Mathematik, Vol. 1, Berlin: SpringerHilbert, D., Bernays, P., 1939, Grundlagen der Mathematik, Vol. 2, Berlin: Springervon Neumann, J., 1927, ‘Zur HilbertschenBeweistheorie’, Mathematische Zeitschrift, 26:1-46Ackermann's 1940 proof is discussed inHilbert, D., Bernays, P., 1970, ‘Grundlagen derMathematik’, Vol. 2, 2nd, edition, Berlin: Springer, SupplementVWang, H., 1963, A Survey of Mathematical Logic, Peking:Science PressMaehara showed how to prove the second epsilon theorem using cutelimination, and then strengthened the theorem to include the schema ofextensionality, inMaehara, S., 1955, ‘The predicate calculus withε-symbol’, Journal of the Mathematical Society ofJapan, 7:323-344Maehara, S., 1957, ‘Equality axiom on Hilbert'sε-symbol’, Journal of the Faculty of Science,University of Tokyo, Section 1, 7:419-435An early application of epsilon substitution is Georg Kreisel'sno-counterexample interpretation.Kreisel, G, 1951, ‘On the interpretation of non-finitistproofs - part I’, Journal of Symbolic Logic,16:241-267The following provide modern presentations of Hilbert's epsiloncalculus, not just from an introductory standpoint:Leisenring, A. C., 1969, Mathematical Logic and Hilbert'sEpsilon-Symbol, London: MacdonaldMints, G., 1996, ‘Thoralf Skolem and the epsilon substitutionmethod for predicate logic’, Nordic Journal of PhilosophicalLogic, 1:133-146 [Available online]Moser, G., 2000, The Epsilon Substitution Method, Master'sThesis, University of LeedsMoser, G., Zach, R., 2006, ‘The epsilon calculus andHerbrand complexity’, Studia Logica, 82(1):133-155. [Preprint available online in PDF]Corrections to errors in the literature (including Leisenring'sbook) can be found inFlannagan, T. B., 1975, ‘On an extension of Hilbert's secondε-theorem’, Journal of Symbolic Logic,40:393-397Ferrari, P. L., 1987, ‘A note on a proof of Hilbert's secondε-theorem’, Journal of Symbolic Logic,52:214-215Yashahura, M., 1982, ‘Cut elimination inε-calculi’, Zeitschrift für mathematische Logikund Grundlagen der Mathematik, 28:311-316A variation of the epsilon calculus based on Skolem functions, andtherefore compatible with first-order logic, is discussed inDavis, M., and R. Fechter, 1991, ‘A free variable version ofthe first-order predicate calculus’, Journal of Logic andComputation, 1:431-451General References for Proof TheoryBuss, S. (ed.), 1998. The Handbook of Proof Theory,Amsterdam: North-HollandTakeuti, G., 1987, Proof Theory, second edition.Amsterdam: North-Holland, AmsterdamTroelstra, A. S., Schwichtenberg, H., 2000, Basic ProofTheory, second edition. Cambridge: Cambridge University PressThe following contains a number of proof-theoretic results that areproved using methods similar to the ones used by Hilbert, Bernays, andAckermann, though using Skolem functions instead of epsilon terms:Shoenfield, J., 1967, Mathematical Logic, Reading,Mass.:Addison-Wesley, republished by the Association for SymbolicLogic, 2001For more on ordinal analysis, see, for example:Takeuti, G., Proof Theory (see above)Pohlers, Wolfram, 1998, ‘Subsystems of set theory andsecond-order number theory’, in S. Buss (ed.), The Handbookof Proof Theory (see above), 209-335Herbrand's TheoremHerbrand's theorem originally appeared inHerbrand, J., 1930, Recherches sur la thèorie de ladèmonstration, Dissertation, University ofParisEnglish translations can be found in van Heijenoort (see above),andHerbrand, J., 1971, Collected Works. W. Goldfarb (ed.),Cambridge, Mass.: Harvard University PressFurther historical information can be found inDreben, B., Andrews, P., Aanderaa, S., 1963, ‘False lemmas inHerbrand’, Bulletin of the American MathematicalSociety, 69:699-706The literature on Herbrand's theorem is vast. For some generaloverviews, in addition to the general proof-theoretic references above,seeBuss, S., 1995, ‘On Herbrand's theorem’, Logic andComputational Complexity (Indianapolis, IN, 1994), Lecture Notesin Computer Science 960, Berlin: Springer, 195-209 [Available online in PDF]Girard, J.-Y., 1982, ‘Herbrand's theorem and prooftheory’, Proceedings of the Herbrand Symposium,Amsterdam: North-Holland, 29-38Statman, R., 1979, ‘Lower bounds on Herbrand'stheorem’, Proceedings of the American MathematicalSociety, 75:104-107Voronkov, A., 1999, ‘Simultaneous rigid E-unification andother decision problems related to the Herbrand theorem’,Theoretical Computer Science, 224:319-352A striking application of Herbrand's theorem and related methods isfound in Luckhardt's analysis of Roth's theorem:Luckhardt, H., 1989, ‘Herbrand-Analysen zweier Beweise desSatzes von Roth: Polynomiale Anzahlschranken’, Journal ofSymbolic Logic, 54:234-263For a discussion of useful extensions of Herbrand's methods, seeSieg, W., 1991, ‘Herbrand analyses’, Archive forMathematical Logic, 30:409-441A model-theoretic version of this is discussed inAvigad, J., 2002, ‘Saturated models of universaltheories’, to appear in the Annals of Pure and AppliedLogicMore Recent Developments in the Epsilon Substitution MethodIn the following two papers, William Tait analyzed the epsilonsubstitution 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 transfiniterecursion,’ Journal of Symbolic Logic 30:155-174.More streamlined and modern versions of this approach can be foundin:Avigad, J., 2002, ‘Update procedures and the 1-consistency ofarithmetic’, Mathematical Logic Quarterly, 48:3-13.Mints, G., 2001, ‘The epsilon substitution method andcontinuity’, in W. Sieg et al. (eds.), Reflectionson the Foundations of Mathematics: Essays in Honor of SolomonFeferman, Lecture Notes in Logic 15, Association for SymbolicLogicThe following paper shows that the epsilon substitution method forfirst-order arithmetic is, in fact, strongly normalizing:Mints, G., 1996, ‘Strong termination for the epsilonsubstitution method’, Journal of Symbolic Logic,61:1193-1205A connection between cut elimination and epsilon substitution methodis explored inMints, G., 1994, ‘Gentzen-type systems and Hilbert's epsilonsubstitution method. I’, Logic, Methodology and Philosophy ofScience, IX (Uppsala, 1991), Amsterdam: North-Holland, 91-122The epsilon substitution method has been extended to predicativefragments of second-order arithmetic in:Mints, G., Tupailo, S., Buchholz, W., 1996, ‘Epsilonsubstitution method for elementary analysis’, Archive forMathematical Logic, 35:103-130Mints, G., Tupailo, S., 1999, ‘Epsilon-substitution methodfor the ramified language andΔ11-comprehension rule’, in A.Cantini et al. (eds.), Logic and Foundations ofMathematics (Florence, 1995), Dordrecht: Kluwer, 107-130Arai, T., 2002, ‘Epsilon substitution method for theories ofjump hierarchies’, Archive for Mathematical Logic,2:123-153The following papers address impredicative theories:Arai, T., 2003, ‘Epsilon substitution method forID1(Π01 ∨ Σ01)’, Annals of Pure and Applied Logic 121:163-208.Mints, G., 2001, ‘An approach to an epsilon-substitutionmethod for ID1’, preprint, Institute Mittag Leffler, 45, MLI,StockholmA development of set theory based on the epsilon-calculus is givenbyBourbaki, N., 1958, Theorie des ensembles , Paris:HermannEpsilon Operators in Linguistics, Philosophy, and Non-classicalLogicsThe following is a list of some publications in the area of languageand linguistics of relevance to the epsilon calculus and itsapplications. The reader is directed in particular to the collectionsvon Heusinger and Egli (2000) and von Heusinger et al. (2002)for further discussion and references.Bell, J. L., 1993a. ‘Hilbert's epsilon-operator and classicallogic’, Journal of Philosophical Logic, 22:1-18Bell, J. L., 1993b. ‘Hilbert's epsilon operator inintuitionistic type theories’, Mathematical LogicQuarterly 39:323-337Chierchia, G., 1992. ‘Anaphora and dynamic logic’.Linguistics and Philosophy, 15:111-183DeVidi, D., 1995. ‘Intuitionistic epsilon- andtau-calculi’, Mathematical Logic Quarterly41:523--546Evans, G., 1980, ‘Pronouns’, LinguisticInquiry , 11:337-362Egli, U., von Heusinger, K., 1995, ‘The epsilon operator andE-type pronouns’, in U. Egli et al. (eds.), LexicalKnowledge 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--16Hintikka, J., Kulas, J., 1985. Anaphora and DefiniteDescriptions: Two Applications of Game-Theoretical Semantics.Dordrecht: ReidelKempson, R., Meyer Viol, W., and Gabbay, D., 2001. Dynamic Syntax: The Flow of Language Understanding. Oxford:BlackwellMeyer Viol, W. P. M., 1995, Instantial Logic. An Investigationinto Reasoning with Instances . Ph.D. thesis, University ofUtrecht. ILLC Dissertation Series 1995-11Meyer Viol, W., 1995a. ‘A proof-theoretic treatment ofassignments’, Bulletin of the IGPL, 3:223-243 [Available online]Mostowski, A., 1963. ‘The Hilbert epsilon function inmany-valued logics’, Acta Philosophica Fennica,16:169-188Reinhart, T., 1992. ‘Wh-in-situ: An apparent paradox’.In: P. Dekker and M. Stokhof (eds.). Proceedings of the EighthAmsterdam Colloquium December 17-20, 1991. ILLC. University ofAmsterdam, 483-491Reinhart, T., 1997. ‘Quantifier scope: How labor is dividedbetween QR and choice functions’. Linguistics andPhilosophy, 20:335-397Slater, B. H. 1986, ‘E-type pronouns andε-terms’, Canadian Journal of Philosophy,16:27-38Slater, B. H. 1988, ‘Hilbertian reference’,Noûs, 22:283-97Slater, B. H. 1994, ‘The epsilon calculus’problematic’, Philosophical Papers, 23:217-42Slater, B.H. 2000, ‘Quantifier/variable-binding’,Linguistics and Philosophy, 23:309-21von Heusinger, K., 1997. ‘Definite descriptions and choicefunctions’. In: S. Akama (ed.). Logic, Language andComputation. Dordrecht: Kluwer, 61-91von Heusinger, K., 2000, ‘The Reference ofIndefinites’, in von Heusinger and Egli, (2000), 265-284von Heusinger, K., 2004, ‘Choice functions and the anaphoricsemantics of definite NPs’, Research in Language andComputation, 2:309-329.von Heusinger, K., Egli, U., (eds.), 2000. Reference andAnaphoric Relations. Dordrecht: Kluwer, 265-284von Heusinger, K., Egli, U., 2000a. ‘ Introduction: Referenceand the Semantics of Anaphora’, in von Heusinger and Egli (2000),1-13von Heusinger, K., Kempson, R., Meyer-Viol, W., (eds.), 2002.Proceedings of the Workshop Choice Function and Natural LanguageSemantics, Arbeitspapier 110. Fachbereich Sprachwissenschaft,Universität KonstanzWinter, Y., 1997. ‘Choice functions and the scopal semanticsof indefinites’. Linguistics and Philosophy,20:399-467Other Internet ResourcesEpsilon 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 Copyright © 2007 byJeremy Avigad<avigad@cmu.edu>Richard Zach<rzach@ucalgary.ca> |
|
