Saved in:
| Main Author: | |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | https://arxiv.org/abs/2601.00811 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866909980127395840 |
|---|---|
| author | Qu, Zhuoyuan |
| author_facet | Qu, Zhuoyuan |
| contents | Russell's paradox is the most easily understandable way to illustrate the inconsistency of naïve set theory. This note proposes a direct encoding of Russell's paradox with type-in-type universe, sigma types, and either extensional identity or intensional identity with the uniqueness of identity proofs (UIP). |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2601_00811 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | A Naive Encoding of Russell's Paradox in Type Theory Qu, Zhuoyuan Logic Logic in Computer Science Russell's paradox is the most easily understandable way to illustrate the inconsistency of naïve set theory. This note proposes a direct encoding of Russell's paradox with type-in-type universe, sigma types, and either extensional identity or intensional identity with the uniqueness of identity proofs (UIP). |
| title | A Naive Encoding of Russell's Paradox in Type Theory |
| topic | Logic Logic in Computer Science |
| url | https://arxiv.org/abs/2601.00811 |