[PTS-Seminars] Maria Osório Costa (University of Lisbon; University College London)

Logical bilateralism challenges the traditional concepts of logic by treating assertion and denial as independent, yet opposed, acts. While inizially devised to justify classical logic, its constructive variants show that both acts admit intuitionistic interpretations. In this talk, we develop this perspective by introducing a logic of incompatible proofs and refutations, BPR. The central idea is that, although proofs and refutations constitute distinct forms of constructive evidence, in some settings, such as mathematical reasoning, they should be incompatible: no statement should be both proved and refuted. Building on a natural-deduction presentation of BPR, we develop a bilateral sequent calculus and establish cut elimination, the subformula property, and consistency. We then explore BPR using base-extension semantics, establishing soundness and completeness and providing a purely semantic proof of the incompatibility between proofs and refutations. We conclude by discussing how the relationship between Wansing's 2Int and BPR mirrors that between Nelson's N4 and N3, and how BPR captures Nelson's intended behaviour of constructive negation. This talk is based on ongoing work with Carlos Olarte, Elaine Pimentel and Victor Barroso-Nascimento.