关于 Herbrand 构造逻辑的自然演绎 I：Dummett 逻辑 LC 的 Curry-Howard 对应
计算机科学中的逻辑
2019-03-14 v2
摘要
Dummett 逻辑 LC 是直觉主义逻辑加上 Dummett 公理的扩展：对于任意两个命题，第一个蕴含第二个，或者第二个蕴含第一个。我们给出一阶与二阶 Dummett 逻辑的自然演绎和 Curry-Howard 对应。我们在 lambda 演算中加入了一个算子，从编程的角度来看，它代表了一种表示并行计算及其间通信的机制；从逻辑的角度来看，它代表了 Dummett 公理。我们证明了我们的类型化演算是可规范化的，并表明存在量化公式的证明项可归约为构成 Herbrand 析取的个体项列表。
引用
@article{arxiv.1609.03190,
title = {On Natural Deduction for Herbrand Constructive Logics I: Curry-Howard Correspondence for Dummett's Logic LC},
author = {Federico Aschieri},
journal= {arXiv preprint arXiv:1609.03190},
year = {2019}
}