But any nonstandard number is not an nth successor of 0 for any n, even nonstandard n (whatever that would mean). So your rephrasing doesn’t mean the same thing, intuitively—P is, intuitively, “x is reachable from 0 using the successor function”.
Couldn’t you say:
P0: x = 0
PS0: x = S0
PSS0: x = SS0
and so on, defining a set of properties (we can construct these inductively, and so there is no Pn for nonstandard n), and say P(x) is “x satisfies one such property”?
But any nonstandard number is not an nth successor of 0 for any n, even nonstandard n (whatever that would mean). So your rephrasing doesn’t mean the same thing, intuitively—P is, intuitively, “x is reachable from 0 using the successor function”.
Couldn’t you say:
P0: x = 0
PS0: x = S0
PSS0: x = SS0
and so on, defining a set of properties (we can construct these inductively, and so there is no Pn for nonstandard n), and say P(x) is “x satisfies one such property”?
An infinite number of axioms like in an axiom schema doesn’t really hurt anything, but you can’t have infinitely long single axioms.
is not an option. And neither is the axiom set
We could instead try the axioms
but then again we have the problem of n being a nonstandard number.