2026/01/22 by Sara Ayhan · 1 voice · 1 citation
Computer Science · Psychology · #Logic, Reasoning, and Knowledge #Logic, programming, and type systems #Philosophy and Theoretical Science
paper · doi:10.1017/s1755020326101063
openalex publication_date 2026/01/22 · openalex created_date 2026/01/23 · openalex updated_date 2026/06/23
Abstract This paper investigates the negation-free fragment of the bi-connexive logic 2C , called 2C Subscript minus - <mml:math xmlns:xlink="http://www.w3.org/1999/xlink" xmlns:mnf="http://cambridge.org/core/manifest" xmlns:cup="http://contentservices.cambridge.org" xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:m="http://cambridge.org/core/metadata" xmlns:core="http://cambridge.org/core" xmlns:c="http://cambridge.org/core/content" display="inline"> <mml:msub> <mml:mi/> <mml:mo>−</mml:mo> </mml:msub> </mml:math> , 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 λ <mml:math xmlns:xlink="http://www.w3.org/1999/xlink" xmlns:mnf="http://cambridge.org/core/manifest" xmlns:cup="http://contentservices.cambridge.org" xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:m="http://cambridge.org/core/metadata" xmlns:core="http://cambridge.org/core" xmlns:c="http://cambridge.org/core/content" display="inline"> <mml:mi>λ</mml:mi> </mml:math> -calculus.