Venue: Meeting room #1 on the 5th floor, Building #9, Waseda University

Speaker:
Kenji Miyamoto (University of Innsbruck, [email protected])

Title:
The epsilon calculus with equality predicate and Herbrand complexity

Abstract:
Hilbert's epsilon-calculus is based on an extension of the language of
predicate logic by a term-forming operator $\varepsilon$ [1].  Two
fundamental results about the epsilon-calculus, the first and second
epsilon theorem, play a role similar to that which the cut-elimination
theorem plays in sequent calculus.  In particular, Herbrand's Theorem
is a consequence of the epsilon theorems.  Moser and Zach study the
epsilon theorems and the complexity of the elimination procedure
underlying their proof, as well as the length of Herbrand disjunctions
of existential theorems obtained by this elimination procedure [2].
We extend their results to epsilon-calculus with equality predicate.
This is joint work with Georg Moser.

[1] D. Hilbert and P. Bernays,
Grundlagen der Mathematik, vol. 2, Springer Berlin, 1939.
[2] G. Moser and R. Zach,
The epsilon calculus and Herbrand complexity,
Studia Logica, vol. 82 (2006), no. 1, pp. 133--155.