FOM: necessity of schemes?

[Randall Holmes]

(Harvey Friedman wrote:)

In fact, the axioms you wrote down are not only very clumsy in comparison
to standard axioms for set theory, they also are unusable as formal f.o.m.
For example, as I have said on the fom, I do not believe that one can
actually conveniently formalize mathematics in any formal system without
schemes. This is because mathematicians routinely use mere expressibility
(by wffs) as a sufficient criterion for object formation (i.e., forms of
comprehension), and do not carefully break up the relevant wffs into their
componenents and successively build up terms or introduce symbols by
definition for the components. This feature of the formalization of
mathematics is well known to people who actually do formalization of
mathematics - e.g., the Mizar people.

(end quote)

I agree with Friedman that principles with the strength of schemes are
needed.  But there is the obvious alternative approach (which would
presumably be used in topos theory, and which I actually do use in my
pending NFU monograph):  give the axioms needed to build sets corresponding to
wff's step by step, then prove and subsequently use a meta-theorem which
gives the strength of the desired scheme.  A system as strong as ZFC was
presented in this way by von Neumann in 1925. 

The practical power of schemes is essential (I learned this the hard way,
by attempting to use combinators instead of lambda-abstraction in a theorem
proving project; even with automated support for synthetic abstraction and
reduction, it isn't feasible).  But this does not militate in favor of
schemes rather than meta-theorems.

Of course, if one is committed to ZFC, one needs axiom schemes, since
ZFC cannot be finitely axiomatized.  But ZFC with proper classes
(treated predicatively) can be finitely axiomatized (as shown by von
Neumann).  So can Mac Lane set theory (bounded ZFC).  So the option
exists of doing mathematics without schemes but without disregarding
the true and important observation that we don't want to build
abstractions over wffs (or terms) by tedious recursions on the
structure of the wffs or terms.

It seems to me that this is a fine outcome from a foundational perspective:
one gets a very simple list of axioms on the one hand and (after a one-time
investment in proving a meta-theorem) the power of a theorem (rather than
axiom) scheme.  One does need the ability to handle meta-reasoning
and theorem schemes; but I do not see that one needs axiom schemes unless
one is committed to a specific theory that is not finitely axiomatizable.
Either von Neumann's system or Mac Lane set theory are perfectly respectable
f.o.m., though the latter is weaker than some may prefer.

And God posted an angel with a flaming sword at | Sincerely, M. Randall Holmes
the gates of Cantor's paradise, that the       | Boise State U. (disavows all) 
slow-witted and the deliberately obtuse might | holmes at math.idbsu.edu
not glimpse the wonders therein. | http://math.idbsu.edu/~holmes