DROPS

Document

DOI: 10.4230/LIPIcs.MFCS.2026.16

Bilateralism with Incompatible Proofs and Refutations

Authors: Victor Barroso-Nascimento, Maria Osório, and Elaine Pimentel

Published in: LIPIcs, Volume 386, 51st International Symposium on Mathematical Foundations of Computer Science (MFCS 2026)

Abstract

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.

Cite as

Victor Barroso-Nascimento, Maria Osório, and Elaine Pimentel. Bilateralism with Incompatible Proofs and Refutations. In 51st International Symposium on Mathematical Foundations of Computer Science (MFCS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 386, pp. 16:1-16:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{barrosonascimento_et_al:LIPIcs.MFCS.2026.16,
  author =	{Barroso-Nascimento, Victor and Os\'{o}rio, Maria and Pimentel, Elaine},
  title =	{{Bilateralism with Incompatible Proofs and Refutations}},
  booktitle =	{51st International Symposium on Mathematical Foundations of Computer Science (MFCS 2026)},
  pages =	{16:1--16:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-442-0},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{386},
  editor =	{Kouck\'{y}, Michal and Petrișan, Daniela},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2026.16},
  URN =		{urn:nbn:de:0030-drops-273974},
  doi =		{10.4230/LIPIcs.MFCS.2026.16},
  annote =	{Keywords: Proofs and refutations, Constructive falsity, Natural deduction, Logical bilateralism, Base-extension semantics}
}

Search Results

Documents authored by Barroso-Nascimento, Victor

Bilateralism with Incompatible Proofs and Refutations

Abstract

Cite as

Thanks for your feedback!

Could not send message