FOM: 2:Axioms

[Harvey Friedman]

This is the second in a series of positive self contained postings to fom
covering a wide range of topics in f.o.m.

Last time (Foundational Completeness, 10:13 AM, 10:26 AM, 11/3/97) we
discussed some basic structures arising out of the usual set theoretic
foundation for mathematics; namely, the initial segments of the cumulative
hierarchy: V(0), V(1), ..., V(n),..., V(w), V(w+1), ..., V(w+n), ...,
V(w+w), under the epsilon relation. We alluded to fundamental axioms
holding in these basic structures.

Actually, people have normally concentrated only on axioms holding in V(w)
and, separately, in V(w+w). There is also some real attention paid to the
case of V(w+1), mostly in a little bit different context (a two-sorted
context with natural numbers and sets of natural numbers).

The "normal" axioms holding in V(w) are the usual axioms of ZFC without
infinity. But are there any sentences of a logical, axiomatic flavor that
hold in V(w) that are not provable in ZFC?

I agree that there is at least a basic ambiguity about this question.
Specifically, what about "every nonempty set has an epsilon maximal
element?" If this is accepted, then we get what would normally be called
ZFC\Infinity + not(Infinity). Is there anything more that would be regarded
as logical or axiomatic in nature?

I think the question is interesting mainly because anything anybody has
ever considered that goes beyond ZFC\Infinity + not(Infinity) seems to be
starkly, blatantly, different than ZFC\Infinity + not(Infinity). So the
very possibility of a completeness theorem for ZFC\Infinity + not(Infinity)
makes the question reasonable, where part of the question is to make a
working definition of "logical or axiomatic" that suffices.

There is another intriguing related aspect here. Notice that the first
axioms holding in V(w) that come to mind are just about all of ZFC - except
infinity. This suggests the following transfer principle:

any sentence true in V(w) is true in the full universe of sets.

The trouble is that this is of course false. not(Infinity) is true in V(w)
and not true in the full universe of sets.

So it is reasonable to search for a natural restriction on the form of the
sentences to be considered so that this transfer principle is playable. And
after a natural restriction is found, one explores the consequences of such
a transfer principle.

I have not "solved" this problem in this form, but have had success with a
related problem. I considered the related transfer principle (for each n,m):

any appropriate existence sentence true about all functions from w^n into
w^m is true about all functions from On^n into On^m,

and found the appropriate class of existential statements for which this is
reasonable. It turns out that it is equivalent to suitable large cardinal
axioms. See Transfer Principles ms. on my website
www.math.ohio-state.edu/~friedman/

But a detailed discussion of this will wait for a later posting.

Obviously V(w) serves as a well known model of the vast tulk practice of
finite mathematics - where every object is finitary. The corersponding
formal system would be ZFC\Infinity + not(Infinity). One can equivalently
formulate not(Infinity) in a more natural looking way, and perhaps more
directly useful way, as the following induction principle: if a property
holds of the emptyset, and whenever it holds of x,y, it holds of x union
{y}, then it holds of all sets. We might call this SetInduction - not the
same as Transfinite Induction, which follows from Foundation. In fact,
SetInduction implies Foundation. So we might boldly use the abbreviation
FST (finite set theory) for the system we are talking about, with its many
axiomatizations. It appears pretty robust. By the way, working out the
relationships between the various fundamental axioms about V(w) seems
worthwhile and rewarding. There are likely to be a number of quite tricky
points relating to showing that some axioms don't follow from others, if
this is investigated systematically.

Another closely related system of great historical importance is Peano
Arithmetic (PA). The close relation of PA to FST is illustrated by the
general model theoretic notion of synonomy. Synonomy and interpretability
have lots of subtleties and there are some striking theorems about them
that I plan to go into in another posting.

In the case of PA, say with just 0,S,+,x, there is even more feeling that
one has all of the basic axioms. Everything else is not an axiom - it's
simply too specialized and/or complicated. But how does one formulate and
prove this?

Can we pin down what is so special about the time tested, time honored,
intensively studied formal systems from f.o.m.?

A successful approach to some aspects of this question in some contexts is
afforded by Reverse Mathematics. This is actually rather striking. Again, a
subject of a future posting.