FOM: Alternatives to ZFC in actual use

[Lawrence N. Stout]

Partly because of reference on this list I recently bought and read
Bell's book _A Primer of Infinitesimal Analysis_ and thought again about
the work on synthetic differential geometry by Anders Kock (_Synthetic
Differential Geormetry_, London Math Society Lecture Notes 51, Cambridge
U Press), Gonzalo Reyes, Eduardo Dubuc and others on which it is based. 
This work provides another answer to the question 

Kanovei wrote:
> 
> Is there any known statement A such that
> 
> 1) A is a meaningful mathematical statement
>    (e.g., NOT of the form Con ZFC)
> 2) A is formalizable in set theoretic language
>    (e.g. NOT on existence of some "universe")
> 3) A is NOT provable in ZFC
> 4) A is provable in ZFC + "universes" or "topoi" or the like.
> 
> ?
> 
> V.Kanovei

The statement A would be "there exists a ring of line type"  which is
inconsistent with the law of the excluded middle.  Hence A satisfies
Kanovei's requirement 3).

Bell and Kock make a good case for infinitesimal analysis using
nilpotent infinitesimals in a ring of line type having mathematical
meaning.  It captures fairly well the intuition used by the founders of
calculus.  Bell in particular shows how standard applications in
Newtonian physics are easily developed using nilpotent infinitesimals. 
This makes a case for requirement 1).

The properties which make a ring "of line type" are formalizable in the
usual set theoretic language of algebra.  The key axiom is that if D is
the subobject of those x in R with x^2=0, then R x R is isomorphic to
R^D. This makes the existence of a ring of line type meet Kanovei's
condition 2).

To meet condition 4) what needs to be done is to construct a topos in
which there is a ring object of line type.  That is what Dubuc did.  Now
the construction starts with the category of smooth manifolds Man and
then constructs subcategories of functor categories based on Man.  Thus
it deals with very large categories.  Using classical logic Dubuc
demonstrated that there is an object in the resulting category which
looks from inside the topos like a ring of line type.  I suspect that
this construction would be hard to formalize in ZFC without using
universes to restrict the size of the categories produced, though few if
any current categorists would worry about the details of how to give set
theoretic foundations, preferring elementary descriptions to
heirarchical ones.

It seems to me unlikely that one can settle questions in foundations by
looking in the index of standard texts.  Almost none will mention the
rank of sets or the distinction between sets and proper classes. 
Johnstone's book on Topos Theory doesn't have an entry in its index for
Grothendieck universes.  Most mathematics books are concerned with
mathematics, not fom.  This does not mean that their contents fail to
make use of foundational concepts, nor does it mean that analysis of
what strength is actually needed to carry out their constructions is
completely known.

Another example related to Konovei's question is the Moore conjecture on
metrizable spaces.  I do not remember the details, but I do remember
that the existence of counterexamples to the Moore space conjecture
depends on large cardinal axioms.



-- 
Lawrence Neff Stout
Professor of Mathematics
Illinois Wesleyan University

http://www.iwu.edu/~lstout

"Fiddling is a viol habit." Anon?
"Dancing is necessary for a well ordered society." Thoinot Arbeau