Talks and Poster Presentations (without Proceedings-Entry):
M. Baaz:
"LKepsilon and the immediate reduction of arbitrary cuts to universal cuts";
Talk: Helmut Veith Memorial Workshop,
Obergurgl (invited);
2017-02-01.
English abstract:
An Epsilon companion of a LK Derivation is an LK-Epsilon proof where both the end sequent and the cuts consist of Epsilon-Translation of first-order formulas. We show, that any LK-Derivation can be translated into an Epsilon companion with only universal cuts with exponential increase of complexity. This demonstrates, that Schütte-Tait Elimination procedures are incompatible with the First Epsilon Theorem, we discuss many additional implications.
Created from the Publication Database of the Vienna University of Technology.