TorqueDrifter comments on Logical Pinpointing

[TorqueDrifter]

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”?

[Incorrect]

An infinite number of axioms like in an axiom schema doesn’t really hurt anything, but you can’t have infinitely long single axioms.

∀x((x = 0) ∨ (x = S0) ∨ (x = SS0) ∨ (x = SSS0) ∨ ...)

is not an option. And neither is the axiom set

P0(x) iff x = 0
PS0(x) iff x = S0
PSS0(x) iff x = SS0
...
∀x(P0(x) ∨ PS0(x) ∨ PS0(x) ∨ PS0(x) ∨ ...)

We could instead try the axioms

P(0, x) iff x = 0
P(S0, x) iff x = S0
P(SS0, x) iff x = SS0
...
∀x(∃n(P(n, x)))

but then again we have the problem of n being a nonstandard number.