Agda康托尔定理 (4-1)

目录

Agda康托尔定理 ▹

前置知识 ▹

康托尔定理（直接证） ▹

Lawvere不动点定理 ▹

存在不可数集合 ▹

康托尔定理(用Lawvere不动点定理证） ▹

延伸阅读 ▹

Agda康托尔定理

康托尔定理是集合论中的一个基本定理, 它断言任何集合都不能满射到它的幂集. 本文将在原味Agda中证明这个定理, 这将说明它也是构造主义成立的.

前置知识

我们假设读者熟悉原味 Agda 以及标准库中的以下概念:

open import Data.Bool using (Bool; true; false; not)

open import Data.Empty using (⊥)

open import Data.Nat using (ℕ; suc)

open import duct using (∃-syntax; _×_; _,_; proj₁; proj₂)

open import Function using (id; _$_)

open import Level using (Level)

open import Relation.Nullary using (¬_)

open import Relation.positionalEquality using (_≡_; refl; sym; subst; cong-app)

我们约定用A 和 B 表示任意宇宙的任意集合. 由CH同构, 它们也可以表示命题.

variable

ℓ ℓ′ : Level

A B : Set ℓ

A 的幂集定义为 A 到集合宇宙 Set 的函数 A → Set, 记作 ℙ A.

ℙ : Set ℓ → Set _

ℙ A = A → Set

我们说A 与 B 逻辑等价, 记作 A ↔ B, 当且仅当 A 蕴含 B 且 B 蕴含 A.

infix 2 _↔_

_↔_ : Set ℓ → Set ℓ′ → Set _

A ↔ B = (A → B) × (B → A)

逻辑等价是自反关系.

↔-refl : A ↔ A

↔-refl = id , id

相等的命题逻辑等价.

≡→↔ : A ≡ B → (A ↔ B)

≡→↔ refl = ↔-refl

任意命题不等价于自身的否定.

A↮¬A : ¬ (A ↔ ¬ A)

A↮¬A (p , q) = p (q (λ x → p x x)) (q λ x → p x x)

我们说A 到 B 的函数 f : A → B 是满射, 当且仅当对任意 b : B, 存在 a : A 使得 f a ≡ b.

surjective : (f : A → B) → Set _

surjective f = ∀ b → ∃[ a ] f a ≡ b

康托尔定理 (直接证)

数学联邦政治世界观提示您：看后求收藏（同人小说网http://tongren.me），接着再看更方便。