Preprint:
Arnold Beckmann and Samuel R. Buss.
"Corrected Upper Bounds for Free-Cut Elimination."
Theoretical Computer Science 412, 39 (2011) 5433-5445.
Download manuscript: PDF.
Abstract:
Free-cut elimination
allows cut elimination to be carried out in the presence of
non-logical axioms.
Formulas in a proof are anchored provided they originate in a
non-logical axiom or non-logical inference.
This paper corrects and strengthens earlier upper bounds
on the size of free-cut elimination.
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 extends
earlier results of Takeuti and of Negri and von Plato.