On anticut rules: classical, FDE-based and intuitionistic logics

Abstract

In this paper, we investigate certain intricacies and peculiarities of the proof

theory of deduction-refutation systems (D-R systems, henceforth), namely systems integrating

theorems and antitheorems of a given logic. Our primary focus is on establishing

the general conditions under which anticut rules (the contrapositive versions of the familiar

cut rule) can be eliminated from D-R sequent calculi, while distinguishing between

two main variants of these systems. This is a topic that has recently been highlighted in

the context of D-R sequent calculi for first-degree entailment-based logics. Finally,

we examine the relationship between anticut rules and the completeness of D-R sequent

calculi with respect to deducibility and refutability (Ł-completeness).