The Grice Club


The Grice Club

The club for all those whose members have no (other) club.

Is Grice the greatest philosopher that ever lived?

Search This Blog

Thursday, February 26, 2015

Grice on the epsilon/iota distinction: 'the', 'a', and their attending implicatures -- with a nod to R. Carnap, "On the use of Hilbert epsilon operator in scientific theories".

We shall consider some of the pragmatic relevance of the so-called
The Epsilon Calculus.



What is the Epsilon Calculus?
The e-calculus is a formalisation of logic without quantifiers

but with the e-operator.

is a formula,
is an e-term.

is an "indefinite description".
is some x for which A(x) is true.

e can replace 9: 9xA(x),A(exA(x))

Axioms of e-calculus:

Propositional tautologies

Equality schemata


Predicate logic, such as System GHP -- a highly powerful version of Myro's System G, can be embedded in e-calculus.


Why Should You Care?
Epsilon calculus is of significant historical interest.

It is connected with the origins of proof theory.

While we often speak of Grice's programme, this is Hilbert’s Programme.

It can provide alternative basis for fruitful proof-theoretic research.

Epsilon Theorems and Herbrand’s Theorem: proof

theory without sequents
The Epsilon Substitution Method yields functionals, e.g.,

` 8x9yA(x,y) 8n: ` A(n, f (n))

It is an Interesting Logical Formalism

The epsilon calculus Trades logical structure for term structure.

It is Suitable for proof formalization.

Choice in logic.

It is Inherently classical (but see work of Bell, DeVidi, Fitting,

and Mostowski).
It has Expressive power.

There are Other Applications:

One is in the use of choice functions in provers (e.g., HOL, Isabelle).

Another is in the Applications in linguistics (choice functions, anaphora).



The epsilon calculus was first introduced by Hilbert

as the basis for his formulation of mathematics for which

Hilbert’s Programme was supposed to be carried out.
The Motivation was Logical choice function. The e-terms represent

“ideal elements” in proofs.

Original work in proof theory (pre-Gentzen) concentrated
on e-calculus and e-substitution method (Ackermann, von

Neumann, Bernays)

The first correct proof of Herbrand’s Theorem was via Epsilon


Epsilon substitution method was used by Kreisel for nocounterexample

interpretation leading to work on analysis of

proofs by Kreisel, Luckhardt, Kohlenbach.

Recent work on ordinal analysis of subsystems of analysis

by Arai, Avigad, Buchholz, Mints, Tupailo, Tait.

The Epsilon Calculus: Syntax
Language of the Elementary Calculus LEC:

There are free variables: a, b, c, . . .

There are bound variables: x, y, z, . . .

There are constant and function symbols: f , g, h, . . . with arities

ar( f ), . . .

There are predicate symbols: P, Q, R, . . . with arities ar(P), . . .

There is equality: =

There are Propositional connectives: ^, _, !, ¬

Language of the Predicate Calculus LPC:

There are two Quantifiers: 8, 9

Language of the Epsilon Calculus Le:

Epsilon: e


1. Any free variable a is a semi-term.

2. Any bound variable x is a semi-term.

3. If f is a function symbol with ar( f ) = 0, f is a semi-term.

4. If f is a function symbol with ar( f ) = n > 0, and t1, . . . , tn

are semi-terms,  f (t1, . . . , tn) is a semi-term.

5. If P is a predicate symbol with ar(P) = n > 0, and t1, . . . , tn

are terms, P(t1, . . . , tn) is an (atomic) semi-formula.

6. If A and B are semi-formulas,  ¬A, A ^ B, A _ B and

A!B are semi-formulas.

7. If A(a) is a semi-formula containing the free variable a and

x is a bound variable not occurring in A(a)8xA(x) and

9xA(x) are semi-formulas.

8. If A is a semi-formula containing the free variable a and x

is a bound variable not occurring in A(a)exA(x) is a

semi-term (an e-expression).


Terms and formulas are defined exactly as above except

that clause (2) is dropped. In other words: a semi-term is

a term and a semi-formula a formula if it contains no bound
variables without a matching 8, 9, or e.

The only sub-semi-terms of a free variable a is a itself. It

has no immediate sub(semi)terms.
A bound variable x has no sub-terms or immediate sub-semi-

terms. Its only sub-semi-term is x itself.

