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.

翻译：逻辑双边主义通过将断定和否定视为独立但对立的行为，挑战了传统的逻辑概念。虽然最初旨在证成经典逻辑，但其构造性变体表明，这两种行为均可接受直觉主义解释。本文提出一个双边系统，其中任一公式不能既被证明又被反驳而不导致矛盾，从而为建模排除不一致性的认知实体（如数学证明与反驳）提供框架。该逻辑通过具有理想证明论性质（包括归一化）的双边自然演绎系统形式化。我们还引入一种基础扩展语义，要求对证明和反驳进行显式构造，同时阻止它们为同一公式建立。该语义被证明相对于演算是可靠且完备的。最后，我们表明我们的反驳概念对应于大卫·尼尔森的构造性虚假，这扩展了而非修正了直觉主义逻辑，并增强了该系统对于表示构造性认知推理的适用性。