一句话：提出区分肯定/否定与强/经典四模态的经典命题逻辑保守扩张，并给出自然演绎、Kripke语义与项赋值系统。
该文研究经典命题逻辑的一个保守扩张，其核心是区分四种陈述模态：命题可被肯定或否定，且可为强命题或经典命题。强命题的证明在某种意义上必须是构造性的，而经典命题的证明可借助反证法。系统采用自然演绎风格，作者证明其相对一个 Kripke 语义是可靠且完备的。随后从命题即类型对应出发，给出项赋值系统，并证明归约的合流性；强规范化证明通过翻译到带 Mendler 式递归的 System F 来完成。该工作为同时容纳构造性证明与经典证明/反驳的逻辑提供了统一的证明论与类型论框架。
We study a conservative extension of classical propositional logic distinguishing between four modes of statement: a proposition may be affirmed or denied, and it may be strong or classical. Proofs of strong propositions must be constructive in some sense, whereas proofs of classical propositions proceed by contradiction. The system, in natural deduction style, is shown to be sound and complete with respect to a Kripke semantics. We develop the system from the perspective of the propositions-as-types correspondence by deriving a term assignment system with confluent reduction. The proof of strong normalization relies on a translation to System F with Mendler-style recursion.
DOI 原文 ·
@inproceedings{paperbot6229,
title = {A Constructive Logic with Classical Proofs and Refutations},
author = {Pablo Barenbaum and Teodoro Freund},
booktitle = {LICS},
year = {2021},
doi = {10.1109/lics52264.2021.9470649}
}