PA2 (Peano Arithmetic in 2º order logic and categoricty)

Question

Second order logic implies categoricity in peano arithmetic. But why are the models isomorphic to the standard model of aritmhetic and not to another non standard model, for example?

Answer 1

The point is that there is a single second-order sentence which completely characterizes (up to isomorphism) the structure $(\mathbb{N}, 0, 1, <, +, \times)$. Specifically, the standard model is characterized by the property that every element has only finitely many predecessors - and we can write this in second-order logic as $$\forall n\forall F([\forall m(m<n\implies F(m)<n) \wedge \forall m_1, m_2(m_1\not=m_2\implies F(m_1)\not=F(m_2))]$$ $$\implies \forall m<n\exists k<n(F(k)=m));$$ in English, this is just saying "for every $n$, every injective function from $\{m: m<n\}$ to $\{m: m<n\}$ is surjective." This sentence, when conjoined with the finitely many non-induction axioms of Peano arithmetic, characterizes the standard model up to isomorphism.