[francisdavey]

It has (lots of) non-standard models. Or, to put it another way, there are statements that can neither be proved or disproved. This extends to any theory containing "enough" arithmetic and certainly any containing Peano Arithmetic. So ZF set theory is also incomplete in that sense.

You can "solve" this in Second Order logic, because you have a more powerful induction axiom, but how exactly you define that logic is tricky. There's no proof system that defines it completely, so you have to do this via a semantics that relies on knowing which models are or are not OK.

I don't think it solves the problem that you can't define all the "truths" (as most logicians would put it) of Peano Arithmetic.