[btilly]

The Peano Axioms lead to both the standard model of arithmetic (the integers that we want), and nonstandard models. See https://en.wikipedia.org/wiki/Non-standard_model_of_arithmet....

In that article you'll see references to "first order logic" and "second order logic". First order logic captures any possible finite chain of reasoning. Second order logic allows us to take logical steps that would require a potentially infinite amount of reasoning to do. Gödel's famous theorems were about the limitations of first order logic. While second order logic has no such limitations, it is also not something that humans can actually do. (We can reason about second order logic though.)

Anyways a nonstandard model of arithmetic can have all sorts of bizarre things. Such as a proof that Peano Axioms lead to a contradiction. While it might seem that this leads to a contradiction in the Peano Axioms, it doesn't because the "proof" is (from our point of view) infinitely long, and so not really a proof at all! (This is also why logicians have to draw a very careful distinction between "these axioms prove" and "these axioms prove that they prove"...)

[pja]

All of these models appear to contain infinitely sized objects that are explicitly named / manipulable within the model, which makes them extensions of the Peano numbers though, or else they add other, extra axioms to the Peano model.

If you (for example) extend Peano numbers with extra axioms that state things like “hey, here are some hyperreals” or “this Goedel sentence is explicitly defined to be true (or false)” it’s unsurprising that you can end up in some weird places.

[btilly]

We are able to recognize that they are nonstandard because they contain numbers that we recognize are infinite. But there is absolutely no statement that can be made from within the model from which it could be discovered that those numbers are infinite.

Furthermore, it is possible to construct nonstandard models such that every statement that is true in our model, remains true in that one, and ditto for every statement that is false. They really look identical to our model, except that we know from construction that they aren't. This fact is what makes the transfer principle work in nonstandard analysis, and the ultrapower construction shows how to do it.

(My snark about NSA is that we shouldn't need the axiom of choice to find the derivative of x^2. But I do find it an interesting approach to know about.)

[Maxatar]

No additional axioms are needed for the existence of these models. On the contrary additional axioms are needed in order to eliminate them, and even still no amount of axioms can eliminate all of these extensions without introducing an inconsistency.