In first-order logic, we can get rid of the ABC—make a statement which rules out any model that has a loop of numbers like
that. But we can’t get rid of the infinite chain underneath it. In second-order logic we can get rid of the extra chain.
(exists x) (forall y) not (S(y) = x)
This statement is a first order statement which is true of standard natural numbers, but is not true in your model.
(exists x) (forall y) not (S(y) = x)
This statement is a first order statement which is true of standard natural numbers, but is not true in your model.
???