Correspondence of Contradictions in the Constructive Connexive Calculus C

The calculus C was introduced by H. Wansing as a constructive logic with strong negation. In addition, C validates the theses of connexive logic that are attributed to Aristotle and Boethius. A further remarkable property of C is that it is a non-trivial but negation inconsistent system: it has a formula and its negation as theorems. From a bilateralist-minded perspective, such a contradiction can be seen as the existence of both a verification and a falsification of one and the same formula. Relatedly, it has been noted by Wansing that there seems to be a kind of correspondence between these two types of derivations when it comes to a proof of contradiction. Following this observation, we attempt in this paper to introduce a precise notion for such a correspondence. We thence establish that this correspondence obtains in propositional and first-order versions of C, via formulations of suitable sequent and tableau calculi.