弗雷格的类型理论
历史与综述
2023-12-27 v3 计算机科学中的逻辑
摘要
常有人认为，弗雷格在《Grundgesetze der Arithmetik》中提出的函数层级理论预示了丘奇简单类型论底层的类型层级。这一主张大致是说，弗雷格在《Grundgesetze》的说明性语言中预设了简单类型论意义上的函数类型。然而，这种观点难以容纳双自变量函数名并将函数视为不完全实体。我提出并辩护了一种对《Grundgesetze》中一级函数名的替代解释，将其解释为简单类型论的开项而非函数类型的闭项。这一解释提供了一种虽非历史但仍更忠实的弗雷格层级理论的类型论近似，并可自然扩展以容纳二级函数。其可能性基于两个关键观察：弗雷格的罗马标记本质上表现为开项，且弗雷格缺乏区分罗马标记与函数名的清晰判据。
引用
@article{arxiv.2006.16453,
title = {Frege's theory of types},
author = {Bruno Bentzen},
journal= {arXiv preprint arXiv:2006.16453},
year = {2023}
}