高阶逻辑的拓扑完备性
逻辑
2023-03-31 v1 范畴论
摘要
利用拓扑斯理论中的近期结果，我们证明两个高阶逻辑系统关于拓扑空间上的层模型（即所谓“拓扑语义”）是完备的。第一个是经典高阶逻辑，带有限高类型的关涉量化；第二个是其一个谓词片段，带类型间函数的量化，但不带任意关系的量化。第二个定理对直觉主义逻辑与经典逻辑均适用。
引用
@article{arxiv.math/9707206,
title = {Topological Completeness for Higher-Order Logic},
author = {Steve Awodey and Carsten Butz},
journal= {arXiv preprint arXiv:math/9707206},
year = {2023}
}