Sufficient conditions for first-order-based sequent calculi to admit cut elimination by a Schütte–Tait style cut elimination proof are established. The worst case complexity of the cut elimination is analysed. The obtained upper bound is parameterized by a quantity related to the calculus. The conditions are general enough to be satisfied by a wide class of sequent calculi encompassing, among others, some sequent calculi presentations for the first order and the propositional versions of classical and intuitionistic logic, classical and intuitionistic modal (...) logic S4, and classical and intuitionistic linear logic and some of its fragments. Moreover the conditions are such that there is an algorithm for checking if they are satisfied by a sequent calculus. (shrink)

The implicational fragment of the logic of relevant implication, $R_{\to}$ is one of the oldest relevance logics and in 1959 was shown by Kripke to be decidable. The proof is based on $LR_{\to}$ , a Gentzen-style calculus. In this paper, we add the truth constant $\mathbf{t}$ to $LR_{\to}$ , but more importantly we show how to reshape the sequent calculus as a consecution calculus containing a binary structural connective, in which permutation is replaced by two structural rules that involve $\mathbf{t}$ (...) . This calculus, $LT_\to^{\text{\textcircled{$\mathbf{t}$}}}$ , extends the consecution calculus $LT_{\to}^{\mathbf{t}}$ formalizing the implicational fragment of ticket entailment . We introduce two other new calculi as alternative formulations of $R_{\to}^{\mathbf{t}}$ . For each new calculus, we prove the cut theorem as well as the equivalence to the original Hilbert-style axiomatization of $R_{\to}^{\mathbf{t}}$ . These results serve as a basis for our positive solution to the long open problem of the decidability of $T_{\to}$ , which we present in another paper. (shrink)

Cut-elimination theorems constitute one of the most important classes of theorems of proof theory. Since Gentzen’s proof of the cut-elimination theorem for the system LK, several other proofs have been proposed. Even though the techniques of these proofs can be modified to sequent systems other than $$\textbf{LK}$$, they are essentially of a very particular nature; each of them describes an algorithm to transform a given proof to a cut-free proof. However, due to its reliance on heavy syntactic arguments and case (...) distinctions, such an algorithm makes the fundamental structure of the argument rather opaque. We, therefore, consider rules abstractly, within the framework of logical structures familiar from universal logic in the sense of Béziau (Universal logic, Prague, 1994) and aim to clarify the essence of the so-called “elimination theorems”. To do this, we first give a non-algorithmic proof of the cut-elimination theorem for the propositional fragment of $$\textbf{LK}$$. From this proof, we abstract the essential features of the argument and define something called normal sequent structures relative to a particular rule. We then prove a version of the rule-elimination theorem for these. Abstracting even more, we define abstract sequent structures and show that for these structures, the corresponding version of the rule-elimination theorem has a converse as well. (shrink)