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.

If

*A*(

*x*)

is a formula,

e

*xA*(*x*)
is an e-term.

Intuitively,

e

*xA*(*x*)
is an "indefinite description".

e

*xA*(*x*)
is some

*x*for which*A*(*x*) is true.
e can replace 9: 9

*xA*(*x*),*A*(e*xA*(*x*))
Axioms of e-calculus:

Propositional tautologies

Equality schemata

*A*(

*t*)!

*A*(e

*xA*(

*x*))

Predicate logic, such as System G

_{HP}-- 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 o**rigins 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.,

` 8

*x*9*yA*(*x*,*y*) 8*n*: `*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**

*L*EC:

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

*L*PC:

There are two Quantifiers: 8, 9

**Language of the Epsilon Calculus**

*L*e:

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*t*1, . . . ,*tn*

are semi-terms,

*f*(*t*1, . . . ,*tn*) is a semi-term.
5. If

*P*is a predicate symbol with ar(*P*) =*n*> 0, and*t*1, . . . ,*tn*

are terms,

*P*(*t*1, . . . ,*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*), 8

*xA*(

*x*) and

9

*xA*(*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*), e*xA*(*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*(*t*1, . . .*tn*) is a semi-term, its immediate sub-semiterms
are

*t*1, . . . ,*tn*, and its immediate subterms are those
among

*t*1, . . . ,*tn*which are terms, plus the immediate
subterms of those among

*t*1, . . . ,*tn*which aren’t terms.
Its sub-semi-terms are

*f*(*t*1, . . . ,*tn*) and the sub-semi-terms
of

*t*1, . . . ,*tn*; its subterms are those of its sub-semi-terms
which are terms.

If

*P*(*t*1, . . . ,*tn*) is an atomic semi-formula, its immediate
sub-semi-terms are

*t*1, . . . ,*tn*. Its immediate sub-terms are
those among

*t*1, . . . ,*tn*which are terms, plus the immediate
sub-terms of those among

*t*1, . . . ,*tn*which aren’t terms. Its
sub-semi-terms are the sub-semi-terms of

*t*1, . . . ,*tn*.
If

*A*is a semi-formula of the form*B*^*C*,*B*_*C*,*B*!*C*, ¬*B*,
8

*xB*or 9*xB*, its immediate sub-semi-formulas and its
sub-semi-formulas are those of

*B*and*C*.
If e

*xA*(*x*) is an e-expression, its immediate sub(semi)
formulas and its sub(semi)formulas are those of

*A*(*x*).

An e-term e

*xA*(*x*) is*an*e*-MATRIX*if all
terms occurring in

*A*are free variables, each of which occurs
exactly once.

Denote e-matrices as e

*xA*(*x*;*a*1, . . . ,*ak*) where the variables*a*1, . . . ,

*ak*displayed are all the free variables occurring in it.

Two matrices e

*xA*(*x*;*a*1, . . . ,*ak*), e*xA*(*x*;*b*1, . . . ,*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 e

*xA*(*x*) there exists a unique
matrix e

*xA*(*x*;*a*1, . . . ,*ak*) and a unique sequence*t*1, . . . ,*tk*of
terms such that e

*xA*(*x*,*t*1, . . . ,*tk*) = e*xA*(*x*).
Example: e

*xA*(*s*, e|*y*{*B*z(*y*})

e

, e

*zC*(*x*,*t*))
Its matrix is: e

*xA*(*a*,*b*, e*zC*(*x*,*c*))
The matrix of e

*xA*(*x*) is obtained by replacing all immediate
subterms of e

*xA*(*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: 2

*X*×Mat×*X*<w !*X*so that for*S**X*, a matrix
e

*xA*(*x*;*a*1, . . . ,*an*) and*d*1, . . . ,*dn*2*S*, F(*S*, e*xA*(*x*;*a*1, . . . ,*an*), h*d*1, . . . ,*dn*i)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,*f*M 2 |M|
If ar(

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

*P*) =*n*> 0,*P*M |M|*n*

A

*variable assignment s*for M is a function*s*: FV !|M|.
We write

*s**c s*0 if*s*(*a*) =*s*0(*a*) for all free variables*a*other than*c*.

The

*value t*M,*s of a term t*and the*satisfaction relation*

M,

*s*|=*A*is defined by:
If

*a*is a free variable,*a*M,*s*=*s*(*a*).
If

*f*is a constant symbol,*f*M,*s*=*f*M.
If

*f*(*t*1, . . . ,*tn*) is a term, (*f*(*t*1, . . . ,*tn*))M,*s*=*f*M(*t*M,*s*

1 , . . . ,

*t*M,*s*

*n*).

If

*P*(*t*1, . . . ,*tn*) is an atomic formula, M,*s*|=*P*(*t*1, . . . ,*tn*)
iff h

*t*M,*s*

1 , . . . ,

*t*M,*s*

*n*i 2

*P*M.

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 9

*xA*(*x*) is a formula and*c*a free variable not in*A*(*x*),
M,

*s*|= 9*xA*(*x*) iff M,*s*0 |=*A*(*c*) for some*s*0*c s*.
If 8

*xA*(*x*) is a formula and*c*a free variable not in*A*(*x*),
M,

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

*e*is an e-term with matrix e*xA*(*x*;*a*1, . . . ,*an*) so that*e*=
e

*xA*(*x*;*t*1, . . . ,*tn*), and*X*= {

*d*2 |M| :M,

*s*0 |=

*A*(

*c*;

*t*1, . . . ,

*tn*),

*s*0

*c s*,

*s*0(

*c*) =

*d*},

*e*M,

*s*= FM(

*X*, e

*xA*(

*x*;

*a*1, . . . ,

*an*), h

*t*M,

*s*

1 , . . . ,

*t*M,*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*) ! 9

*xA*(

*x*)

8

*xA*(*x*) !*A*(*a*).
Any substitution instance of

*A*(

*a*)!

*A*(e

*xA*(

*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*A*1, . . . ,*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*A*1, . . . ,*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*!8

*xA*(

*x*)

*A*(

*a*)!

*B*` 9

*xA*(

*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*= e*xA*(*x*,*t*1, . . . ,*tn*)*e*M,

*s*= FM({

*d*2 |

*M*| :M,

*s*0 |=

*A*(

*c*;

*t*1, . . . ,

*tn*),

*s*0

*c s*0,

*s*0(

*c*) =

*d*})

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

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

*extensionality axiom*

8

*x*(*A*(*x*)$*B*(*x*))!e*xA*(*x*) = e*xB*(*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

9

*x*and 8*x*as follows:
9

*xA*(*x*) ,*A*(e*xA*(*x*))
8

*xA*(*x*) ,*A*(e*x*¬*A*(*x*))
Define

*A*e by:*x*e =

*x*,

*a*e =

*a*

[e

*xA*(*x*)]e = e*xA*(*x*)e*f*(

*t*1, . . . ,

*tn*)e =

*f*(

*t*e

1, . . . ,

*t*e*n*),

*P*(

*t*1, . . . ,

*tn*)e =

*P*(

*t*e

1, . . . ,

*t*e*n*).

(

*A*^*B*)e =*A*e ^*B*e, (*A*_*B*)e =*A*e _*B*e, (*A*!*B*)e =*A*e !*B*e,
(¬

*A*)e = ¬*A*e.
(9

*xA*(*x*))e =*A*e(e*xA*e(*x*)0).
(8

*xA*(*x*))e =*A*e(e*x*¬*A*e(*x*)0).
where

*A*e(*x*)0 is*A*e(*x*) with all variables bound by quantifiers or
e’s in

*A*e(*x*) renamed by new bound variables (to avoid collision
of bound variables when e

*xA*e(*x*) is substituted into*A*e(*x*) where*x*may be in the scope of a quantifier or epsilon binding a

variable occurring in

*A*e(*x*).**Embedding**PC

**in**ECe

**: Examples**

9

*x*(*P*(*x*) _ 8*yQ*(*y*))e =
= [

*P*(*x*)_8*yQ*(*y*)]e {*x*e*x*[*P*(*x*)_8*yQ*(*y*)]e}
[

*P*(*x*)_8*yQ*(*y*)]e =*P*(*x*)_*Q*(e|*y*¬{*Q*z (*y*})*e*1

)

=

*P*(*x*)_*Q*(e|*y*¬{*Q*z (*y*})*e*1

) {

*x*e*x*[*P*(*x*)_*Q*(e|*y*¬{*Q*z (*y*})*e*1

)]

| {z }

*e*2

}

=

*P*(e*x*[*P*(*x*)_*Q*(e|*y*¬{*Q*z (*y*})*e*1

)]

| {z }

*e*2

)_

*Q*(e|*y*¬{*Q*z (*y*})*e*1

)

[9

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

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

*yA*(*x*,*y*)]e =*A*(*x*, e|*yA*{(z*x*,*y*})*e*1(

*x*)

)

=

*A*(*x*, e|*yA*{(z*x*,*y*})*e*1(

*x*)

){

*x*e|*xA*(*x*, e{*z*z*A*(*x*,*z*)})*e*2

}

=

*A*(e|*xA*(*x*, e{*z*z*A*(*x*,*z*)})*e*2

, e

*yA*(e|*xA*(*x*, e{*z*z*A*(*x*,*z*)})*e*2

,

*y*)
| {z }

*e*1(

*e*2)

)

**Embedding**PC

**in**ECe

**(cont’d)**

**Prop.**If PCe `

*A,*ECe `

*A*e.

Translations of quantifier axioms provable from critical

formulas:

[

*A*(*t*)!9*xA*(*x*)]e =*A*e(*t*)!*A*e(e*xA*(*x*)e)
Suppose PCe `

*B*!*A*(*a*), and*a*does not occur in*B*. By IH, we
have a proof p in ECe of

*B*e !*A*(*a*)e.
Replacing

*a*everywhere
in p by e

*x*¬*A*(*x*) results in a proof of
[

*B*!8*xA*(*x*)]e =*B*e !*A*e(e*x*¬*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 9

*x*1 . . .9

*xnA*(

*x*1, . . . ,

*xn*)

is a purely existential formula containing only the bound

variables

*x*1, . . . ,*xn*, and
PCe ` 9

*x*1 . . .9*xnA*(*x*1, . . . ,*xn*),
there are terms

*ti j*such that
EC `

_

i

*A*(

*ti*1, . . . ,

*tin*).

**Second Epsilon Theorem.**If

*A*is an e-free formula and

PCe `

*A,*PC `*A*.

**Degree of an**e

**-Term**

deg(e

*xA*(*x*)) = 1 if*A*(*x*) contains no e-subterms.
If

*e*1, . . . ,*en*are all immediate e-subterms of*A*(*x*),
deg(e

*xA*(*x*)) = max{deg(*e*1), . . . ,deg(*en*)}+1.**Rank of an**e

**-Expression**

An e-expression

*e*is*subordinate*to e*xA*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

*e*1, . . . ,*en*are all the e-expressions subordinate to*e*,
rk(

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

Examples

*P*(e

*x*[

*P*(

*x*)_

*Q*(e|

*y*¬{

*Q*z (

*y*})

*e*1

)]

| {z }

*e*2

)_

*Q*(e|*y*¬{*Q*z (*y*})*e*1

)

deg(

*e*1) = 1, deg(*e*2) = 2
rk(

*e*1) = rk(*e*2) = 1*A*(e|

*xA*(

*x*, e{

*z*z

*A*(

*x*,

*z*)})

*e*2

, e

*yA*(e|*xA*(*x*, e{*z*z*A*(*x*,*z*)})*e*2

,

*y*)
| {z }

*e*1(

*e*2)

)

deg(

*e*2) = 1, deg(*e*1(*e*2)) = 2
rk(

*e*2) = 2, rk(*e*1(*e*2)) = 1

Rank of Critical Formulas and Derivations

Rank of a critical formula

*A*(*t*)!*A*(e*xA*(*x*)) is rk(e*xA*(*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,*E*e =*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 p

*e*

with end formula

*A*so that rk(p*e*) rk(p), deg(p*e*) deg(p) and*o*(p

*e*,rk(

*e*)) =

*o*(p,rk(

*e*))−1.

The First Epsilon Theorem: Main Lemma

*Proof.*Construct p

*e*as follows:

Suppose

*A*(*t*1) !*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

p

*i*`*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 p

*i*.

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

p

*i*`*A*(*ti*)!*E*,
and

p0 `

^

¬

*A*(*ti*)!*E*,
to get p

*e*`*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 p

*i*, 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*= e*xA*(*x*) would be a proper
subterm of itself, which is impossible.

If

*e*appears in another critical formula*B*(*s*)!*B*(e*yB*(*y*)), we
have three cases.

Case I

*Case*:

*e*occurs only in

*s*.

Replacing

*e*by*ti*results in a critical formula*B*(*s*0) !*B*(e

*yB*(

*y*)).

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

as the original formula.

Hence

*o*(p*i*,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 e*yB*(*y*).
In other words, the critical formula has the form

*B*0(

*s*0(

*e*),

*e*)!

*B*0(e

*yB*0(

*y*,

*e*),

*e*).

But then the e-term belonging to this critical formula

*e*0 = e

*yB*0(

*y*,

*e*) ,

is of higher degree than

*e*.
By our assumptions, this implies that rk(e

*yB*0(*y*,*e*)) < rk(*e*).
Replacing

*e*by*ti*results in a different critical formula*B*0(

*s*0(

*ti*),

*ti*)!

*B*0(e

*yB*0(

*y*,

*ti*),

*ti*) ,

belonging to the e-term e

*yB*0(*y*,*ti*) which has the same rank as*e*0 and hence a lower rank than

*e*itself.

Hence again

*o*(p*i*,rk(*e*)) =*o*(p,rk(*e*))−1.

Case III

*Case*:

*e*does contain

*s*or e

*yB*(

*y*).

Then

*e*is of the form*e*0(*s*) or*e*0(e*yB*(*y*)), and*B*(

*a*) is really of the form

*B*0(

*e*0(

*a*)) where

*e*0(

*a*) is an e-term

of the same rank as

*e*.
Then e

*yB*(*y*) has the form e*yB*0(*e*0(*y*)), to which the e-
expression

*e*0(*y*) is subordinated.
But then e

*yB*0(*e*0(*y*)) has higher rank than*e*0(*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*(p*e*,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*m*fold
application of the lemma results in a derivation p0 of rank

< rk(p).

The Extended First Epsilon Theorem

**Theorem.**

If 9

*x*1 . . .9*xkA*(*x*1, . . . ,*xk*) is a purely existential
formula containing only the bound variables

*x*1, . . . ,*xk*, and
PCe ` 9

*x*1 . . .9*xkA*(*x*1, . . . ,*xk*),
there are terms

*ti j*such that
EC `

_

i

*A*(

*ti*1, . . . ,

*tik*).

Consider proofs in PCe of 9

*x*1 . . .9*xkA*(*x*1, . . . ,*xk*), where*A*(

*a*1, . . . ,

*ak*) contains no bound variables.

Employing embedding we obtain a derivation p of

*A*(

*s*1, . . . ,

*sk*), where

*s*1, . . . ,

*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*(*s*1, . . . ,*sk*) may
contain e-terms.

Hence the first elimination step transform the end-formula

into a disjunction.

*A*(

*s*01, . . . ,

*s*0

*k*)_. . ._

*A*(

*sn*1, . . . ,

*snk*) .

The Second Epsilon Theorem

**Theorem.**

If

*A*is an e-free formula and PCe `*A,*PC `*A*.

Assume

*A*has the form
9

*x*8*y*9*zB*(*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*= 9

*x*8

*y*9

*zB*(

*x*,

*y*,

*z*).

If

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

*AH*

of

*A*is 9*x*9*zB*(*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*_9*yG*(*y*)
(n) :

*F*_*G*(*a*) `*F*_8*zG*(*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 `*A*e. Due to the Second Epsilon Theorem
we obtain ECe `

*A*e implies PCe `*A*.**Herbrand’s Theorem.**Assume

*A*= 9

*x*8

*y*9

*zB*(

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

*xA*(

*x*) be a

purely existential formula (possibly containing =). Then

PCe [Ax ` 9

*xA*(*x*) implies
EC[Ax `

_

i

*A*(

*ti*1, . . . ,

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

*A*e. Then there exists a tautology of

the form ^

*i*,

*j*

(

*Bi*(*t j*)!*Bi*(e*xBi*(*x*)))!*A*e . (3)
Thus as soon as the critical formulas

*Bi*(*t j*) !*Bi*(e*xBi*(*x*))
are known, we only need to verify that (3) is a tautology to

infer that

*A*e 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 S*0: 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*(e

*xP*(

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

*xP*(*x*).
Note that the critical axiom

*P*(*t*)!*P*(e*xP*(*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 ` 8

*x*9*yA*(*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 8*xA*(*x*,*f*(*x*)) holds.

Peano Arithmetic: Results

**Non-counter example interpretation.**Let

9

*x*8*y*9*zA*(*a*,*x*,*y*,*z*)
be deducible in PAe such that only the indicated free variable

*a*occurs.

Let 9

*x*9*zA*(*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 `*A*e.

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.

*Archive for*

*Mathematical Logic*, 41.

T. Arai. Epsilon substitution method for

*ID*1(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.

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

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

16.*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*,
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*9*th*

*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.*
## No comments:

## Post a Comment