Yes, all theories at least as strong as PA (including ZF) have models with nonstandard naturals.

Another fun fact is that ZF has a countable model, even though ZF proves that uncountable sets exist. https://en.wikipedia.org/wiki/Skolem%27s_paradox

Can you express the notion of nonstandardsness within the language (and so add the axiom "no natural numbers are non standard")?

You could try, but your internal view of "standardness" won't always coincide with the external view, just like with finiteness or countability. In fact, here's a proof that the attempt can never succeed:

Take any formal theory T that talks about natural numbers, like PA or ZF. We'll assume that T can be encoded as a computer program, printing out sentences about natural numbers in some simple language with arithmetic and quantifiers. We won't make any other assumptions about the theory's internal workings, it can use any axioms it likes.

Thanks to the miracle of Turing completeness, any facts about that computer program can also be encoded as sentences about natural numbers. So we can construct a sentence called Con(T) which says essentially "the program will never print 0=1", or equivalently "there's no natural number N encoding a proof in T that 0=1". That sentence encodes the idea that "T is a consistent theory" within T itself.

Godel's theorem says that T cannot prove Con(T). Therefore we can extend T with the negation of Con(T), and the resulting "self-hating" theory T+¬Con(T) will be as consistent as T itself. Like all consistent theories, that theory will have a model, which is also a model of the original theory T. In that model, Con(T) is axiomatically false, so the above-defined number N is asserted to exist. But if we assume that T was consistent to begin with, then there's actually no finite proof in T that 0=1, so N can't be a standard natural number. Therefore N is nonstandard, so T has a model with a nonstandard natural number. QED.

Not in first order logic.

Why doesn't one simply use higher order logic to solve this problem? (serious question, I'm a mathematician, but not a set theorist).

It turns out this only pushes back the problem. You can write down second-order axioms for arithmetic which have a unique model, but in a model of a second-order theory predicates are interpreted as sets. So, you need to choose a version of set theory, to know what a model actually is. Suppose you choose ZFC (the usual axioms of set theory). Unfortunately this itself has infinitely many models!

I explained this in a bit more detail here:

https://johncarlosbaez.wordpress.com/2016/04/02/computing-th...

Thanks, this looks plausible.

A lot of properties that you'd want in a logic stop holding once you hit second-order logic: https://en.wikipedia.org/wiki/Second-order_logic#Metalogical...