I was assuming we’ve specified the behaviour of the numbers sufficiently in the background ;) But the difficulty of doing that is part and parcel of the FOL weirdness: you don’t get the Lowenheim Skolem theorem in SOL! I was going to say that you need Compactness to prove it, but now that I think about it I don’t know that you need it, although it’s usually used in the proof of the upwards component.
I was assuming we’ve specified the behaviour of the numbers sufficiently in the background ;) But the difficulty of doing that is part and parcel of the FOL weirdness: you don’t get the Lowenheim Skolem theorem in SOL! I was going to say that you need Compactness to prove it, but now that I think about it I don’t know that you need it, although it’s usually used in the proof of the upwards component.