对罗素式分支类型理论的构造性考察
逻辑
2017-04-25 v1 范畴论
摘要
本文考察了分支类型层级到具有无穷序列宇宙的Martin-Löf类型理论中的自然解释。我们表明，在这种谓词性解释下，罗素可归约公理的一些有用特例是有效的，即函数可归约性。这足以使类型层级可用于构造性数学的发展。我们提出了一种适合此目的的分支类型理论。可以将本文的结果视为罗素理论问题的一个替代解决方案，它避免了非谓词性，而是采用了构造性逻辑。这里引入的直觉主义分支类型理论也表明存在一个自然关联的谓词性初等拓扑斯概念。
引用
@article{arxiv.1704.06812,
title = {A Constructive Examination of a Russell-style Ramified Type Theory},
author = {Erik Palmgren},
journal= {arXiv preprint arXiv:1704.06812},
year = {2017}
}
备注
14 pages