Contradictions Without Negation and a Proof-Theoretic, Bilateralist Account of Connexive Logics

Abstract This paper investigates the negation-free fragment of the bi-connexive logic 2C, called 2C Subscript minus _- −, from the perspective of bilateralist proof-theoretic semantics (PTS). It is argued that eliminating primitive negation has two important conceptual consequences. First, it requires a reconceptualization of contradictory logics: in a bilateralist framework, contradiction need not be understood in terms of negation inconsistency, but rather as the coexistence of proofs and refutations for certain formulas within a non-trivial system. Second, it challenges the standard definition of connexive logics, which typically rely on negation-based schemata. Instead, a rule-based conception of connexivity, grounded in bilateralist PTS, is proposed. This reconception avoids dependence on the validation of specific formula schemata and thereby also dependence on negation. The paper also addresses the issue of proof–refutation duality in the absence of strong negation, which can be formalized and recovered at a meta-level by extending the system with a two-sorted typed lamda λ -calculus.