FOM: Is ZF true?

[Jon Barwise]

Harvey Friedman long ago (around 1970) wrote an essay that I found very
stimulating.  He never published it, as far as I know, but it was fairly
widely circulated.  One of the issues he raised was why in the world anyone
would think that the axiom of full replacement was true on the cummulative
conception.  As I recall, he said that the intuitive cumulative picture
justified only Sigma_1(Power) replacement.  Maybe he has changed him mind
since then, but in the essay he looked for ANYTHING in mathematics that
used more than that.  The only thing he could think of as a candidate was
Hanf's proof for the existence of the Hanf number of, say, second order
logic.  Harvey conjectured that the existence of this cardinal was not
provable with just Sigma_1(Power) replacement.  I was thrilled to prove a
conjecture of Harvey's (The Hanf Number of Second-Order Logic.  The Journal
of Symbolic Logic 37 (1972): 588-94).  Harvey later improved by showing
that if k is the HN of second order logic then V(k) is a Sigma_1(Power)
submodel of V.  (I don't recall the reference for the article.)

The relevance of all this is that it is very hard to find results in
mathematics or logic that take advantage of more than Sigma_1(Power).  I
would be EXTREMELY shocked if Z+Sigma_1(Power) were inconsistent since it
seems to be to be true on the cumulative conception.  I would be surprised
for sociological reasons if full replacement were inconsistent; many very
smart people have tried to prove it so and have failed. But I would not be
shocked or loose faith in the cummulative picture. Nor would I expect
everyday mathematics to change much at all. In the long run, it would be
seen as a refinement of the axioms, the correction of an oversight.

There are relevant discussions of this in Hallet's 1984 book on set theory,
and in a paper by James van Aaken in the JSL in 1986.  The basic point that
both of them make in different ways is that there are two separate
intuitions that are used to justify the axioms of ZF, the cumulative
conception and the doctrine of size.  Some axioms are justified on once
conception, some on the other.  (Maybe Harvey made the point in his essay.
I forget.) Moss and I discuss this further in the final chapter our book on
nonwellfounded sets.  We propose that ZF is the theory of hereditarily
small, cumulative classes, and that Aczel's ZFA is the theory of
hereditarily small classes.  This raises several open questions which we
discuss but do not answer.  One is: what is the theory of cumulative
classes, without the restriction to hereditarily small.  Here is seems that
one can justify Sigma_1(Power) replacement only, as far as I see.

Jon