pith. sign in

arxiv: 2510.16763 · v2 · submitted 2025-10-19 · 💻 cs.LO

Bilateralism with incompatible proofs and refutations

Victor Barroso-Nascimento , Maria Os\'orio , Elaine Pimentel This is my paper

Pith reviewed 2026-05-18 06:45 UTC · model grok-4.3

classification 💻 cs.LO
keywords bilateralismnatural deductionbase-extension semanticsconstructive falsityintuitionistic logicproof normalisationepistemic reasoningincompatible proofs
0
0 comments X

The pith

A bilateral logic system ensures no formula can be both provable and refutable without contradiction.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper introduces a bilateral approach to logic where assertion and denial are treated as independent but opposing acts. It develops a natural deduction system that normalizes proofs and refutations while preventing both from applying to the same formula. A corresponding base-extension semantics enforces this incompatibility through explicit constructions and is shown to be sound and complete. This setup aligns refutations with constructive falsity, extending intuitionistic logic to better represent consistent epistemic reasoning such as in mathematics.

Core claim

The central discovery is a bilateral natural deduction calculus in which proofs and refutations are incompatible, formalized with normalisation, and equipped with a sound and complete base-extension semantics that requires constructions for both while excluding their joint occurrence for any formula, with the refutation rules corresponding directly to constructive falsity and thereby extending rather than revising intuitionistic logic.

What carries the argument

The base-extension semantics that enforces mutual exclusion of proofs and refutations for each formula while requiring explicit constructions for both.

If this is right

  • The system provides a framework for modelling epistemic entities like mathematical proofs and refutations that exclude inconsistency.
  • The refutation notion corresponds to constructive falsity, allowing the logic to extend intuitionistic logic.
  • The natural deduction system satisfies normalisation, ensuring desirable proof-theoretic properties.
  • The semantics is sound and complete with respect to the calculus, validating the incompatibility claim.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • If the incompatibility is enforced this way, similar bilateral systems could be developed for other connectives or modal operators to model more complex epistemic states.
  • This might connect to applications in computer science for verifying consistency in knowledge bases or reasoning systems.
  • Extending the correspondence to other constructive falsity notions could broaden its use in paraconsistent reasoning.

Load-bearing premise

A base-extension semantics exists that demands explicit constructions for both proofs and refutations while strictly preventing both from being established for the same formula, and this semantics is sound and complete relative to the natural deduction rules.

What would settle it

A specific formula for which both a proof and a refutation can be derived in the natural deduction system without deriving a contradiction, or a base where the semantics assigns both a proof and a refutation to the same formula.

Figures

Figures reproduced from arXiv: 2510.16763 by Elaine Pimentel, Maria Os\'orio, Victor Barroso-Nascimento.

