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?

Question

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.

Answer 1

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.

Answer 2

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.