non-standard models of arithmetic in second order arithmetic?
Background:
According to Godel's theorem, if we have, in a given consistent system S, a non-provable wff. A, then we can extend the system to either S1 or S2 by including A or ~A as a new axiom, respectively. Both S1 and S2, according to Godel, will be consistent. If S is a first order system, then both S1 and S2 have at least a model, (let us call them M1 and M2) and the two models are essentially different because in M1 A is true, but in M2 ~A is true.
If S is PA (peano arithmetic), then that means that there are infinitely many unintended models in addition to the natural numbers, each one obtained by extending PA with a new axiom which is not true for the model of the natural numbers. These unintended interpretations are named non-standard models of arithmetic.
The question(s):
The above conclusions refer to first order systems. However, it is unclear to why this argument is restricted to first order systems, as Godel's proof is also valid for second order systems: Any extension of second order PA can be consistently extended into two different systems by including any non-provable wff. A or ~A as a new axiom, respectively. These two systems should in turn describe two essentially different models, and so there should also be non-standard models of arithmetic in second order arithmetic.
The problem is, that it is often stated that second order PA determine the set of natural numbers uniquely, and so there should be not room for non-standard models of arithmetic in second order arithmetic, which contradicts what .
Metaquestion: I am sure there is something wrong in my reasoning leading to this contradiction. But I cannot find any errors, can anybody help me, please!!!!
Best Answer
Let $\mathsf{PA_2}$ be a standard recursively axiomatized second-order Peano Arithmetic (e.g. the theory which Hilbert and Bernays call $\mathsf{Z}_2$). And interpret the wffs of $\mathsf{PA_2}$'s language with the 'full' semantics, where the second-order quantifiers are constrained to run over the full collection of sets of numbers.
Then (i) Gödel's theorem applies, of course, to $\mathsf{PA_2}$, so (assuming consistency) there will be a true canonical Gödel sentence $\mathsf{G}$ such that $\mathsf{PA_2} \nvdash \mathsf{G}$.
However, (ii) $\mathsf{PA_2}$, with the full semantics, is categorical by Dedekind's argument, so has only one model (up to isomorphism). In that one model, $\mathsf{G}$ is true, so $\mathsf{PA_2} \vDash \mathsf{G}$.
This shows that syntactic provability $\vdash$ falls short of semantic entailment $\vDash$ in the scecond-order case (there is no complete deductive system for second-order consequence, assuming the full semantics).
In summary, then, while the claim "$\mathsf{PA}$ settles all arithmetical truths" is false however we interpret it (where $\mathsf{PA}$ is first-order Peano Arithmetic), the situation with the corresponding claim "$\mathsf{PA_{2}}$ settles all arithmetical truths" is more complex. It depends whether you mean "semantically entails" or "deductively implies".
For vividness, it may well help to put that symbolically. We'll use $\{\mathsf{PA}, \vdash\}$ to denote the set of theorems that follow in $\mathsf{PA}$'s formal proof system, and $\{\mathsf{PA}, \vDash\}$ to mean the set of sentences semantically entailed by $\mathsf{PA}$'s axioms (given the standard semantics for first-order arithmetic). Similarly, we'll use $\{\mathsf{PA_{2}}, \vdash_2\}$ to mean the set of theorems that follow in $\mathsf{PA_{2}}$'s formal proof system, and $\{\mathsf{PA_{2}}, \vDash_{2}\}$ to mean the set of sentences semantically entailed by $\mathsf{PA_{2}}$'s axioms (given the "full" semantics for the quantifiers). Finally we'll use $\mathcal{T}_{A}$ to denote the set of truths of first order arithmetic (often called, simply, True Arithmetic); and we'll now use $\mathcal{T}_{2A}$, the set of truths of the language of second-order arithmetic (True Second-Order Arithmetic). Then we can very perspicuously display the relations between these sets as follows, using `$\subset$' to indicate strict containment:
$\{\mathsf{PA}, \vdash\} \;=\; \{\mathsf{PA}, \vDash\} \;\subset\; \mathcal{T}_{A}$
$\{\mathsf{PA_{2}}, \vdash_2\} \;\subset\; \{\mathsf{PA_{2}}, \vDash_{2}\} \;=\; \mathcal{T}_{2A}$.
The completeness of first-order logic which yields $\{\mathsf{PA}, \vdash\} = \{\mathsf{PA}, \vDash\}$ is, though so familiar, a remarkable mathematical fact which is enormously useful in understanding $\mathsf{PA}$ and its models. This has led some people to think the strict containment $\{\mathsf{PA_{2}}, \vdash_2\} \subset \{\mathsf{PA_{2}}, \vDash_{2}\}$ is a sufficient reason to be unhappy with second-order logic. Others think that the categoricity of theories like second-order arithmetic, and the second-order definability of key mathematical notions like finiteness, suffices to make second-order logic the natural logic for mathematics. Stewart Shapiro's Foundations without Foundationalism is a classic defence of the second position.
The issue here is discussed at some length in Ch. 29 (or Ch. 22 of the 1st edition) of my Gödel book, if you want more!