Figure 1
Figure 1. Figure 1: System BPR 5 [PITH_FULL_IMAGE:figures/full_fig_p005_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: Proper (proof) reductions 26 [PITH_FULL_IMAGE:figures/full_fig_p026_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: Proper (dual proof) reductions 27 [PITH_FULL_IMAGE:figures/full_fig_p027_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: Permutative reductions. 28 [PITH_FULL_IMAGE:figures/full_fig_p028_4.png] view at source ↗
read the original 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 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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 2 minor

Summary. The paper develops a bilateral natural deduction system in which proofs and refutations are mutually incompatible for any formula. It establishes normalisation for the calculus, introduces a base-extension semantics requiring explicit constructions of both proofs and refutations while enforcing their exclusion, proves soundness and completeness of the semantics with respect to the rules, and claims an exact correspondence between its refutation rules and David Nelson's constructive falsity (~), thereby extending rather than revising intuitionistic logic for constructive epistemic reasoning.

Significance. If the central claims hold, the work strengthens constructive bilateralism by supplying a framework that models epistemic entities with explicit positive and negative evidence under a consistency constraint. The normalisation result and the base-extension semantics provide proof-theoretic and semantic foundations that align with Nelson's strong negation, offering a bridge to existing literature on constructive falsity without altering the underlying intuitionistic connectives.

major comments (2)
  1. [§4.3] §4.3 (refutation rules for implication and disjunction): the claimed exact match to Nelson's clauses ~ (A → B) ≡ A ∧ ~B and ~ (A ∨ B) ≡ ~A ∧ ~B is load-bearing for the 'extends rather than revises' thesis, yet the paper supplies only schematic rules without a connective-by-connective derivation or counter-example check showing that refutation of A → B cannot be obtained from refutation of B alone; this gap directly affects whether the correspondence holds without hidden adjustments.
  2. [§5] §5 (soundness and completeness proofs): the base-extension semantics is asserted to be sound and complete, but the argument for the refutation direction relies on the same rule correspondence that is under-specified in §4.3; without an explicit induction that preserves the Nelson-style polarity for every connective, the completeness claim for the full language remains unverified.
minor comments (2)
  1. [§2] Notation for the bilateral turnstile and the refutation operator could be introduced earlier and used consistently to improve readability.
  2. [§3] The normalisation theorem is stated but the reduction steps for the new bilateral rules are only sketched; a short appendix with the critical cases would aid verification.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the careful reading and constructive comments on our manuscript. We address each major comment below and will revise the paper to incorporate additional explicit details where needed.

read point-by-point responses

  1. Referee: [§4.3] §4.3 (refutation rules for implication and disjunction): the claimed exact match to Nelson's clauses ~ (A → B) ≡ A ∧ ~B and ~ (A ∨ B) ≡ ~A ∧ ~B is load-bearing for the 'extends rather than revises' thesis, yet the paper supplies only schematic rules without a connective-by-connective derivation or counter-example check showing that refutation of A → B cannot be obtained from refutation of B alone; this gap directly affects whether the correspondence holds without hidden adjustments.

    Authors: We agree that making the correspondence fully explicit strengthens the argument for the 'extends rather than revises' claim. The refutation rules in §4.3 are deliberately schematic to mirror Nelson's clauses for constructive falsity directly. In the revised version we will add a short subsection (or expanded paragraph) in §4.3 that supplies a connective-by-connective derivation together with a brief counter-example verification: for instance, we will show that a refutation of B alone does not yield a refutation of A → B without an assertion of A, and likewise for the disjunction case. This addition will confirm that no hidden adjustments to the intuitionistic connectives are required. revision: yes

  2. Referee: [§5] §5 (soundness and completeness proofs): the base-extension semantics is asserted to be sound and complete, but the argument for the refutation direction relies on the same rule correspondence that is under-specified in §4.3; without an explicit induction that preserves the Nelson-style polarity for every connective, the completeness claim for the full language remains unverified.

    Authors: The soundness and completeness arguments in §5 are already carried out by induction on formula structure, with separate cases for proofs and refutations that preserve Nelson-style polarity. To meet the referee's request for explicit verification, we will expand the completeness proof in the revision to display the full inductive step for each connective, paying particular attention to the refutation cases for implication and disjunction. This will make transparent that the base-extension semantics is complete with respect to the rules while maintaining the exact correspondence to constructive falsity. revision: yes

Circularity Check

0 steps flagged

No significant circularity; derivations rely on independent proof-theoretic constructions and external Nelson reference

full rationale

The paper defines a bilateral natural deduction calculus with explicit rules for proofs and refutations, proves normalisation directly from the rules, introduces a base-extension semantics that enforces mutual exclusion by construction of the semantic clauses, and establishes soundness/completeness via standard induction. The correspondence to Nelson's constructive falsity is shown by exhibiting a translation between the refutation rules and Nelson's strong negation clauses, which are external (1949). No step reduces a claimed result to a fitted parameter or self-citation chain; the system is self-contained against the stated semantics and external benchmark. Minor background citations to bilateralism literature are not load-bearing for the central claims.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The paper relies on standard background assumptions from intuitionistic logic and bilateralism; no free parameters, new invented entities, or ad-hoc axioms are mentioned in the abstract.

axioms (1)
  • domain assumption Intuitionistic logic provides the underlying setting that is extended rather than revised
    The abstract states that the system extends rather than revises intuitionistic logic.

pith-pipeline@v0.9.0 · 5679 in / 1307 out tokens · 40549 ms · 2026-05-18T06:45:25.023216+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

What do these tags mean?
matches
The paper's claim is directly supported by a theorem in the formal canon.
supports
The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends
The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses
The paper appears to rely on the theorem as machinery.
contradicts
The paper's claim conflicts with a theorem or certificate in the canon.
unclear
Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Reference graph

Works this paper leans on

25 extracted references · 25 canonical work pages

  1. [1]

    A cut-free sequent calculus for the bi-intuitionistic logic 2int, 2020

    Sara Ayhan. A cut-free sequent calculus for the bi-intuitionistic logic 2int, 2020

    work page 2020

  2. [2]

    Bilateral base-extension se- mantics, 2025

    Victor Barroso-Nascimento and Maria Os´ orio Costa. Bilateral base-extension se- mantics, 2025. Arxiv preprint. https://arxiv.org/abs/2505.01593

    work page arXiv 2025

  3. [3]

    An ecu- menical view of proof-theoretic semantics.Synthese, 206(197), 2025

    Victor Barroso-Nascimento, Luiz Carlos Pereira, and Elaine Pimentel. An ecu- menical view of proof-theoretic semantics.Synthese, 206(197), 2025

    work page 2025

  4. [4]

    Bilateralism in proof-theoretic semantics.J

    Nissim Francez. Bilateralism in proof-theoretic semantics.J. of Philosophical Logic, 43(2):239–259, 2014

    work page 2014

  5. [5]

    Kripke completeness of first-order constructive logics with strong negation.Logic Journal of the IGPL, 11(6):615–646, 2003

    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

    work page 2003

  6. [6]

    Nelson algebras, resid- uated lattices and rough sets: A survey.J

    Jouni J¨ arvinen, S´ andor Radeleczki, and Umberto Rivieccio. Nelson algebras, resid- uated lattices and rough sets: A survey.J. Appl. Non Class. Logics, 34(2-3):368– 428, 2024

    work page 2024

  7. [7]

    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

    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

    work page 2009

  8. [8]

    Nel- son’s logic s.Logic Journal of the IGPL, 28(6):1182–1206, 2020

    Thiago Nascimento, Umberto Rivieccio, Jo˜ ao Marcos, and Matthew Spinks. Nel- son’s logic s.Logic Journal of the IGPL, 28(6):1182–1206, 2020

    work page 2020

  9. [9]

    Logical ecumenism, 2018

    Victor Nascimento. Logical ecumenism, 2018. Master’s Dissertation

    work page 2018

  10. [10]

    Constructible falsity.The Journal of Symbolic Logic, 14(1):16–26, 1949

    David Nelson. Constructible falsity.The Journal of Symbolic Logic, 14(1):16–26, 1949

    work page 1949

  11. [11]

    Negation and separation of concepts in constructive systems

    David Nelson. Negation and separation of concepts in constructive systems. In Arend Heyting, editor,Constructivity in Mathematics, pages 205–225, Amsterdam,

    work page

  12. [12]

    Strong negation is definable in 2int, 2025

    Hrafn Valt?r Oddsson. Strong negation is definable in 2int, 2025

    work page 2025

  13. [13]

    Dordrecht, Nether- land, 2008

    Sergei Odintsov.Constructive Negations and Paraconsistency. Dordrecht, Nether- land, 2008

    work page 2008

  14. [14]

    An ecumenical notion of entailment.Synthese, 198(22-S):5391–5413, 2021

    Elaine Pimentel, Luiz Carlos Pereira, and Valeria de Paiva. An ecumenical notion of entailment.Synthese, 198(22-S):5391–5413, 2021

    work page 2021

  15. [15]

    Dover Publications, 1965

    Dag Prawitz.Natural Deduction: A Proof-Theoretical Study. Dover Publications, 1965

    work page 1965

  16. [16]

    Dover Publications, 2006

    Dag Prawitz.Natural deduction: A proof-theoretical study. Dover Publications, 2006

    work page 2006

  17. [17]

    Classical versus intuitionistic logic

    Dag Prawitz. Classical versus intuitionistic logic. In Bruno Lopes Edward Her- mann Haeusler, Wagner de Campos Sanz, editor,Why is this a Proof ?, Festschrift for Luiz Carlos Pereira, volume 27, pages 15–32. College Publications, 2015

    work page 2015

  18. [18]

    I. Rumfitt. Yes and no.Mind, 109(436):781–823, 2000

    work page 2000

  19. [19]

    Base-extension semantics for intuitionistic sentential logic.Logic J

    Tor Sandqvist. Base-extension semantics for intuitionistic sentential logic.Logic J. of the IGPL, 23(5):719–731, 2015

    work page 2015

  20. [20]

    Uniform proof-theoretic semantics for logical constants (abstract).Journal of Symbolic Logic, 56:1142, 1991

    Peter Schroeder-Heister. Uniform proof-theoretic semantics for logical constants (abstract).Journal of Symbolic Logic, 56:1142, 1991

    work page 1991

  21. [21]

    Validity concepts in proof-theoretic semantics.Synthese, 148(3):525–571, 2006

    Peter Schroeder-Heister. Validity concepts in proof-theoretic semantics.Synthese, 148(3):525–571, 2006

    work page 2006

  22. [22]

    Proof-Theoretic Semantics

    Peter Schroeder-Heister. Proof-Theoretic Semantics. In Edward N. Zalta and Uri Nodelman, editors,The Stanford Encyclopedia of Philosophy. Metaphysics Re- search Lab, Stanford University, Winter 2022 edition, 2022

    work page 2022

  23. [23]

    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

    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. 20

    work page 2005

  24. [24]

    Falsification, natural deduction and bi-intuitionistic logic.Jour- nal of Logic and Computation, 26(1):425–450, 07 2013

    Heinrich Wansing. Falsification, natural deduction and bi-intuitionistic logic.Jour- nal of Logic and Computation, 26(1):425–450, 07 2013

    work page 2013

  25. [25]

    A more general general proof theory.J

    Heinrich Wansing. A more general general proof theory.J. Appl. Log., 25:23–46, 2017. 21 A Proof of some selected results A.1 Proofs from Section 3 Proof (of Lemma 1).We prove the result by induction on the complexity value ⟨d, n⟩ofΠ, showing that, if it is not the case thatd=n= 0, thenΠreduces to a deductionΠ ′ which has complexity value⟨d ′, n′⟩for⟨d ′, ...

    work page 2017