一句话：为 Dummett 逻辑 LC 建立一阶与二阶自然演绎及 Curry-Howard 对应，并证明其类型化演算可规范化并导出 Herbrand 析取。
Dummett 逻辑 LC 是在直觉主义逻辑上加入 Dummett 公理（任意两命题必有其一蕴涵另一）而得到的逻辑。本文为一阶和二阶 Dummett 逻辑给出自然演绎系统与 Curry-Howard 对应。作者在 lambda 演算中增加一个算子：编程上表示并行计算及通信机制，逻辑上对应 Dummett 公理。文章证明所得类型化演算具有规范化性质，并进一步说明存在量化公式的证明项可归约为由个体项列表构成的 Herbrand 析取。该工作为 Herbrand 构造逻辑系列研究奠定基础。
Dummett's logic LC is intuitionistic logic extended with Dummett's axiom: for every two statements the first implies the second or the second implies the first. We present a natural deduction and a Curry-Howard correspondence for first-order and second-order Dummett's logic. We add to the lambda calculus an operator which represents, from the viewpoint of programming, a mechanism for representing parallel computations and communication between them, and from the viewpoint of logic, Dummett's axiom. We prove that our typed calculus is normalizing and show that proof terms for existentially quantified formulas reduce to a list of individual terms forming an Herbrand disjunction.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{Aschieri16,
title = {On Natural Deduction for Herbrand Constructive Logics I: Curry-Howard Correspondence for Dummett's Logic LC},
author = {Federico Aschieri},
journal = {Logical Methods in Computer Science},
volume = {Volume 12, Issue 3},
year = {2017},
doi = {10.2168/lmcs-12(3:13)2016}
}