ちなみにだけど、後者を写像と言っていいか微妙な感じだから、ペアノシステムに5つの性質を挙げたけどここに６つ目の性質、
6. n,mが台集合の元でn=m ならば nの後者 = mの後者
を追加したい。
(あるいは、4. を nとnの後者は一対一 というふうにするだけでもok)

> 君が「2つ組」にこだわるのは、「2つ組さえあれば台集合の一意性が言えそうに見えるから、本質的には2つ組だけで十分なんじゃないか」という感覚から来ていると思われる。
そう。まさにその通り。

つまり、2つ組さえあれば台集合の一意性が言えそうに見えるけど、果たして本当にそうなのかというのが議論の的だと言える。


方針としては、２つ組から一意的な台集合の作り方を決めて、そこにまだ足りない性質を付け足して完成というやり方。
例えば、先頭が1で、後者が(+1 mod3) という場合は台集合{1,2,0,1,2,0 ... } = {1, 2, 0}は一意的に決まるけど3.を満たさなくなっちゃう。
そういったもののために台集合の作り方を決めるのとは別に足りない性質を付け足す必要がある。

>602で付け足したのが今の例を防ぐためのもの(3.)と、4. と 6. 。
つまり、台集合を一意的に決めるという事は、1. 2. 5. が満たされる事と同義だと思ったって事。

>「台集合の一意性」は、既存のペアノの公理系における「5」にほとんど完全に対応している
というのは納得しているけど、俺の考えだと5.だけでなく、1. 2. 5. の３つに対応している。
592では 5. とだけ言ったけど、その時は適当に考えてたから許してほしい。

さっき602では「...」で誤魔化したけど、「(先頭, 後者)から1. 2. 5. を満たすような台集合を作る」ってふうにすれば問題ないように思える。
1. と 2. は分かりやすいけど、 5. が何の制約になってるかというと、先頭と、その次と、 ... では作れないような元が入れ込めないようにしていると解釈してる。
つまり、1. 2. だけだと(1, ÷2)の組の台集合に2とか∞とかが入ってる事が否定できないけど、これを5. が防いでくれてる。
この３つの性質があれば、台集合が一意に定まる事は証明できると思うんだけどどう？