[FOM] circumscription and Peano Arithmetic

[Harvey Friedman]

On 1/21/04 7:39 PM, "Martin Davis" <martin at eipye.com> wrote:

> Harvey Friedman asks:
> 
> <<By the way, did the T(min) people ever notice that it generates Peano
> Arithmetic?>>
> 
> Yes. See my ancient paper referenced in a recent posting.
> 
I now have a copy of your "ancient" paper

M. Davis, The Mathematics of Non-Monotonic Reasoning, Artificial
Intelligence, vol.13(1980), pp. 73-80.

What you show there is that

T(min) = a perfectly good form of Peano Arithmetic

where T is, essentially, the nonnegative part of the theory of discrete
ordered rings formulated with RELATION SYMBOLS and not the usual FUNCTION
SYMBOLS and CONSTANT SYMBOLS.

In fact, you prove a sharper form of this with RELATION SYMBOLS, in that you
isolated the fragment of the nonnegative part of the theory of discrete
ordered ring axioms that you need for your relativization argument.

My result (or observation), that

T(min) = Peano Arithmetic for Z

where T is literally the axioms of discrete ordered rings, formulated as
usual with CONSTANTS and FUNCTIONS, does not follows from yours, or what you
do in your very nice paper.

In fact, what I did is (merely) a (very satisfying) reformulation of a form
of (the by now well known) "cut shortening technology", going back to
Solovay (unpublished) and Edward Nelson (published in Predicative
Arithmetic, 1986). 

M. Davis, in 1980, avoids this delicious twist by using relation symbols
instead.

The reason for the difference is that, model theoretically, we are talking
about definable submodels of models. This takes on a different character
when using constant and function symbols, than it does with only relation
symbols, because submodels have to be closed under the functions.

In fact, you comment explicitly that you wish to avoid using function
symbols because you only get "a weakening of mathematical induction".
However, the cut shortening technology (going back to Solovay (unpublished)
and Edward Nelson (published)) shows that the weakening is in fact
equivalent to mathematical induction.

By the way, I used discrete ordered rings because of its very familiar
completely mathematical nature. One can use very weak fragments, as Nelson
does with his cut shortening. E.g., the whole matter can be properly
formulated over R.M. Robinson's Q. Cut shortening for Q goes back to Nelson
(published in Predicative Arithmetic, 1986).

Harvey Friedman