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

[Petr Andreyev]

Harvey Friedman wrote:
> ....
> 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.
>

probably the following is relevant:

In every nonstandard extension one can define y>>x iff y > *f(x)
for every standard function f. The standard set of natural numbers
will then be a model for PA(>>).

If the extension is 2^aleph0-saturated
then for any y there are x, v such that y>>x>>v
(this statement could be a candidate for a strengtening of PA(>>)).

If the extension is compact then every >>-sentence is equivalent to a
sentence without >> since every sentence will be equivalent
to an internal one (this is a result of Karel Cuda (199?);
the situation here is similar to that with BST as Vladimir Kanovei wrote).

Moreover, Cuda has also a paper (which I have not read but which should be
relevant to the question 2)

[Č1982] K.Čuda, An elimination of the predicate "To be a
standard number"in nonstandard models of arithmetic, CMUC 23 (1982), 785-803

The interpretation of >> mentioned above gives rise to Ye.Gordon's notion
of relative standardness. I have a small text on this topic in which
it is shown, in particular, that the predicate of >> can be useful
in the full context of nonstandard analysis.
(http://www.xanadu.ru/~viron/motiv3.ps)

Another possible interpretation could be derived
in the same manner from Y.Peraire's RIST, which could be a source for
possible strenghtenings of PA(>>).

I am curious who was the first who introduced and used >> in the sense of
PA(>>).

--
Petr