If f (t1, . . . tn) is a semi-term, its immediate sub-semiterms

are t1, . . . , tn, and its immediate subterms are those

among t1, . . . , tn which are terms, plus the immediate

subterms of those among t1, . . . , tn which aren’t terms.

Its sub-semi-terms are f (t1, . . . , tn) and the sub-semi-terms

of t1, . . . , tn; its subterms are those of its sub-semi-terms

which are terms.
If P(t1, . . . , tn) is an atomic semi-formula, its immediate

sub-semi-terms are t1, . . . , tn. Its immediate sub-terms are

those among t1, . . . , tn which are terms, plus the immediate

sub-terms of those among t1, . . . , tn which aren’t terms. Its

sub-semi-terms are the sub-semi-terms of t1, . . . , tn.


If A is a semi-formula of the form B^C, B_C, B !C, ¬B,

8xB or 9xB, its immediate sub-semi-formulas and its

sub-semi-formulas are those of B and C.

If exA(x) is an e-expression, its immediate sub(semi)

formulas and its sub(semi)formulas are those of A(x).


An e-term exA(x) is an e-MATRIX if all

terms occurring in A are free variables, each of which occurs

exactly once.
Denote e-matrices as exA(x;a1, . . . ,ak) where the variables

a1, . . . ,ak displayed are all the free variables occurring in it.

Two matrices exA(x;a1, . . . ,ak), exA(x;b1, . . . ,bk) that differ

only in the indicated tuples of variables a and b, respectively,

are considered to be equal. The set of all matrices is denoted

Corresponding to each e-term exA(x) there exists a unique

matrix exA(x;a1, . . . ,ak) and a unique sequence t1, . . . , tk of

terms such that exA(x, t1, . . . , tk) = exA(x).

Example: exA(s, e|y{Bz(y})

, ezC(x, t))

Its matrix is: exA(a,b, ezC(x,c))

The matrix of exA(x) is obtained by replacing all immediate

subterms of exA(x) by distinct new free variables. In this newly

obtained term we replace distinct occurrences of the same

variable by different variables.


The Epsilon Calculus: Intensional Semantics
An intensional choice function F for a set X is a

function F: 2X ×Mat×X<w ! X so that for S X, a matrix

exA(x;a1, . . . ,an) and d1, . . . , dn 2S, F(S, exA(x;a1, . . . ,an), hd1, . . . ,dni)2

S if S 6= /0.

An intensional e-structure M = h|M|, (·)M,FMi consist of

a domain |M| 6= /0, an interpretation function (·)M, and an

intensional choice function FM for |M|, where

If ar( f ) = 0fM 2 |M|

If ar( f ) = n > 0fM: |M|n !|M|

If ar(P) = n > 0PM |M|n

A variable assignment s for M is a function s : FV !|M|.

We write s c s0 if s(a) = s0(a) for all free variables a other than




The value tM,s of a term t and the satisfaction relation

M, s |= A is defined by:

If a is a free variable, aM,s = s(a).

If f is a constant symbol, fM,s = fM.

If f (t1, . . . , tn) is a term, ( f (t1, . . . , tn))M,s = fM(tM,s

1 , . . . , tM,s

n ).

If P(t1, . . . , tn) is an atomic formula, M, s |= P(t1, . . . , tn)

iff htM,s

1 , . . . , tM,s

n i 2 PM.

If A and B are formulas,

M, s |= A^B iff M, s |= A and M, s |= B.

M, s |= A_B iff M, s |= A or M, s |= B.

M, s |= A!B iff M, s 6|= A or M, s |= B.

M, s |= ¬A iff M, s 6|= A.

If 9xA(x) is a formula and c a free variable not in A(x),

M, s |= 9xA(x) iff M, s0 |= A(c) for some s0 c s.

If 8xA(x) is a formula and c a free variable not in A(x),

M, s |= 8xA(x) iff M, s0 |= A(c) for all s0 c s.

If e is an e-term with matrix exA(x;a1, . . . ,an) so that e =

exA(x;t1, . . . , tn), and

X = {d 2 |M| :M, s0 |= A(c;t1, . . . , tn), s0 c s, s0(c) = d},

eM,s = FM(X, exA(x;a1, . . . ,an), htM,s

1 , . . . , tM,s

n i).


