NNO = (first order) PA - MathOverflow

NNO = (first order) PA

2012-04-10T07:50:32Z

Recall the definition of a Natural Numbers Object in a topos, and the first order axioms for Peano Arithmetic. I am more familiar with the first definition than the second, so I cannot tell from the (obviously infallible) Wikipedia page whether first order PA is equivalent to 'second order' PA -- PA with the induction axiom scheme replaced by a similar one involving inductive subsets $A \subset \mathbb{N}$.

The equivalence between 'second order' PA and a NNO in $Set$ in one direction (NNO $\Rightarrow$ PA) is easy, and the other (PA $\Rightarrow$ NNO) is in MacLane's book Mathematics, form and function which I haven't seen (bonus question: another reference for the proof would be nice).

But I would like to see a proof of NNO = (first order) PA, if possible.

My motivation is to consider possibly weaker forms of arithmetic, and it is how to deal with (versions of) the induction axiom schema as usually presented from a logic point of view on which I would like a bit of background.

Edit: As Andreas points out, I really should be asking about models of PA and NNOs.

Answer by Emil Jeřábek for NNO = (first order) PA

2012-04-10T11:25:59Z

A NNO is unique up to isomorphism (likewise, a model of second-order arithmetic is unique). In contrast, every first-order theory with at least one infinite model has a proper class of nonisomorphic models of arbitrary large cardinalities, due to Löwenheim–Skolem theorem. Thus, NNO cannot be equivalent to PA, or any other first-order arithmetic for that matter.

Answer by Andrej Bauer for NNO = (first order) PA

2012-04-11T07:05:25Z

J. Lambek and P. J. Scott: Introduction to higher-order categorical logic, Cambridge University Press, 1986, Part II, Section 4, Theorem 4.1 shows that a nno satisfies the first-order Peano rules (which are listed on page 135 under 3.7, 3.8., 3.9), while Part II, Section 12, Proposition 12.4 shows that Peano rules give a nno for the syntactic topos. By the universal property of the syntactic topos it then follows that in any topos which validates Peano rules has a nno.

The whole business with classical vs. non-classical logic is a red herring. You may throw excluded middle in if that is your wish.