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

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).