多态性与二阶逻辑的顽固循环性：受害者的故事
逻辑
2018-04-30 v1 计算机科学中的逻辑
摘要
关于高阶类型理论及相关的参数化多态概念的研究，构成了二阶及更高阶逻辑循环性（或非直谓性）这一古老基础问题的技术对应物。然而，此类研究及其常非平凡结果的认识论意义，在当代基础论争中未受足够重视。本文回顾的结果表明，二阶逻辑循环性问题不能简化为对恶性循环的简单判定。通过比较 Frege 为 Grundgesetze 逻辑系统（被罗素悖论证明不一致）与 Martin-Löf 为带所有类型之类型的直觉类型论（被 Girard 悖论证明不一致）所给出的错误一致性论证，以及二阶类型理论（或系统 F）的规范化论证，我们指出了隐藏在危险的直谓量化观念背后的一簇微妙数学问题与逻辑概念，它们构成了一个广阔（且很大程度上未被探索）的基础研究领域。
引用
@article{arxiv.1710.10205,
title = {Polymorphism and the obstinate circularity of second order logic: a victims' tale},
author = {Paolo Pistone},
journal= {arXiv preprint arXiv:1710.10205},
year = {2018}
}