Agda康托尔定理 (4-2)

定理 (Cantor) 不存在 A 到其幂集 ℙ A 的满射 f : A → ℙ A.

_ : (f : A → ℙ A) → surjective f → ⊥

证明 假设存在这样的 f, 构造子集 S : A → Set = λ x → ¬ f x x, 或者用传统符号表达即

S＝{x ∈ A|x ∉ f(x) }

由于f 是满射, 存在 a : A 使得 eq : f a ≡ S.

用cong-app 对 eq 两边同时运用 a 得到 f a a ≡ ¬ f a a, 即

α ∈ f(α) ↔ α ∉ f(α)

矛盾 ∎

_ = λ f H → let (a , eq) = H (λ x → ¬ f x x) in

A↮¬A $ ≡→↔ $ cong-app eq a

这种证法也叫对角线证法, 哥德尔不完备定理以及停机定理的证明都具有类似的形式. 以下是它们的一般化.

Lawvere不动点定理

定理 (Lawvere) 如果存在 A 到 A → B 的满射 f : A → A → B, 那么任意 g : B → B 都有不动点 b : B 使得 g b ≡ b.

Lawvere : (f : A → A → B) → surjective f → (g : B → B) → ∃[ b ] g b ≡ b

证明 留作练习 (提示: 将 g 看作对康托尔定理证明中出现的 ¬_ 的一般化) ∎

Lawvere f H g = let (a , eq) = H (λ x → g (f x x)) in

f a a , subst (λ h → g (f a a) ≡ h a) (sym eq) refl

存在不可数集合

令Lawvere 中的 g 为布尔值的否定函数 not 立即可知 𝔹ℕ 不可数, 因为 not 没有不动点.

2^ℕ-uncountable : (f : ℕ → ℕ → Bool) → surjective f → ⊥

2^ℕ-uncountable f H with Lawvere f H not

... | true , ()

... | false , ()

令Lawvere 中的 g 为自然数的后继函数 suc 立即可知 ℕℕ 不可数, 因为 suc 没有不动点.

ℕ^ℕ-uncountable : (f : ℕ → ℕ → ℕ) → surjective f → ⊥

ℕ^ℕ-uncountable f H with Lawvere f H suc

... | (_ , ())

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

令Lawvere 中的 g 为命题的否定函数 ¬_ 立即可知 A 不能满射到 ℙ A, 因为 ¬_ 没有不动点, 否则与 A↮¬A 矛盾.

Cantor : (f : A → ℙ A) → surjective f → ⊥

Cantor f H = A↮¬A $ ≡→↔ $ sym $ proj₂ $ Lawvere f H ¬_

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