有理整数を基本とするにしても、
標数0の環の最小の部分環が同型を除いて一意的であることを示すためには
結局、ペアノの公理系を使う
「1をn回（有限回）足す」の意味を確定させないといけないから