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.
翻译:我们研究传统理论逻辑的保守延伸,区分了四种表述方式:一种主张可以被肯定或否定,也可以是强烈的或古典的。 强烈主张的证明必须具有某种意义上的建设性,而传统主张的证明则是自相矛盾的。 从自然推理的风格来看,这个制度对Kripke语义学来说是健全和完整的。 我们从主张的类式对应的角度来发展这个制度,方法是引出一个术语分配制度,并减少共性。 强烈正常化的证据取决于对Mendler式递归的系统F的翻译。