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

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

相关小说

小世界——灵魂快穿 连载中
小世界——灵魂快穿
逝桉
0.3万字9个月前
卿如许 连载中
卿如许
唯梦闲人不梦卿
诈尸了又,最近会陆陆续续更一些,也会对之前的一些做一些修改。总的来说世界观会变得更大然后人物会变多,主线以卿安(长卿)的视角写,在其故事中未......
2.8万字9个月前
王秋儿和王冬儿穿越凤逆天下 连载中
王秋儿和王冬儿穿越凤逆天下
泪无翼
弃坑慎入
5.1万字9个月前
斗龙战士神之审判 连载中
斗龙战士神之审判
四月落雪
熠诺末画凯曼熠诺玄幻小说禁止抄袭,抄袭可耻
3.2万字9个月前
宠妻上瘾,帝尊大大不要啊 连载中
宠妻上瘾,帝尊大大不要啊
银河柒分甜
这人很懒,啥都没写。
12.7万字9个月前
尸兄篇 连载中
尸兄篇
晰昕
[已签约]本人原创,创作非常渣
20.6万字9个月前