Axiomatization of the Epsilon Calculus: Axioms
Let AxEC be the set of formulas containing all formulas

which are either substitution instances of propositional

tautologies, or substitution instances of
a = a

a = b ! (A(a)!A(b)).

AxPC is AxEC together with all substitution instances of

A(a) ! 9xA(x)

8xA(x) ! A(a).

Any substitution instance of

is called a critical formula.

We obtain Axe

EC and Axe

PC by adding the critical formulas

to AxEC and AxPC, respectively.


A deduction in EC or ECe is a sequence A1, . . . , An of

formulas such that each Ai is either in AxEC or Axe

EC or follows

from Aj, Ak with j,k < i by modus ponens:

B,B!C ` C

A deduction in PC or PCe is a sequence A1, . . . , An of

formulas such that each Ai is either in AxPC or Axe

PC or follows

from Aj, Ak with j,k < i by modus ponens: B,B !C ` C, or

follows from Aj with j < i by generalization:

B!A(a) ` B!8xA(x)

A(a)!B ` 9xA(x)!B

A formulas A is called deducible (in EC, ECe, PC, PCe),

` A, if there is a deduction (in AxEC, Axe

EC, AxPC, Axe


respectively) which has A as its last formula.


Extensional Epsilon Calculus
Alternative semantics: Choice function maps just sets to

FM(S) 2 S

Then if e = exA(x, t1, . . . , tn)

eM,s = FM({d 2 |M| :M, s0 |= A(c;t1, . . . , tn), s0 c s0, s0(c) = d})

In extensional e-semantics, equivalent e-terms have same

value, i.e., it makes valid the e-extensionality axiom

8x(A(x)$B(x))!exA(x) = exB(x)


Embedding PC in ECe

The epsilon operator allows the treatment of quantifiers in
a quantifier-free system: using e terms it is possible to define

9x and 8x as follows:

9xA(x) , A(exA(x))

8xA(x) , A(ex¬A(x))

Define Ae by:

xe = x, ae = a

[exA(x)]e = exA(x)e

f (t1, . . . , tn)e = f (te

1, . . . , te

n), P(t1, . . . , tn)e = P(te

1, . . . , te


(A ^ B)e = Ae ^ Be, (A _ B)e = Ae _ Be, (A ! B)e = Ae ! Be,

(¬A)e = ¬Ae.

(9xA(x))e = Ae(exAe(x)0).

(8xA(x))e = Ae(ex¬Ae(x)0).

where Ae(x)0 is Ae(x) with all variables bound by quantifiers or

e’s in Ae(x) renamed by new bound variables (to avoid collision

of bound variables when exAe(x) is substituted into Ae(x) where

x may be in the scope of a quantifier or epsilon binding a

variable occurring in Ae(x).


Embedding PC in ECe: Examples

9x(P(x) _ 8yQ(y))e =

= [P(x)_8yQ(y)]e {x ex [P(x)_8yQ(y)]e}

[P(x)_8yQ(y)]e = P(x)_Q(e|y¬{Qz (y})


= P(x)_Q(e|y¬{Qz (y})


) {x ex [P(x)_Q(e|y¬{Qz (y})


| {z }

= P(ex [P(x)_Q(e|y¬{Qz (y})


| {z }

)_Q(e|y¬{Qz (y})


[9x 9y A(x,y)]e =

= [9yA(x,y)]e {x ex [9yA(x,y)]e}

[9yA(x,y)]e = A(x, e|yA{(zx,y})


= A(x, e|yA{(zx,y})


){x e|xA(x, e{zzA(x, z)})


= A(e|xA(x, e{zzA(x, z)})


, eyA(e|xA(x, e{zzA(x, z)})



| {z }


Embedding PC in ECe (cont’d)

Prop. If PCe ` A,  ECe ` Ae.

Translations of quantifier axioms provable from critical

[A(t)!9xA(x)]e = Ae(t)!Ae(exA(x)e)

Suppose PCe ` B!A(a), and a does not occur in B. By IH, we

have a proof p in ECe of Be !A(a)e.
Replacing a everywhere

in p by ex¬A(x) results in a proof of

[B!8xA(x)]e = Be !Ae(ex¬A(x)e).


The Epsilon Theorems
First Epsilon Theorem. If A is a formula without bound

