arnold beckmann's pages
Corrected Upper Bounds for Free-Cut Elimination
Author: Arnold Beckmann and Sam Buss
Title: Corrected Upper Bounds for Free-Cut Elimination
Journal: TCS 2011, 412(39): 5433-5445
The paper corrects earlier upper bounds on the size of free-cut
elimination. Free-cut elimination allows cut elimination to be carried
out in the presence of non-logical axioms. The correction requires
that the notion of a free-cut be modified so that a cut formula is
anchored provided that all of its introductions are anchored, instead
of only requiring that one of its introductions is anchored. With the
correction, the originally proved size upper bounds remain unchanged.
These results also apply to partial cut elimination. We also apply
these bounds to elimination of cuts in propositional logic.
If the non-logical inferences are closed under cut and infer only
atomic formulas, then all cuts can be eliminated. This generalizes
earlier results of Takeuti and of Negri and van Plato.