鳩ノ巣原理
証明書こう書こうと思っていて未だに書けてないやつtakker.icon
証明すべき論理式
$ \forall m, n\in\Bbb{N}\ \left( m\gt n\implies \lnot\exists f:[0, m]\cap\Bbb{N} \rightarrowtail [0, n]\cap\Bbb{N}\right)
任意の集合に対して拡張した式
$ \forall A,B\ \left(|A|>|B|\implies \lnot\exists f:A\rightarrowtail B\right)
これが成り立つかどうかはわからない
多分成り立つと思うけど
証明の方針
$ \left(\exists f:[0, m]\cap\Bbb{N} \rightarrowtail [0, n]\cap\Bbb{N}\right)\implies\bot を示せればなんとかなるな
つまり背理法を使う
$ x\mapsto x で$ \exists f:[0, n]\cap\Bbb{N} \rightarrowtail [0, m]\cap\Bbb{N} を示せるから、これと$ \exists f:[0, m]\cap\Bbb{N} \rightarrowtail [0, n]\cap\Bbb{N} とSchröder–Bernsteinの定理とを組んで$ \exists f:[0, m]\cap\Bbb{N} ⤖ [0, n]\cap\Bbb{N} を示せる んでさらにこれから$ \big|[0, m]\cap\Bbb{N}\big|=\big|[0, n]\cap\Bbb{N}\big| を導けるが、$ \big|[0, m]\cap\Bbb{N}\big|=m\neq n=\big|[0, n]\cap\Bbb{N}\big| で矛盾する
あとはこれを厳密に論理式で書き直せばいいだけか
これは非可算無限集合の場合に適用できない
この証明に関係するのが↓なんだろうな
せきゅーん @integers_blog
@tsujimotter @motcho_tw ペアノの公理から厳密に証明出来る定理として、$ \{1,2,…,n\} を$ [n] と表すとき、自然数$ m, n に対して写像$ f:[m]→[n] が単射ならば$ m≦nであるというものがありますが、これの対偶が鳩ノ巣原理だったりしません？
References
図解付きでかなり解説が丁寧