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.

翻译：逻辑双边主义通过将断言与否定视为独立而对立的行为，对传统逻辑概念提出了挑战。尽管最初旨在为经典逻辑提供辩护，但其构造性变体表明这两种行为均可容纳直觉主义解释。本文提出一个双边系统，其中公式不能在不产生矛盾的情况下同时可证明与可反驳，从而为建模排除不一致性的认知实体（如数学证明与反驳）提供了框架。该逻辑通过具有良好证明论性质（包括正规化）的双边自然演绎系统形式化。我们还引入了一种基础扩展语义学，要求显式构造证明与反驳，同时防止对同一公式同时建立两者。该语义学被证明相对于演算系统具有可靠性与完备性。最后，我们证明本文的反驳概念对应于大卫·尼尔森的构造性假值，这是对直觉主义逻辑的扩展而非修正，从而强化了该系统在表征构造性认知推理方面的适用性。