How is the standard model of number theory specified, and why can't we use that specification to prove any number theoretical sentence of interest?

According to Gödel's incompleteness theorem, there exists a sentence $G$ in the vocabulary of number theory ($N$) which is not provable from any (recursively enumerable) consistent set of axioms $T$, and yet which is true under the standard model ($SM$) of $N$. Also, this means that there is some other model $M$ of $T$ under which $G$ is false (for otherwise, if $G$ was true in all models of $T$, then $G$ would be provable from $T$, by the completeness theorem for FOL).

My question is, how, or in what fashion, do we specify or describe the standard model $SM$ of $N$? Some kind of a description/specification (in some metalanguage perhaps) seems necessary if we are to show that $G$ is true under $SM$, and also if we are to differentiate it from some other, non standard model $NSM$ of $N$. But once we have such a formalized specification $S$, isn't that itself a kind of an axiomatization of the standard model (which presumably can be expressed in first order logic)?

In other words, from S we would be able to prove any sentence $\phi$, as long as $\phi$ is valid under all models $M$ described by $S$ (i.e. $M\models S$). But since S is a formalized description/specification of the standard model of $N$, the models described by it have exactly the structure of what we normally mean by "numbers" and "arithmetic" and "number theory", and hence we would be able to prove any number theoretical sentence that was truly of interest to us.

• I think the set of axioms needs to be recursive, not merely recursively enumerable. Otherwise if someone gives you a purported proof that contains a nonaxiom but claims that it is an axiom, you can't tell that the proof is lying. – MJD Jun 9 '13 at 18:15
• "According to Godel's incompleteness theorem, there exists a sentence G in the vocabulary of number theory (N) which is not provable from any (recursively enumerable) consistent set of axioms T, and yet which is true under the standard model (SM) of N." This is certainly not true - just take $G$ itself as an axiom! The quoted phrase is a relatively common misstatement of the incompleteness theorem. The rest of the question is OK, however. – Carl Mummert Jun 9 '13 at 18:16
• @MJD: for any r.e. theory $T$ there is a recursive theory $T'$ which proves exactly the same sentences (and we can obtain an index for $T'$ effectively from an r.e. index for $T$; and we can even make $T'$ primitive recursive and find a p.r. index for it effectively from an r.e. index of $T$). – Carl Mummert Jun 9 '13 at 18:17
• Thanks, I did not know that! Can you point me to a reference? – MJD Jun 9 '13 at 18:18
• @MJD: Let $T$ be an r.e. theory, so it is the range of some computable function $f$. Define $T'$ so that a formula $\psi$ is an axiom of $T'$ if and only if $\psi$ is of the form $\phi \land \phi \land \cdots \land \phi$, for some number $k$ of conjuncts, so that $f(k) = \phi$. Then this $T'$ will be a recursive theory with the same consequences as $T'$. A similar technique can be used to make $T$ be primitive recursive. The upshot is that an arbitrary theory has an r.e. axiomatization if and only if it has a primitive recursive one, so the incompletness theorem can be stated either way. – Carl Mummert Jun 9 '13 at 18:26

Here's a quick response, in headline terms.

To specify the standard model, up to isomorphism, we need the idea that zero is a number, that the successor of a number is a number, and nothing else is a number.

Now, the last clause here is the troublesome one here. On the one hand, the idea it encapsulates seems very basic, very simple, something we pick up early in our mathematical training. On the other hand, we can show that it is inexpressible in a first-order theory of arithmetic like first-order Peano Arithmetic.

To pin down that last closure condition, we need (it seems) to invoke second-order ideas. But second-order logic (with the relevant "full" semantics") is not recursively axiomatizable (so that's why it is wrong to say "once we have such a formalized specification $S$ [of the standard model], isn't that itself a kind of an axiomatization of the standard model (which presumably can be expressed in first order logic").

For more on this, see e.g. Shapiro's classic book on second-order logic (Foundations without Foundationalism), or my Gödel book.

• @Joe: it just takes 50 reputation to comment - which is only one or two answers. Don't hesitate to write answers if you have something to add to the existing ones. Thanks for the edit. – Carl Mummert Jun 10 '13 at 0:54

We can also think about the intended interpretations of theories in a non-mathematical, or pre-mathematical way.

For example, even young children can conceptualize an infinite flat two dimensional plane. On the basis of that understanding, they can see that Euclid's axioms (with the possible exception of the parallel postulate) are consistent. We don't really "specify" the idealized plane in great detail - we think we already know what it is, and then we try to use that previous knowledge to understand geometrical axioms.

Similarly, one way to think about the intended interpretation of arithmetic is the following. We usually think we have a good feeling for what a "finite string" is. Of course we can only write down relatively short strings, but just as we can imagine points arbitrarily far apart on a plane, we can imagine finite strings of arbitrary length. Now think about all the finite strings that only have the symbol 'a' in them: a, aa, aaa, aaaa, ... These form an intended interpretation of arithmetic starting with 1. The successor operation, in this interpretation, just adds another 'a' to the end of a string, and two strings are equal if the have the same length. This seems, to many, like a relatively concrete description of a model of arithmetic. For example, if we know that the string 'a' has some particular property, and we know that concatenating an 'a' onto a string with that property gives another string with the property, then we see immediately that every finite string of 'a's has the property - this is the principle of induction.

Of course, just because we think we have specified the model, does not mean that we know everything about the model on the basis of that specification. We ma know just enough to see that the axioms of a theory are true, without knowing enough to know whether some more complicated property (e.g. the twin primes conjecture) is true.