FOM: Monomathematics and Friedman; non-standard numbers

[Neil Tennant]

This is directed to Harvey, but for consumption by everyone on the
list.

Harvey stated a conservative extension theorem that goes roughly like
this.

Let S be a predicate intended to mean "...is a standard natural
number". (Note that S is uppercase; lowercase s means as usual the
successor function.)  For any formula F of the language of arithmetic,
let F(S) be the formula resulting from F by relativizing all
quantifiers to (the extension of) S. If X is a set of formulae, then
X(S) is the set of all F(S), F in X. 

Take PA in a free logic, so that it includes as explicit axioms

Ex x=0
(x)Ey y=s(x)

Let nsPA be the theory whose axioms are those of PA and of PA(S), plus
the axiom Ex~S(x).

Theorem (Friedman): For all S-free F, nsPA |- F => PA |- F.

This result (appropriately generalized) could play a significant role
in arguing for the legitimacy of what one might call the
"monomathematical" conception, namely the conception of certain areas
of mathematics (natural number theory; real number theory; the theory
of complex functions; set theory) as being about *unique intended
structures*, despite the limitations imposed by the Goedel phenomena.
(Indeed, Goedel himself was a monomathematician--see his essay 'What
is Cantor's continuum problem?'.)

The appropriate generalization it would be nice for Harvey to provide
is the following:

1. The above theorem holds upon replacing PA with any true extension T
of PA.

2. It also holds with intuitionistic logic as the underlying logic of
the theories T, nsT.

3. There is no blow-up in length of proof of S-free theorems as one
passes from nsT to T.

Then: What about : 1', 2' and 3', where these result from 1, 2 and 3
upon replacing "true" in 1 with "consistent"?

Harvey, if you could answer these queries, I'd be grateful. It would
sharpen Occam's razor for one who wishes to be a monomathematician
about the natural number structure N.

Neil Tennant