Bilateral Labeled Sequent Calculi

Abstract

This paper 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 paper concludes with some observations on systems related to C, such as C3 and N4, and outlines potential directions for future work.