命题逻辑弱规范化的简化证明

中文摘要 AI 辅助

我们提出了直觉主义自然演绎中弱规范化的一个新证明。该证明的显著特点在于，它仅处理割（cut）而非割段（cut segments），提供了明确的局部规则来确定是收缩整个证明还是归约其某个子证明，并且在后者情况下，确定应归约哪个子证明。我们还讨论了在Lean中形式化整个证明的过程，并提出了一个确定性的弱规范化算法。

英文摘要

We present new proofs of weak normalization for intuitionistic and classical propositional logics (with the full set of operators -- falsum, implication, conjunction and disjunction). These proofs work with cuts rather than cut segments, and they provide explicit ``local'' rules for determining whether to contract a whole proof or reduce one of its subproofs, and in the latter case, which subproof to reduce. Interestingly, much of the complication in the case of intuitionistic logic is due to the disjunction elimination rule, while our version of the same rule for classical logic has falsum as conclusion always, and so is much easier to handle. All the complication in the case of classical logic shifts to cuts involving the reductio ad absurdum rule. We also discuss a formalization of the entire proof in Lean, and present a deterministic algorithm for weak normalization.

发表机构

• Chennai Mathematical Institute（钦奈数学研究所）

机构由 AI 辅助整理，请以论文原文为准。