FOM: 9:Nonstandard Arithmetic

[Harvey Friedman]

This is the ninth in a series of positive self contained postings to fom
covering a wide range of topics in f.o.m. Previous ones are:

1:Foundational Completeness   11/3/97, 10:13AM, 10:26AM.
2:Axioms  11/6/97.
3:Simplicity  11/14/97 10:10AM.
4:Simplicity  11/14/97  4:25PM
5:Constructions  11/15/97  5:24PM
6:Undefinability/Nonstandard Models   11/16/97  12:04AM
7.Undefinability/Nonstandard Models   11/17/97  12:31AM
8.Schemes 11/17/97    12:30AM

Let me remind you that a complete archiving of fom, message by message, is
available at http://www.math.psu.edu/simpson/fom/index.html

In 7, I mentioned a result of mine from 1967, which is a conservative
extension result about formalized nonstandard arithmetic:

>Add a predicate St(x) for "x is standard" to the language of Peano
>Arithmetic (PA). Consider the following axioms:

>1. Usual equational axioms and axioms for successor.
>2. Induction for all formulas with respect to the Standard integers only.
>3. Induction for all formulas that don't mention St with respect to all
>integers.
>4. The successor of every standard integer is standard.
>5. There exists a nonstandard integer.

>THEOREM. Every sentence without St that is provable is already provable in PA.

NOTE: I forgot to say "axioms for successor, addition, and multiplication."

Actually, now that I recall, the result is somewhat more comprehensive. I
proved this result for the somewhat stronger system:

1. Usual equational axioms and axioms for successor, addition, and
multiplication.
2. Induction for all formulas with respect to the Standard integers only.
3. Induction for all formulas that don't mention St with respect to all
integers.
4. The successor of every standard integer is standard.
5. There exists a nonstandard integer.
6. Every formula with parameters from the standard integers that holds in
the standard integers, holds in the integers.

I.e., the axiom that the standard integers form an elementary submodel of
the integers. (By "integers" we always mean natural numbers, of course).
One can derive that the standard integers are a proper initial segment of
the integers.

But there is a neater equivalent axiomatization for those of us who care
about elegance (I do!):

1. Usual equational axioms and axioms for successor, addition, and
multiplication.
2. The successor of every standard integer is standard.
3. Induction for all formulas with respect to the Standard integers only.
4. x1,...,xk standard & (therexists y)(A(x1,...,xk,y), implies (therexists
standard y)(A(x1,...,xk,y)).
5. There exists a nonstandard integer.

Call this system NPA. It proves the following:

a. the standard integers are closed under successor, addition, and
multiplication.
b. that the standard integers under S,+,x, are an elementary extension of
the integers.
c. induction with respect to formulas not mentioning St. In particular, NPA
proves PA.
d. the usual axioms for < with the usual definition, and that every integer
< some standard integer is a standard integer.

NPA looks like a robust system like PA.

THEOREM 1 (1967). Any sentence without St provable in NPA is provable in PA.

We isolate and prove the key model theoretic fact about nonstandard models
of arithmetic that implies this Theorem.

THEOREM 2. Fix n >= 1. Every nonstandard model M of PA has an n-elementary
end extension M' where every nonempty subset of dom(M) definable over
(M,M') has a least element. (Any parameters from dom(M') are allowed).

Proof: Let n,M be as given. Now sit in M and do f.o.m. in M. Form the
theory consisting of the true sigma_n sentences plus PA. Now there is a
problem, becuase M might not satisfy that PA is consistent. So pick a
nonstandard integer m in M such that Con(PA_m) holds in M. In fact, we can
pick a nonstandard integer m in M such that K = true sigma_n sentences plus
PA_m, is consistent from the point of view of M. To see this, one uses an
overspill argument, and the formalized cut elimination theorem for
predicate calculus. Recall that n is a standard integer.      Now that M
knows that K is consistent, M can do the Godel completeness theorem
(f.o.m.!), and construct an explicitly defined model M' of K. Induction in
M shows that M' is an end extension of M. Also (M,M') is defined in M, and
so the conclusion holds. QED.

We have just come to realize that there is a sensible general form of this.
Let T be any extension of PA by formulas and schemes. The schemes may
involve restrictions on free variables. We also allow expansion of the
language, and the schemes may involve additional restrictions on the
substitution formulas in terms of the nonlogical symbols allowed. However,
if the language is expanded, we insist that the induction scheme be taken
to incorporate all formulas in the extended language. Then there is the
concept of "nonstandard T". It has a new monadic predicate symbol St for
"standard object."

1. All axioms of T.
2. The standard objects form an elementary submodel of the objects, using
all of the relations, constants, and function symbols in the language.
3. There exists a nonstandard integer.
4. Each nonstandardization of each scheme. This is the result of a)
relativizing all quantifiers and free variables in the scheme to the
standard objects, and b) allowing any formula, incluing St, to be used for
substitution (subject to the original restrictions made for the scheme).

THEOREM 3. Any sentence without St provable in Nonstandard T is provable in T.

Use the same proof.

Now we come to lengths of proofs. Let PA_n be PA with the induction scheme
for sigma_n. Let NPA_n be NPA with the induction scheme and elementarity
for sigma_n.

THEOREM 3. NPA_n is interpretable in PA_n+1, where the standard integers
get interpreted as the integers. The size of the verification of the
interpretation is linear as a function of n.

Proof: Adapt the proof of Theorem 2. We first have to prove in PA_n+1 that
PA_n + "the true simgma_n sentences" is consistent. The proof ultimately
rests on a giant induction, corresponding to the soundness of the cut free
rules of inference with respect to the appropriate truth definition. We
claim that this has a proof whose size as a function on n is linear.
Although the proof uses the cut elimination theorem for predicate calculus,
which has a blowup, the cut elimination theorem has a perfectly good proof
in PA_1, and is reflected in all of this as a constant. QQED.

THEOREM 4. Theorem 1 is true without blowup in length of proof. It is true
linearly.

It also appears that Theorem 4 can be adapted to general contexts such as
in Theorem 3.