We shall consider some of the pragmatic relevance of the so-called
The Epsilon Calculus.
The e-calculus is a formalisation of logic without quantifiers
but with the e-operator.
If
A(x)
is a formula,
exA(x)
is an e-term.
Intuitively,
exA(x)
is an "indefinite description".
exA(x)
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
A(t)!A(exA(x))
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
Calculus
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
Mat.
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})
e
, 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 ) = 0, fM 2 |M|
If ar( f ) = n > 0, fM: |M|n !|M|
If ar(P) = n > 0, PM |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
c.
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
A(a)!A(exA(x))
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
PC,
respectively) which has A as its last formula.
Extensional Epsilon Calculus
Alternative semantics: Choice function maps just sets to
elements:
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
n).
(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})
e1
)
= P(x)_Q(e|y¬{Qz (y})
e1
) {x ex [P(x)_Q(e|y¬{Qz (y})
e1
)]
| {z }
e2
}
= P(ex [P(x)_Q(e|y¬{Qz (y})
e1
)]
| {z }
e2
)_Q(e|y¬{Qz (y})
e1
)
[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})
e1(x)
)
= A(x, e|yA{(zx,y})
e1(x)
){x e|xA(x, e{zzA(x, z)})
e2
}
= A(e|xA(x, e{zzA(x, z)})
e2
, eyA(e|xA(x, e{zzA(x, z)})
e2
,y)
| {z }
e1(e2)
)
Embedding PC in ECe (cont’d)
Prop. If PCe ` A, ECe ` Ae.
Translations of quantifier axioms provable from critical
formulas:
[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 ` A EC `
A.
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 `
_
i
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
Examples
P(ex [P(x)_Q(e|y¬{Qz (y})
e1
)]
| {z }
e2
)_Q(e|y¬{Qz (y})
e1
)
deg(e1) = 1, deg(e2) = 2
rk(e1) = rk(e2) = 1
A(e|xA(x, e{zzA(x, z)})
e2
, eyA(e|xA(x, e{zzA(x, z)})
e2
,y)
| {z }
e1(e2)
)
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
formulas.
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).
Lemma.
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
A(ti)!A(e),
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
V
¬A(ti)!E by:
• Add
V
¬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 ,
and
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)) =
o(p,rk(e))−1.
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) !
B(eyB(y)).
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
B0(s0(e),e)!B0(eyB0(y,e),e).
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
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 `
_
i
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
Theorem.
If A is an e-free formula and PCe ` A, PC `
A.
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).
If
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 `
_
i
B(ri, f (ri), si) (1)
We now can replace the ti by new free variables ai and obtain
from (1), that _
i
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).
Generalizations
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)
axioms.
Extended First Epsilon Theorem. Let 9xA(x) be a
purely existential formula (possibly containing =). Then
PCe [Ax ` 9xA(x) implies
EC[Ax `
_
i
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
Calculus.
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
e-matrices).
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
exP(x).
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)) ,
holds.
The transformation ()e : Le ! LPC defined yesterday, can
be employed to show that Peano Arithmetic embeds into PAe:
Then if PA ` A, PAe ` Ae.
References
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.
TABLEAUX’99, LNCS.
Mathematical Logic, 41.
T. Arai. Epsilon substitution method for ID1(p01
_s01
). Annals of Pure and Applied
Logic.
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,
65.
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
Anniversary.
D. DeVidi. Intuitionistic epsilon- and tau-calculi. Mathematical Logic Quarterly
41.
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,
16.
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,
16,17.
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
d11
-comprehension rule. In A. Cantini et al., editor, Logic and Foundations of
Mathematics.
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,
30
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.
Posts
No comments:
Post a Comment