Bilateral Labeled Sequent Calculi

This article investigates the proof theory of contra-classical logics, with a focus on Heinrich Wansing’s constructive connexive logic C. Drawing on Wansing’s semantic bilateral framework—which characterizes connectives in terms of support of truth and support of falsity—we introduce a bilateral labeled sequent calculus incorporating specific verification and falsification rules. The resulting calculus is shown to exhibit key structural properties: All logical rules are height-preserving invertible, all structural rules are height-preserving admissible, and the cut rule is admissible. Moreover, the system, proven to be both sound and complete, allows for terminating proof search and the extraction of countermodels from failed root-first proof search. Finally, the computational complexity of the resulting decision procedure is established. The article concludes with some observations on systems related to C, such as C3 and N4, and outlines potential directions for future work.