Tautology Elimination, Cut Elimination and S4?

Abstract

The paper “Tautology elimination, cut elimination, and S5” published in this journal presents a novel method for establishing by proof analysis the admissibility of the rule of tautology elimination for certain sequent calculi. Since tautology elimination will typically imply the admissibility of cut, the method promises a new path to show the admissibility of cut for cut-free calculi on which the standard techniques within structural proof theory seem inapplicable. This paper shows that the method as presented involves an error.