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.
Being an ex-proof theorist, I'm a bit dubious of not having one.