FOM: Logic of x >> 0 and x >> y

[Harvey Friedman]

The discussion of infinitesmals has stimulated me to think about formal
systems of arithmetic with nonstandard (infinitely large) integers and also
with x >> y. The idea of x >> y is that x >> 0 is a special case
corresponding to x being nonstandard (infinitly large).

I had worked on this topic already as a student in 1967. I considered
several systems, among them being the following system PA(St) with the
language of PA augmented with a predicate symbol St(x) for "x is standard":

i) quantifier free axioms of PA;
ii) the standard integers are closed under addition and multiplication and
include 0,1;
iii) the induction scheme along the standard integers for all formulas in
the extended language;
iv) any formula not mentioning St, with parameters for standard integers,
holds if and only if it holds when relativized to St.

The 1967 Theorem was that such systems are conservative extensions of PA =
Peano arithmetic.

Since then, a variety of people have taken up the study of such systems,
including Avigad, Hrbacek, Nelson (I believe), Sommer, and others. I have
not kept up with the literature. These studies include the consideration of
such systems beyond the context of arithmetic.

In rethinking these matters, some directions occurred to me that I don't
remember seeing discussed.

1. In PA(St), modify the induction scheme analogous to the various ways
that the induction scheme has been modified in the detailed study of
fragments of PA - e.g., see Hajek/Pudlak, Metamathematics of First-Order
Arithmetic. Then figure out what the conservative extension results should
be.

2. Let phi be an arbitrary sentence in the language of PA(St). Can we
figure out whether phi is true? By this I mean, is there always a sentence
psi without S such that PA(St) proves (phi iff psi)? If this fails, is
there an interesting extension of PA(St) so that this holds?

NOTE: I now see that this fails. The only direction along these lines that
seems promising is to study this question with restrictions placed on phi.

3. What happens when intuitionistic logic is used for PA(St) and such
systems? Do we still have conservative extension results?

Now consider the system PA(>>) based on the idea of x >> y, meaning "x is
infinitely greater than y".

i) quantifier free axioms of PA;
ii) for any given x, the y's such that y >> x form a tail of nonnegative
integers higher than x;
iii) if phi(x) is a formula without >> that has parameters not>> y and
which has a solution x, then phi(x) has a solution x not>> y;
iv) if y >> x then you can raise y and/or lower x;
v) >> is transitive;
vi) induction holds for the integers y not>> x provided in the formula, the
relation >> is used only between the y >> x.

4. Study the above questions 1-3 for PA(>>). I think there are some
interesting strengthenings of PA(>>) that should also be studied.

5. At least I see how to show that PA(>>) is a conservative extension of PA
if we weaken vi) to apply only to formulas as given there which must also
be bounded. This is also a conservative extension of PA(St) in the
appropriate sense.