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

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

相关小说

蓝天画的冷漠 连载中
蓝天画的冷漠
浅心夏
[情之所绊,心之所想,浅夏之歌,唯爱再受]她蓝天画(莫灵画)三年再次见面,却变得冷漠无情,他东方末三年再次见面,他爱上了别人,他洛小熠三年之......
3.1万字8个月前
穿越兽世做大厨 连载中
穿越兽世做大厨
彗星糯米团
人间百味,百味俱全。夏子悠的最大爱好就是研究美食,谁知在山里寻觅食材时一不小心就穿到了兽人满地跑的兽世,只是如雌性坐拥遍地美男这类事都只是传......
25.9万字8个月前
高级化妆师 连载中
高级化妆师
李小莫
假期更,谨慎进入!谨慎进入!谨慎进入!勿上升正主!!剧情虚构!!
0.2万字8个月前
记录我的梦境 连载中
记录我的梦境
荼靡茶香
记梦到的东西
0.0万字8个月前
心机绿茶上位记 连载中
心机绿茶上位记
江非予z薄筠
简介正在更新
2.9万字8个月前
omega上司有点甜 连载中
omega上司有点甜
阿音爱写文
【已签约】禁止抄袭转载。一次意外,谢凛分化成了s级alpha,没过几天,就有一个自称幽久所负责人的家伙邀请他入伙。作为中二少年的他,听多了神......
14.8万字8个月前