数学联邦政治世界观
超小超大

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),接着再看更方便。

相关小说

梦断南宫 连载中
梦断南宫
梦境之旅_
生命只有一次,又或许平行世界有无数次。一诺的妈妈会在另个世界依旧陪伴一诺吗?
13.4万字9个月前
停摆的钟 连载中
停摆的钟
芋香忧
在不同的时空里的我,总是想念第一次遇见的我们,如果给我一次机会,我会奋不顾身握住我们的未来,,,
0.8万字9个月前
我莫名多了九个师兄 连载中
我莫名多了九个师兄
白了个云
母亲被抓,莫名多了九个师兄,还都是一方霸主死亡转世原因渐渐浮出水面背后阴谋尽然是...(主爽文,进度快,想法很多)
4.5万字9个月前
青丘狐狸顾烟萝 连载中
青丘狐狸顾烟萝
吕凤伦
我本是一卷空白的书,他们都叫我无字天书。有一天,我的主人经过再三考虑,便在我的身上写了天机两个字。字体是甲骨文。从此以后我又叫《天机》。我本......
23.7万字9个月前
潜执(有刀有甜) 连载中
潜执(有刀有甜)
温柔的执法
潜执校园篇,甜文
0.4万字9个月前
绝世女君:魂归妖女倾绝天下 连载中
绝世女君:魂归妖女倾绝天下
醋鱼a
2.8万字9个月前