直觉主义一阶逻辑：基于 Curry-Howard 同构的范畴语义
逻辑
2013-07-02 v1 计算机科学中的逻辑
摘要
本文介绍了一种针对一阶直觉主义逻辑的新型可靠且完备的语义，该语义建立在范畴论框架之上，并基于所谓的 Curry-Howard 同构对逻辑进行计算解释。此外，还推导出了相应 lambda-演算的可靠且完备的语义。这种语义在某种程度上扩展了由 Heyting 范畴、topos 论解释以及 Kripke 模型所给出的更传统的含义。引入这种新语义的理由在于其“无点”（point-free）特性，即不存在用于解释逻辑项的元素宇宙。换言之，项并不指代某个集合中的个体，而是指代将语句解释维系在一起的“粘合剂”，这与形式拓扑中的情况类似。由于所提出的语义可以平凡地扩展至所有基于直觉主义系统的一阶逻辑理论（并且在适当注意下也可扩展至极小系统），因此该语义涵盖了所有谓词理论，尽管应当指出这些理论的一些特殊方面。
引用
@article{arxiv.1307.0108,
title = {Intuitionistic First-Order Logic: Categorical Semantics via the Curry-Howard Isomorphism},
author = {Marco Benini},
journal= {arXiv preprint arXiv:1307.0108},
year = {2013}
}
备注
92 pages