A Naive Encoding of Russell's Paradox in Type Theory

TL;DR

This paper presents a straightforward encoding of Russell's paradox within type theory using universe, sigma types, and identity types, highlighting the paradox's implications for type-theoretic consistency.

Contribution

It introduces a direct encoding of Russell's paradox in type theory with universe and identity types, exploring its impact on type-theoretic foundations.

Findings

Encoding demonstrates inconsistency issues in naive type theory

Uses universe, sigma types, and identity types for encoding

Highlights implications for type-theoretic foundations

Abstract

Russell's paradox is the most easily understandable way to illustrate the inconsistency of na\"ive 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).