集合论与类型论序数相吻合
计算机科学中的逻辑
2023-08-15 v3 逻辑
摘要
在构造性集合论中，序数是遗传传递集。在同伦类型论（HoTT）中，序数是具有传递、良基且外延的二元关系的类型。我们表明，若使用（Aczel构造性集合论到类型论解释的HoTT精炼）Aczel解释，则两定义等价。此后，我们推广类型论序数概念以捕获Aczel解释中的所有集合而非仅序数。这导出一类自然的有序结构，其包含类型论序数并实现集合论的高阶归纳解释。我们所有结果均在Agda中形式化。
引用
@article{arxiv.2301.10696,
title = {Set-Theoretic and Type-Theoretic Ordinals Coincide},
author = {Tom de Jong and Nicolai Kraus and Fredrik Nordvall Forsberg and Chuangjie Xu},
journal= {arXiv preprint arXiv:2301.10696},
year = {2023}
}
备注
v2: Minor changes. To appear at LICS'23. v3: Acknowledgments updated