2026-08-21T18:34:57Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:27397 2026-08-21T14:42:38Z ddc:004 open_access

Bilateralism with Incompatible Proofs and Refutations Barroso-Nascimento, Victor Osório, Maria Pimentel, Elaine Proofs and refutations Constructive falsity Natural deduction Logical bilateralism Base-extension semantics Logical bilateralism challenges traditional concepts of logic by treating assertion and denial as independent yet opposed acts. While initially devised to justify classical logic, its constructive variants show that both acts admit intuitionistic interpretations. This paper presents a bilateral system where a formula cannot be both provable and refutable without contradiction, offering a framework for modelling mathematical proofs and refutations that exclude inconsistency. We formalise the logic via a bilateral natural deduction system with the desirable proof-theoretic properties of normalisation, subformula property and consistency, together with a base-extension semantics grounded in explicit proofs and refutations. Finally, refutation is shown to coincide with Nelson’s constructive falsity, extending intuitionistic logic for constructive epistemic reasoning. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Victor Barroso-Nascimento and Maria Osório and Elaine Pimentel 2026 Is Part Of LIPIcs, Volume 386, 51st International Symposium on Mathematical Foundations of Computer Science (MFCS 2026) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.MFCS.2026.16 urn:nbn:de:0030-drops-273974 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2026.16 eng https://creativecommons.org/licenses/by/4.0/legalcode