Russell 悖论在类型论中的一种朴素编码
逻辑
2026-01-06 v1 计算机科学中的逻辑
摘要
Russell 悖论是最容易理解的na"ive 集合论不一致之处。本文提出一种直接将 Russell 悖论编码到类型论中的方法，运用类型-类型宇宙、sigma 类型以及任一等位或内涵等位（UIP）实现。
引用
@article{arxiv.2601.00811,
title = {A Naive Encoding of Russell's Paradox in Type Theory},
author = {Zhuoyuan Qu},
journal= {arXiv preprint arXiv:2601.00811},
year = {2026}
}