Mario Piazza, Andrea Sabatini

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

Introduction

On anticut rules: classical, fde-based and intuitionistic logics. Explore anticut rules in deduction-refutation (D-R) systems for classical, FDE-based, and intuitionistic logics. Investigate conditions for anticut elimination and their relation to Ł-completeness.

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

Full Text

Comments

You need to be logged in to post a comment.