>>703
順序はなくして標数0にした方が良いか
自然に順序も誘導されるし
最小性は帰納法のようにある意味一階で表現できるが、完備のような最大性は一階では無理なので、敢えて代数的と断って実閉体にした
どちらにせよ標準モデルのように特定したいなら、ZFCで自然数の標準モデル(に+*入れたもの)を作って
それから順序対の同値類別で整数作って
それから順序対の同値類別で有理数作って
それからコーシー列なり切断なりで実数作って
となるけど、自然数はペアノの公理というならモデルではなく公理系を求めているんだろうからこれは違うかなと