variables (no quantifiers, no epsilons) and PCe ` EC `


Extended First Epsilon Theorem. If 9x1 . . .9xnA(x1, . . . ,xn)

is a purely existential formula containing only the bound
variables x1, . . . , xn, and

PCe ` 9x1 . . .9xnA(x1, . . . ,xn),

there are terms ti j such that

EC `

A(ti1, . . . , tin).

Second Epsilon Theorem. If A is an e-free formula and

PCe ` A, PC ` A.


Degree of an e-Term

deg(exA(x)) = 1 if A(x) contains no e-subterms.

If e1, . . . , en are all immediate e-subterms of A(x),

deg(exA(x)) = max{deg(e1), . . . ,deg(en)}+1.

Rank of an e-Expression

An e-expression e is subordinate to exA if e is a proper

sub-expression of A and contains x.

rk(e) = 1 if no sub-e-expression of e is subordinate to e.

If e1, . . . , en are all the e-expressions subordinate to e,

rk(e) = max{rk(e1), . . . ,rk(en)}+1


P(ex [P(x)_Q(e|y¬{Qz (y})


| {z }

)_Q(e|y¬{Qz (y})


deg(e1) = 1, deg(e2) = 2

rk(e1) = rk(e2) = 1

A(e|xA(x, e{zzA(x, z)})


, eyA(e|xA(x, e{zzA(x, z)})



| {z }

deg(e2) = 1, deg(e1(e2)) = 2

rk(e2) = 2, rk(e1(e2)) = 1


Rank of Critical Formulas and Derivations
Rank of a critical formula A(t)!A(exA(x)) is rk(exA(x)).

Rank of a derivation rk(p): maximum rank of its critical

Critical e-term of a derivation: e-term e so that A(t)!A(e)

is a critical formula.
Order of a derivation o(p, r) wrt. rank r: number of different

critical e-terms of rank r.


The First Epsilon Theorem
(Proof for case without =)

Suppose PCe `p E and E contains no bound variables. We

show that EC ` E by induction on the rank and degree of p.

First, w.l.o.g. we assume p is actually a derivation in ECe .

Since E contains no bound variables, Ee = E.

Second, w.l.o.g. we assume p doesn’t contain any free

variables (replace free variables by new constants—may be

resubstituted later).
Let e be a critical e-term of p of maximal degree

among the critical e-terms of maximal rank.
Then there is pe

with end formula A so that rk(pe) rk(p), deg(pe) deg(p) and

o(pe,rk(e)) = o(p,rk(e))1.


The First Epsilon Theorem: Main Lemma
Proof. Construct pe as follows:

Suppose A(t1) ! A(e), . . . , A(tn) ! A(e) are all the critical

formulas belonging to e. For each critical formula


we obtain a derivation
pi ` A(ti)!E :

Replace e everywhere it occurs by ti. Every critical

formula A(t) ! A(e) belonging to e turns into a formula

of the form B!A(ti).

Add A(ti) to the axioms. Now every such formula is

derivable using the propositional tautology
A(ti)!(B!A(ti)) ,

and modus ponens.
Apply the deduction theorem for the propositional

calculus to obtain pi.


The First Epsilon Theorem: Main Lemma
2. Obtain a derivation p0 of

¬A(ti)!E by:


¬A(ti) to the axioms. Now every critical formula

A(ti) ! A(e) belonging to e is derivable using the

propositional tautology ¬A(ti)!(A(ti)!A(e)).

Apply the deduction theorem.

Combine the proofs
pi ` A(ti)!E ,

p0 `

¬A(ti)!E ,

to get pe ` E (case distinction)


Why is this correct?
Verify that the resulting derivation is indeed a derivation in
ECe with the required properties.

We started with critical formulas of the form
A(ti)!A(e) .

The proof p0 does not contain any critical formulas

belonging to e. Hence e is no longer a critical e-term

in p0. All other critical formulas (and the critical e-terms

they belong to) remain unchanged. Thus o(p0,rk(e)) =


In the construction of pi, we substituted e by t throughout

the proof. Such uniform substitutions of a term by another

are proof-preserving.
Replacing e by ti in A(e) indeed results in A(ti), since e

cannot occur in A(x)—else e = exA(x) would be a proper

subterm of itself, which is impossible.
If e appears in another critical formula B(s)!B(eyB(y)), we

have three cases.

Case I
Case: e occurs only in s.

Replacing e by ti results in a critical formula B(s0) !


The new critical critical formula belongs to the same e-term

as the original formula.
Hence o(pi,rk(e)) = o(p,rk(e))1.



Case II
Case: e may occur in B(y) and perhaps also in s, but

contains neither s nor eyB(y).

In other words, the critical formula has the form

But then the e-term belonging to this critical formula

e0 = eyB0(y,e) ,

is of higher degree than e.

By our assumptions, this implies that rk(eyB0(y,e)) < rk(e).

Replacing e by ti results in a different critical formula

B0(s0(ti), ti)!B0(eyB0(y, ti), ti) ,

belonging to the e-term eyB0(y, ti) which has the same rank as

e0 and hence a lower rank than e itself.

Hence again o(pi,rk(e)) = o(p,rk(e))1.


Case III
Case: e does contain s or eyB(y).

Then e is of the form e0(s) or e0(eyB(y)), and

B(a) is really of the form B0(e0(a)) where e0(a) is an e-term

of the same rank as e.

Then eyB(y) has the form eyB0(e0(y)), to which the e-

expression e0(y) is subordinated.

But then eyB0(e0(y)) has higher rank than e0(y), which has

the same rank as e. This cannot happen.

Finally the proof of the lemma follows: In all of the cases
considered one e-critical term of rk(e) was removed and other

e-critical terms of rk(e) remained equal. Thus o(pe,rk(e)) =

o(p,rk(e))1 holds.


The First Epsilon Theorem: Proof
By induction on rk(p).

If rk(p) = 0, there is nothing to prove (no critical formulas).

If rk(p) > 0 and the order of p wrt. rk(p) is m, then mfold

application of the lemma results in a derivation p0 of rank

< rk(p).


The Extended First Epsilon Theorem
If 9x1 . . .9xkA(x1, . . . ,xk) is a purely existential

formula containing only the bound variables x1, . . . , xk, and

PCe ` 9x1 . . .9xkA(x1, . . . ,xk),

there are terms ti j such that

EC `

A(ti1, . . . , tik).

Consider proofs in PCe of 9x1 . . .9xkA(x1, . . . ,xk), where

A(a1, . . . ,ak) contains no bound variables.

Employing embedding we obtain a derivation p of

A(s1, . . . , sk), where s1, . . . , sk are terms (containing e’s).

Proof Sketch. We employ the same sequence of

elimination steps as in the proof of the First Epsilon Theorem.
The difference being that now the end-formula A(s1, . . . , sk) may

contain e-terms.

Hence the first elimination step transform the end-formula

into a disjunction.
A(s01, . . . , s0k)_. . ._A(sn1, . . . , snk) .


The Second Epsilon Theorem
If A is an e-free formula and PCe ` A, PC `


Assume A has the form

9x8y9zB(x,y, z) ,

with B(x,y, z) quantifier-free and no other than the indicated

variables occur in A.

Herbrand Normal Form. Suppose A = 9x8y9zB(x,y, z).

f is a new function symbol, the Herbrand normal form AH

of A is 9x9zB(x, f (x), z).

Suppose PCe ` A.
Then PCe ` AH.


Second Epsilon Theorem: Proof
The Strong First Epsilon Theorem yields:
There are e-free terms ri, si so that

EC `

B(ri, f (ri), si) (1)

We now can replace the ti by new free variables ai and obtain

from (1), that _

B(ri,ai, si) , (2)

is deducible in EC.

Then the original prenex formula A can be obtained

from (2) if we employ the following rules (deducible in PC)

(μ) : F _G(t) ` F _9yG(y)

(n) : F _G(a) ` F _8zG(z), provided a appears only in G(a)

at the displayed occurrences.


Conservative Extension. Due to the Second Epsilon

Theorem the Epsilon Calculus (with equality) is a conservative

extension of pure predicate logic.
Equivalence. Due to the Embedding Lemma we have

PCe ` A implies ECe ` Ae. Due to the Second Epsilon Theorem

we obtain ECe ` Ae implies PCe ` A.

Herbrand’s Theorem. Assume A = 9x8y9zB(x,y, z).

Iff PCe ` A, there are terms ri, si such that EC ` W

iB(ri, f (ri), si).


First Epsilon Theorem. Let A be a formula without

bound variables (no quantifiers, no epsilons) but possible
including =. Then

PCe [Ax ` A implies EC[Ax ` A ,

where Ax includes instances of quantifier-free (and e-free)

Extended First Epsilon Theorem. Let 9xA(x) be a

purely existential formula (possibly containing =). Then

PCe [Ax ` 9xA(x) implies

EC[Ax `

A(ti1, . . . , tin) ,

where Ax is defined as above.


Second Epsilon Theorem. If A is an e-free formula

(possibly containing =) and

PCe [ Ax ` A implies PC[Ax ` A ,

where Ax includes instances of e-free axioms.

Some facts in favour of the Epsilon Calculus:
The input parameter for the proof of Herbrand’s Theorem is

the collection of critical formulas C used in the derivation.

E.g. this gives a bound depending only on C.

The Epsilon Calculus allows a condensed representation

of proofs.
Why: Assume ECe ` Ae. Then there exists a tautology of

the form ^

i, j

(Bi(t j)!Bi(exBi(x)))!Ae . (3)

Thus as soon as the critical formulas Bi(t j) ! Bi(exBi(x))

are known, we only need to verify that (3) is a tautology to
infer that Ae is provable in ECe.

Formalization of proofs should be simpler in the Epsilon


A bluffer’s guide to Hilbert’s “Ansatz”
Assume we work within number theory and let N denote

the standard model of number theory.

For conciseness we ignore induction.
The initial substitution S0: Assign the constant function 0

to all e-terms (by assigning the constant function 0 to all


Assume the substitution Sn has already been defined.

Define Sn+1.
Pick a false critical axiom, e.g.

P(t)!P(exP(x)) .

False means wrt. to N and the current substitution Sn.

Let z 2 N denote the value of t under Sn.
Then the next

substitution Sn+1 is obtained by assigning the value z to


Note that the critical axiom P(t)!P(exP(x)) is true wrt. to N

and the current substitution Sn+1.


Peano Arithmetic: Results
1-consistency. Every purely existential formula

derivable in PAe is true.

Provable Recursive Functions. The numerical content

of proofs of purely existential formulas in PAe is extractable.

Put differently: The provable recursive functions of PAe are

exactly the < e0-recursive functions.

Assume PAe ` 8x9yA(x,y) with A(a,b) quantifier-free and

without free variables other than the shown. Then we can find
a < e0-recursive function f such that 8xA(x, f (x)) holds.


Peano Arithmetic: Results
Non-counter example interpretation. Let

9x8y9zA(a,x,y, z)

be deducible in PAe such that only the indicated free variable

a occurs.
Let 9x9zA(a,x, f (x), z) denote the Herbrand normal

form of A.

Then there exists < e0-recursive functionals G and H such

that for all functions f ,

A(n,G( f ,n), f (G),H( f ,n)) ,

The transformation ()e : Le ! LPC defined yesterday, can

be employed to show that Peano Arithmetic embeds into PAe:

Then if PA ` A, PAe ` Ae.


W. Ackermann. Begr ¨undung des Tertium non datur mittels der Hilbertschen
Theorie der Widerspruchsfreiheit. Mathematische Annalen, 93.

W. Ackermann. Zur Widerspruchsfreiheit der Zahlentheorie. Mathematische

Annalen, 117.

W. Ahrendt and M. Giese. Hilbert’s e-terms in automated theorem proving. In Proc.

T. Arai. Epsilon substitution method for theories of jump hierarchies. Archive for

Mathematical Logic, 41.
T. Arai. Epsilon substitution method for ID1(p01


). Annals of Pure and Applied


G. Asser. Theorie der logischen Auswahlfunktionen. Zeitschrift f ¨ur Mathematische

Logik und Grundlagen der Mathematik 3.

J. Avigad. Update procedures and the 1-consistency of arithmetic. Mathematical

Logic Quarterly 48.

J. Avigad and R. Zach. The Epsilon Calculus. In Edward N. Zalta, editor, The

Stanford Encyclopedia of Philosophy.

M. Baaz and A. Leitsch. Methods of function extensions. Collegium

Logicum—Annals of the Kurt G¨odel Society, 1.
J. L. Bell. Hilbert’s epsilon-operator and classical logic. Journal of Philosophical

Logic, 22.

J. L. Bell. Hilbert’s epsilon operator in intuitionistic type theories. Mathematical

Logic Quarterly, 39.
A. Blass and Y. Gurevich. The logic of choice. Journal of Symbolic Logic,

N. Bourbaki. E´ le´ments of Mathe´matique, volume Chap. I et II of Livre I (The´orie

des Ensembles). Paris.

W. Buchholz, G. Mints, and S. Tupailo. Epsilon substitution method for elementary
analysis. Archive for Mathematical Logic 35.

R. Carnap. On the use of Hilbert’s e-operator in scientific theories. In Essays on

the Foundations of Mathematics dedicated to A. A. Fraenkel on his Seventieth

D. DeVidi. Intuitionistic epsilon- and tau-calculi. Mathematical Logic Quarterly
P. L. Ferrari. A note on a proof of Hilbert’s second e-theorem. Journal of Symbolic

Logic, 52.


M. Fitting. A modal logic epsilon-calculus. Notre Dame Journal of Formal Logic,
T. B. Flannagan. On an extension of Hilbert’s second e-theorem. Journal of

Symbolic Logic, 40.

 D. Hilbert and P. Bernays. Grundlagen der Mathematik I. Springer, Berlin.

D. Hilbert and P. Bernays. Grundlagen der Mathematik II. Springer, Berlin.

U. Kohlenbach. On the no-counterexample interpretation. Journal of Symbolic

Logic, 64.

G. Kreisel. Interpretation of non-finitist proofs I,II. Journal of Symbolic Logic,

G. Kreisel. Mathematical significance of consistency proof. Journal of Symbolic

Logic, 23.

A.C. Leisenring. Mathematical Logic and Hilbert’s e-symbol. MacDonald Technical

and Scientific, London.

H. Luckhardt. Herbrand-Analysen zweier Beweise des Satzes von Roth:
Polynomiale Anzahlschranken. Journal of Symbolic Logic, 54.

S. Maehara. The predicate calculus with e-symbol. Journal of the Mathematical

Society of Japan, 7.

S. Maehara. Equality axiom on Hilbert’s e-symbol. Journal of the Faculty of

Science, University of Tokyo.

W. P. M. Meyer Viol. Instantial Logic. An Investigation into Reasoning with

Instances. ILLC Dissertation.

G. Mints. Epsilon substitution method for the theory of hereditarily finite sets
(Russian). In Proc. Eston. Acad. of Sci. Fiz.-Math.

G. Mints. Hilbert’s Substitution Method and Gentzen-type Systems. In Proc. of 9th

International Congress of Logic, Methododology and Philososophy of Science,

Uppsala, Sweden.
G. Mints. Strong termination for the epsilon substitution method. Journal of

Symbolic Logic, 61.

G. Mints. Thoralf Skolem and the epsilon substitution method for predicate logic.
Nordic Journal of Philosophical Logic, 1.

G. Mints. Strong termination for the epsilon substitution method for predicate logic.
Journal of Symbolic Logic.

G. Mints and S. Tupailo. Epsilon-substitution method for the ramified language and

-comprehension rule. In A. Cantini et al., editor, Logic and Foundations of



G. Moser. The Epsilon Substitution Method. Master’s Thesis, Deptartment of Pure

Mathematics, University of Leeds.
A. Mostowski. The Hilbert epsilon function in many-valued logics. Acta Philos.

Fenn., 16.

N. Motohasi. Epsilon theorems and elimination of uniqueness conditions. In Proc.

of the Patras Logic Symposium.
W. W. Tait. Functionals defined by transfinite recursion. Journal of Symbolic Logic,

W. W. Tait. The substitution method. Journal of Symbolic Logic, 30

J. v. Neumann. Zur Hilbertschen Beweistheorie. Mathematische Zeitschrift.
M. Yashahura. Cut elimination in e-calculi. Zeitschrift f ¨ur mathematische Logik und

Grundlagen der Mathematik, 28.

R. Zach. The practice of finitism. Epsilon calculus and consistency proofs in
Hilbert’s program. Synthese.

R. Zach. Hilbert’s “Verungl¨uckter Beweis”, the first epsilon theorem, and
consisteny proofs. History and Philosophy of Logic.

No comments:

Post a Comment