Bilateralism with incompatible proofs and refutations
Fuente:
arXiv
Salvato in:
| Autori principali: | , , |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2025
|
| Soggetti: | |
| Accesso online: | |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866910186509172736 |
|---|---|
| author | Barroso-Nascimento, Victor Osório, Maria Pimentel, Elaine |
| author_facet | Barroso-Nascimento, Victor Osório, Maria Pimentel, Elaine |
| contents | 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 epistemic entities, such as mathematical proofs and refutations, that exclude inconsistency.
The logic is formalised through a bilateral natural deduction system with desirable proof-theoretic properties, including normalisation. We also introduce a base-extension semantics requiring explicit constructions of proofs and refutations while preventing them from being established for the same formula. The semantics is proven sound and complete with respect to the calculus. Finally, we show that our notion of refutation corresponds to David Nelson's constructive falsity, extending rather than revising intuitionistic logic and reinforcing the system's suitability for representing constructive epistemic reasoning. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2510_16763 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Bilateralism with incompatible proofs and refutations Barroso-Nascimento, Victor Osório, Maria Pimentel, Elaine Logic in Computer Science 03F03, 00A30 F.3; F.4 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 epistemic entities, such as mathematical proofs and refutations, that exclude inconsistency. The logic is formalised through a bilateral natural deduction system with desirable proof-theoretic properties, including normalisation. We also introduce a base-extension semantics requiring explicit constructions of proofs and refutations while preventing them from being established for the same formula. The semantics is proven sound and complete with respect to the calculus. Finally, we show that our notion of refutation corresponds to David Nelson's constructive falsity, extending rather than revising intuitionistic logic and reinforcing the system's suitability for representing constructive epistemic reasoning. |
| title | Bilateralism with incompatible proofs and refutations |
| topic | Logic in Computer Science 03F03, 00A30 F.3; F.4 |
| url | https://arxiv.org/abs/2510.16763 |