Document Open Access Logo

Bilateralism with Incompatible Proofs and Refutations

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

PDF

File

Thumbnail PDF
PDF
LIPIcs.MFCS.2026.16.pdf
  • Filesize: 0.8 MB
  • 18 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Proof theory
  • Theory of computation → Constructive mathematics
  • Theory of computation → Logic and verification
Keywords
  • Proofs and refutations
  • Constructive falsity
  • Natural deduction
  • Logical bilateralism
  • Base-extension semantics

Metrics

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 Get BibTex

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) https://doi.org/10.4230/LIPIcs.MFCS.2026.16

Author Details

Victor Barroso-Nascimento
  • Department of Computer Science, University College London, UK
Maria Osório
  • Faculty of Sciences, University of Lisbon, Portugal
Elaine Pimentel
  • Department of Computer Science, University College London, UK

Funding

Pimentel and Barroso-Nascimento are supported by the Leverhulme Trust grant RPG-2024-196 and by the European Union’s Horizon Europe research and innovation programme under the Marie Skłodowska-Curie Staff Exchanges action, grant agreement No 101299559 (SemPER).
  • Osório, Maria: Osório is supported by the Portuguese Foundation for Science and Technology grant 2024.00633.BD.

References

  1. Sara Ayhan and Heinrich Wansing. On synonymy in proof-theoretic semantics: The case of 2Int. Bulletin of the Section of Logic, 52:50, July 2023. URL: https://doi.org/10.18778/0138-0680.2023.18.
  2. Victor Barroso-Nascimento and Maria Osório. Bilateral base-extension semantics. Journal of Philosophical Logic, 2026. URL: https://doi.org/10.1007/s10992-026-09855-5.
  3. Victor Barroso-Nascimento, Luiz Carlos Pereira, and Elaine Pimentel. An ecumenical view of proof-theoretic semantics. Synthese, 206(4):197-206, 2025. URL: https://doi.org/10.1007/s11229-025-05269-z.
  4. Marcello D'Agostino, Dov Gabbay, and Sanjay Modgil. Normality, non-contamination and logical depth in classical natural deduction. Studia Logica: An International Journal for Symbolic Logic, 108(2):291-357, 2020. URL: https://doi.org/10.1007/S11225-019-09847-4.
  5. Antonio Piccolomini d'Aragona. A comparison of three kinds of monotonic proof-theoretic semantics and the base-incompleteness of intuitionistic logic. J. Log. Comput., 35(8), 2025. URL: https://doi.org/10.1093/LOGCOM/EXAF062.
  6. Pedro del Valle-Inclan. Harmony and normalisation in bilateral logic. Bulletin of the Section of Logic, 52(3):377-409, 2023. URL: https://doi.org/10.18778/0138-0680.2023.14.
  7. Fernando Ferreira. The co-ordination principles: A problem for bilateralism. Mind, 117(468):1051-1057, October 2008. URL: https://doi.org/10.1093/mind/fzn036.
  8. Nissim Francez. Bilateralism in proof-theoretic semantics. J. of Philosophical Logic, 43(2):239-259, 2014. URL: https://doi.org/10.1007/s10992-012-9261-3.
  9. Nissim Francez. Bilateralism does provide a proof theoretic treatment of classical logic (for non-technical reasons). Journal of Applied Logics: The ifCoLog Journal of Logics and Their Applications, 5(8):1653-1662, 2018. Reply to Gabbay’s "Bilateralism does not provide a proof theoretic treatment of classical logic (for technical reasons)". URL: https://www.collegepublications.co.uk/downloads/ifcolog00028.pdf.
  10. Dov M. Gabbay. Intuitionistic basis for non-monotonic logic. In D. W. Loveland, editor, 6th Conference on Automated Deduction, pages 260-273, Berlin, Heidelberg, 1982. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/BFb0000064.
  11. Michael Gabbay. Bilateralism does not provide a proof theoretic treatment of classical logic (for technical reasons). Journal of Applied Logic, 25:108-122, 2017. URL: https://doi.org/10.1016/j.jal.2017.11.001.
  12. Rajeev Goré. Dual intuitionistic logic revisited. In Roy Dyckhoff, editor, Automated Reasoning with Analytic Tableaux and Related Methods, International Conference, TABLEAUX 2000, St Andrews, Scotland, UK, July 3-7, 2000, Proceedings, Lecture Notes in Computer Science, pages 252-267. Springer, 2000. URL: https://doi.org/10.1007/10722086_21.
  13. Yuri Gurevich. Intuitionistic logic with strong negation. Studia Logica, 36:49-59, 1977. URL: https://doi.org/10.1007/BF02121114.
  14. Ichiro Hasuo and Ryo Kashima. Kripke completeness of first-order constructive logics with strong negation. Logic Journal of the IGPL, 11(6):615-646, 2003. URL: https://doi.org/10.1093/jigpal/11.6.615.
  15. Jouni Järvinen, Sándor Radeleczki, and Umberto Rivieccio. Nelson algebras, residuated lattices and rough sets: A survey. J. Appl. Non Class. Logics, 34(2-3):368-428, 2024. URL: https://doi.org/10.1080/11663081.2024.2336386.
  16. Norihiro Kamide and Sara Negri. Unified natural deduction for logics of strong negation. Notre Dame Journal of Formal Logic, 66, 2025. URL: https://doi.org/10.1215/00294527-2025-0016.
  17. Andreas Kapsner. Logics and Falsifications: A New Perspective on Constructivist Semantics. Springer, Cham, Switzerland, 2014. Google Scholar
  18. Nils Kürbis. Some comments on Ian Rumfitt’s bilateralism. Journal of Philosophical Logic, 45(6):623-644, 2016. URL: https://doi.org/10.1007/s10992-016-9395-9.
  19. Nils Kürbis. Proof and Falsity: A Logical Investigation. Cambridge University Press, Cambridge, UK, 2019. Google Scholar
  20. Nils Kürbis. Normalisation for bilateral classical logic with some philosophical remarks. FLAP, 8(2):531-556, 2021. URL: https://collegepublications.co.uk/ifcolog/?00044.
  21. Nils Kürbis and Yaroslav Petrukhin. Normalisation for some quite interesting many-valued logics. Logic and Logical Philosophy, 30(3):493-534, 2021. URL: https://doi.org/10.12775/LLP.2021.009.
  22. George Metcalfe. A sequent calculus for constructive logic with strong negation as a substructural logic. Bulletin of the Section of Logic, 38(1/2):1-7, 2009. Google Scholar
  23. Thiago Nascimento, Umberto Rivieccio, João Marcos, and Matthew Spinks. Nelson’s logic s. Logic Journal of the IGPL, 28(6):1182-1206, 2020. URL: https://doi.org/10.1093/jigpal/jzaa015.
  24. David Nelson. Constructible falsity. The Journal of Symbolic Logic, 14(1):16-26, 1949. URL: https://doi.org/10.2307/2268973.
  25. David Nelson. Negation and separation of concepts in constructive systems. In Arend Heyting, editor, Constructivity in Mathematics, pages 205-225, Amsterdam, 1959. North-Hollan. Google Scholar
  26. Hrafn Valtýr Oddsson. Strong negation is definable in 2int, 2025. URL: https://arxiv.org/abs/2501.13979.
  27. Sergei Odintsov. Constructive Negations and Paraconsistency. Trends in Logic. Springer Dordrecht, Dordrecht, Netherland, 2008. URL: https://doi.org/10.1007/978-1-4020-6867-6.
  28. Dag Prawitz. Natural Deduction: A Proof-Theoretical Study. Dover Publications, 1965. Google Scholar
  29. Cecylia Rauszer and C Rauszer. An algebraic and Kripke-style approach to a certain extension of intuitionistic logic, volume 167. Państwowe Wydawnictwo Naukowe, 1980. Google Scholar
  30. Ian Rumfitt. Yes and no. Mind, 109(436):781-823, 2000. URL: https://doi.org/10.1093/mind/109.436.781.
  31. Tor Sandqvist. Base-extension semantics for intuitionistic sentential logic. Logic J. of the IGPL, 23(5):719-731, 2015. URL: https://doi.org/10.1093/jigpal/jzv021.
  32. Katsuhiko Sano and Masanobu Toyooka. Cut-free sequent calculi for Wansing’s expansions of Nelson’s logics. Studia Logica, 2025. URL: https://doi.org/10.1007/s11225-025-10210-z.
  33. Peter Schroeder-Heister. Uniform proof-theoretic semantics for logical constants (abstract). Journal of Symbolic Logic, 56:1142, 1991. Google Scholar
  34. Peter Schroeder-Heister. Validity concepts in proof-theoretic semantics. Synthese, 148(3):525-571, 2006. URL: https://doi.org/10.1007/s11229-004-6296-1.
  35. Peter Schroeder-Heister. Proof-Theoretic Semantics. In Edward N. Zalta and Uri Nodelman, editors, The Stanford Encyclopedia of Philosophy. Metaphysics Research Lab, Stanford University, Winter 2022 edition, 2022. URL: https://plato.stanford.edu/archives/win2022/entries/proof-theoretic-semantics/.
  36. Yaroslav Shramko. Dual intuitionistic logic and a variety of negations: The logic of scientific research. Studia Logica: An International Journal for Symbolic Logic, 80(2/3):347-367, 2005. URL: https://doi.org/10.1007/S11225-005-8474-7.
  37. Ryan Simonelli. A general schema for bilateral proof rules. J. Philos. Log., 53(3):623-656, 2024. URL: https://doi.org/10.1007/S10992-024-09743-W.
  38. Ryan Simonelli. "yes," "no," neither, and both. Synthese, 207, January 2026. URL: https://doi.org/10.1007/s11229-025-05385-w.
  39. Heinrich Wansing. Semantics-based nonmonotonic inference. Notre Dame Journal of Formal Logic, 36(1):44-54, 1995. URL: https://doi.org/10.1305/ndjfl/1040308828.
  40. Heinrich Wansing. Displaying the modal logic of consistency. J. Symb. Log., 64(4):1573-1590, 1999. URL: https://doi.org/10.2307/2586798.
  41. Heinrich Wansing. Falsification, natural deduction and bi-intuitionistic logic. Journal of Logic and Computation, 26(1):425-450, July 2013. URL: https://doi.org/10.1093/logcom/ext035.
  42. Heinrich Wansing. A more general general proof theory. J. Appl. Log., 25:23-46, 2017. URL: https://doi.org/10.1016/J.JAL.2017.01.002.
  43. Peter Schroeder-Heister Will Stafford, Thomas Piecha. Logics of proof-theoretic validity. Topoi, 2025. URL: https://doi.org/10.1007/s11245-025-10248-7.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact