[francisdavey]

The fact that Peano Arithmetic isn't categorical, and that if you want to nail it down you need either bigger theories (within which you can of course nail down a single model) or move to theories which don't have proof theories like second order arithmetic, suggests all might not be as easy as it looks here.

Being an ex-proof theorist, I'm a bit dubious of not having one.

[feanaro]

What does it mean that Peano Arithmetic isn't categorical?

[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.

[cubefox]

Pure terminology. In some areas "Peano Arithmetic" is short for "first-order Peano arithmetic". In first-order logic, Peano's induction axiom can't be properly formalized, which means the resulting theory isn't categorical. For other people "Peano arithmetic" just describes the usual Peano axioms in natural language, which includes the proper induction axiom. Which can only be formalized by using at least second-order logic. That theory is categorical.