简单类型论中的斯科伦化：逻辑与理论两种视角
计算机科学中的逻辑
2023-05-08 v1
摘要
Peter Andrews 于 1971 年提出了寻找简单类型论中斯科伦定理类比的问题。一个初步想法导向了一条仅对带选择公理的简单类型论有效的朴素规则，而一般情形直到十多年后才由 Dale Miller 解决。最近，我们与 Thérèse Hardin 和 Claude Kirchner 一起提出了一种新方法，针对简单类型论不同但等价的表述证明 Miller 定理的类比。在本文（不含新技术结果）中，我试图表明斯科伦化问题及其各种解的历史，体现了简单类型论上两种视角之间的张力：逻辑视角与理论视角。
引用
@article{arxiv.2305.03322,
title = {Skolemization in Simple Type Theory: the Logical and the Theoretical Points of View},
author = {Gilles Dowek},
journal= {arXiv preprint arXiv:2305.03322},
year = {2023}
}