Abstract

This paper deals with predicate logics involving two truth values (here referred to as bivalent logics). Sequent calculi for these logics rely on a general notion of sequent that helps to make the principles of excluded middle and non-contradiction explicit. Several formulations of the redundancy of cut are possible in these sequent calculi. Indeed, four different forms of cut can be distinguished. I prove that only two of them hold for positive sequent calculus (which is both paraconsistent and paracomplete) while all of them hold for classical sequent calculus. As for complete and consistent sequent calculi (which are respectively paraconsistent and paracomplete), I prove that they only admit one form of cut in addition to the two that hold for positive sequent calculus