FOM: Monomathematics and Friedman; non-standard numbers
neilt at hums62.cohums.ohio-state.edu
Mon Nov 17 13:38:06 EST 1997
This is directed to Harvey, but for consumption by everyone on the
Harvey stated a conservative extension theorem that goes roughly like
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
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
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.
More information about the FOM