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

[Petr Andreyev]

Dear Harvey,

now I see I missed your nice iv) and was wrong in the corresponding mine
(but still, iv) is true when the nonstandard extension is
2^aleph0-saturated).

Moreover, I am not sure whether vi) holds in the model I described. Could
you please write what you mean under "the relation >> is used only between
the y >> x"?

--
Petr

> 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.
>>