Posted at

ペアノの公理の後者をうっかり2つに増やすと実数になっちゃう説

Haskellで下記のデータ型を定義した時にBinat -> Nat型の単射な関数が思いつかず、タイトルの仮説が浮かんだ次第。

data Nat = Zero | Succ Nat

data Binat = Bizero | LSucc Binat | RSucc Binat


なんでそう思ったかの概略

証明する気はないが、なんで実数(とBinat型のすべての値の集合の濃度が同じ)と思ったか、概略を述べておく。

まず、LSuccRSuccBizeroに有限回適用して得られる値の集合$B_0$は可算無限集合。

次に、RSuccは有限回、LSuccは可算無限回Bizeroに適用して得られる値の集合$B_1$も可算無限集合。

最後に、LSuccRSuccBizeroに可算無限回適用して得られる値の集合を$B_2$として、差集合$B_2 \setminus B_1$を考える。LSuccを0、RSuccを1と読み替えれば、半開区間$(0, 1]$の各実数を二進数の無限小数で一意1に表したものと一対一に対応するので、$B_2 \setminus B_1$の濃度は連続体濃度。

以上より、Binat型のすべての値の集合は連続体濃度2





  1. 0.1とか0.1000...は0.0111...の表記に統一すると一意になる。なお、0.1の有限小数の表記は$B_0$に、0.1000...のゼロが無限に続く表記は$B_1$にそれぞれ対応するイメージ 



  2. 正確にはx = LSucc xみたいなBizeroを含まない奴らも考えてあげないといけないが、リストのreverseのような関数を想定すれば$B_2$の値と一対一対応するので無視して良いかなって感じがある