Comment by Kranar

I think your contribution to this discussion has been very thorough but I need to nitpick some details:

>For any X⊆N, if 0 ∈ X, and for every n ∈ X, S(n) ∈ X, then X=N.

You're right that this is a perfectly valid axiom in SOL, but it's not true that it rules out non-standard "shit". What this axiom does is it forces your theory to have a single model, the categorical model. But this axiom does not in anyway pick out the standard model as the categorical model, it doesn't force the categorical model to be the standard model. It's possible that N = {0, 1, 2, ..., Q - 1, Q, Q + 1, ...} in which case the categorical model ends up being nonstandard. This axiom has no way to force N to be intended standard model.