关于 Herbrand 构造逻辑的自然演绎 II：一阶逻辑与算术中 Markov 原理的 Curry-Howard 对应
计算机科学中的逻辑
2018-11-13 v2 逻辑
摘要
正如 Herbelin 所示，以受限形式的 Markov 原理扩展的直觉主义一阶逻辑是构造性的，并且允许 Curry-Howard 对应。我们提供了该结果的一个更简单的证明，然后研究了以不受限的 Markov 原理扩展的直觉主义一阶逻辑。从经典自然演绎出发，我们限制了排中律，获得了该逻辑的一个自然演绎系统和一个并行 Curry-Howard 同构。我们证明，存在量词公式的证明项可归约为一个代表所有可能见证的个体项列表。作为推论，我们得出该逻辑是 Herbrand 构造性的：每当它证明某个存在公式时，它也证明了该公式的一个 Herbrand 析取。最后，使用刚刚引入的技术，我们还提供了带有 Markov 原理的算术的一种新的计算解释。
引用
@article{arxiv.1612.05457,
title = {On Natural Deduction for Herbrand Constructive Logics II: Curry-Howard Correspondence for Markov's Principle in First-Order Logic and Arithmetic},
author = {Federico Aschieri and Matteo Manighetti},
journal= {arXiv preprint arXiv:1612.05457},
year = {2018}
}