Isn't that just true for models of a first-order axiomatisation of the natural numbers? As far as I know, if you write down the Peano axioms in second order logic (as is required), you do get the natural numbers uniquely, and applying the successor function over and over again does exhaust all the natural numbers eventually.
The reason why you get non-standard models of arithmetic in first-order logic is the Löwenheim-Skolem theorem, but that isn't available for second-order logic.
The context of the comment is ZFC and its concept of the natural numbers (and what I had in mind in particular was what is its minimal infinite inductive set?). ZFC is a first-order theory, so "model" means model of a first-order theory.
> The reason why you get non-standard models of arithmetic in first-order logic is the Löwenheim-Skolem theorem
The ultrafilter construction I described is a way around the compactness theorem, in that it constructs new models semantically rather than syntactically. Ultrafilters are also a good way to prove the compactness theorem. But in any case, it's essentially the first half of the upwards Löwenheim-Skolem theorem before applying the downwards Löwenheim-Skolem theorem -- I think the significance of that theorem is that you can get models of any infinite cardinality you want, rather than just a strictly larger one. (Though I'm no logician.)
It's worth noting that this construction relies on the axiom of choice, so exists in ZFC but not ZF. Generally a lot of counter-intuitive constructions disappear when eliminating the axiom of choice (such as the Banach–Tarski paradox and non-continuous functions).
I think the step function doesn't depend on choice. Say f(x) = 0 if x < 0 and f(x) = 1 if x >= 0. Also, suppose we define the reals through Dedekind cuts. We can define f(x) by checking whether 0 is an element of x as a cut. We can prove f is discontinuous in the usual way.
What I had heard is that Brouwer proved, using some kind of constructive/intuitionistic logic, that every function is continuous, but ZF is still based in classical logic. I believe the step function is not definable constructively.
You can't define the classical reals this way in a constructive setting, only the computable reals.
I was objecting to this:
> Generally a lot of counter-intuitive constructions disappear when eliminating the axiom of choice (such as [...] non-continuous functions).
In context of the discussion, this non-standard model of the natural numbers gives some intuition about what happens if the consistency of ZFC is independent of ZFC and you add in the axiom that ZFC is inconsistent: your natural numbers will have to be something similarly weird.
> you have just made a new type of number not comparable to natural numbers
But they are comparable. The everyday natural numbers are embedded in this new system, which is what these (n,n,n,...) elements represent. One way to interpret what we've done here is to add in infinities to the number system so that all the normal operations still work, and there's even a total ordering on them!
Using the real numbers instead of the naturals, you get the so-called nonstandard real numbers, which is the number system used in nonstandard analysis. Nonstandard analysis is a way to do analysis without epsilon-delta proofs. Nonstandard reals include infinitesimals and infinities, similar to nonstandard naturals having infinities. There are even textbooks on the subject -- I haven't read them, but they claim it makes analysis easier.
The last thing that comes to mind is that nonstandard numbers of this exact type show up when you study certain infinite-dimensional number systems and calculate the points (like in the end of my comment).
Oh, I forgot I commented more than once today on HN. I was referring to this one: https://news.ycombinator.com/item?id=27851188
The ultrafilter construction gives one such model. You take the set of all sequences of natural numbers (n1, n2, n3, ...) then use an ultrafilter to decide which of these sequences are considered to be equal. The usual operations of natural numbers are defined term-by-term. You can think of the usual natural numbers as being the sequences (0,0,0,...), (1,1,1,...), (2,2,2,...) and so on. However, there are many additional numbers in this system, like (0,1,2,...) that are strictly greater than all the usual numbers, and these cannot be reached by repeatedly adding one. (The reason (0,1,2,...) is greater than (n,n,n,...) is that if we do the comparison term-by-term we get (false,false,...,false,true,true,true,...), and the ultrafilter will decide the comparison is true because it is true for all but finitely many terms. Ultrafilters are devices to consistently turn infinite sequences of trues and falses into a single decision, but every ultrafilter will make a true decision in the case there are only finitely many falses.)
Counter-intuitively, proofs by induction still work for this system... speaking with no authority here, maybe an intuition is that it's doing a hypercomputation.