经典、直觉主义与一致可证明性之间的对应关系
计算机科学中的逻辑
2016-08-31 v1
摘要
基于对所用推理规则的分析,我们刻画了经典可证明性蕴含直觉主义可证明性的情形。随后我们考察这些可推导性概念与一致可证明性(直觉主义可证明性的一种限制,体现了一种特殊形式的目标导向性)之间的关系。我们首先确定了前述关系蕴含后者的条件。利用这一结果,我们识别出经典逻辑与直觉主义逻辑中所谓抽象逻辑程序设计语言的最丰富版本。接着我们研究通过向假设集添加待证公式的否定,将经典可证明性以及由此衍生的直觉主义可证明性归约为一致可证明性。我们此处的重点在于理解实现这种归约的情境。然而,我们的讨论指出了基于该归约的证明过程的结构,此问题亦在别处被显式探讨。
引用
@article{arxiv.cs/9809015,
title = {Correspondences between Classical, Intuitionistic and Uniform Provability},
author = {Gopalan Nadathur},
journal= {arXiv preprint arXiv:cs/9809015},
year = {2016}
}
备注
31 pages