[FOM] From theorems of infinity to axioms of infinity

[Nik Weaver]

Mort Dowd wrote:

> Regarding point 2, I'm not an expert, but there is a thriving body of work
> on how much of classical mathematics can be formalized in PA, and also
> subsystems of second order arithmetic,  This is a specialized topic,  though,
> because infinity and power set give the cumulative hierarchy, which  allows
> formalizing the real numbers without any of the "tricks" needed to  formalize
> in weaker systems.

Mort,

This is about the worst example you could use to make this point.  Unless
your formal system takes the real numbers as primitive, you will need some
kind of coding machinery to model them.  Probably the formally simplest
way to encode reals in ZFC is as Dedekind cuts of rationals, which are
themselves equivalence classes of ordered pairs (encoded by Kurtowski's
"trick") of natural numbers (encoded as ordinals by von Neumann's
"trick").  One uses substantially *less* trickery to encode real numbers
in subsystems of second order arithmetic because sets of natural numbers
are already built into the formalism.

You would be better advised to talk about encoding structures on the
level of sets of reals, where the language of set theory has a clear
advantage over the language of second order arithmetic.  But this is
not a fair comparison because people like me who reject the power set
axiom have no qualms about the language of third order arithmetic; we
just think of the third order variables as representing classes.  I
have explicitly shown how to formulate standard measure theory and
functional analysis in such a system; see

http://arxiv.org/abs/0905.1675

If you wanted to formalize arbitrary sets of sets of reals, then my
system would not be so good.  But then, it is not so easy to think of
structures of real importance in mainstream mathematics that require
this.  So I think the point actually goes against you: ZFC goes way
beyond what is needed for ordinary mathematics, and in doing so it
admits a raft of nonseparable pathology of no obvious interest.  If
the standard of judgement is based on formalizing normal mathematics,
then we are better served by the more elementary systems which are
fully adequate to this task, involve coding machinery which is no
more complicated than what we encounter in ZFC, and avoids the
metaphysical extravagence of ZFC which has no clear philosophical
justification and merely makes room for pathological structures we
don't care about.

Nik Weaver
Math Dept.
Washington University
St. Louis, MO 63130
nweaver at math.wustl.edu