くるるの数学ノート このページをアンテナに追加 RSSフィード

2014-07-13

[][] |2^N|>|N|

まあすでにやっている人は多いと思いますが、昨日突然思いついて、自然数の集合が非可算個あることをCoqで証明してみました。

Require Import Arith. 

Definition diag (F : nat -> (nat -> bool)) (n : nat) : bool := negb (F n n). 

Theorem nat_to_nat_uncountable : forall (F : nat -> (nat -> bool)), 
exists (g : nat -> bool), forall (n : nat), F n <> g.  
Proof.
intro F.
exists (diag F). 
intro n. 
intro H. 
absurd (F n n = diag F n).
unfold diag.
intro H1.
destruct (F n n).
inversion H1.
inversion H1. 
rewrite H. reflexivity. 
Qed. 

Software Foundations読んでいる途中なので、できるだけautoとかは使わずに書いてしまっています。

なんでこんなことをやろうと思い立ったかというと、「CSの人は記述可能な関数しか存在しないと思っている、少なくともコンピュータの世界はそれで終わると思っているのではないか」という思い込みがあって、それに対して「そんなことないよな、定理証明器とか非可算な世界も扱っちゃっているよな」ということを小難しく考えていたら、いきなり「そんな難しいこと考えなくても世界最古の非可算集合存在証明がそのまま実行できるじゃん!」と思い立ってしまったと。今考えてみると、前記の思い込みは思いっきり藁人形だった気もします。

それとも、ある立場の人はこの証明を見ても nat -> bool が非可算であるとは思わずに、nat -> (nat -> bool)という型では列挙が記述できないと思うだけなんでしょうか?その辺りの感性はよくわかりません。

まあとりあえずできちゃったんで置いておきます。

2013-01-18

2013年01月18日のツイート

2013-01-17

2013年01月17日のツイート

2013-01-12

2013年01月12日のツイート

2013-01-07

2013年01月07日のツイート