FOM: alternative foundations

[Randall Holmes]

This posting is from M. Randall Holmes.

(I quote Friedman, Sun, 25 Jan 1998 18:26:15 +0100)

Classical logic is the major way to do foundations of mathematics. Other
logics are normally used to formalize interesting restrictions on proofs
for many diverse foundational purposes and investigations. For instance, in
many contexts, if a proof is based on intuitionistic logic then we can
immediately deduce certain kinds of algorithmic information. Also in many
contexts, there are good reasons for looking at intuitionsitic logic since
it seems to correspond to a robust, informal conception - and this can be
backed up by important theorems.

The "logic" one is operating under is appropriately placed outside the
formalization - not enmeshed with mathematical objects. So from the point
of view of genuine f.o.m., what you wrote is philosophically incoherent.
You are confusing some sort of formal algebraic treatment of logic with
logic itself. This is a typical conceptual error of categorical
foundationalists. E.g., Lawvere told me that the existential quantifier is
not only best understood as some sort of map or functor (or other more
complex categorical object) - but can only be properly understood that way.

(end quote)

There are of course mathematicians working in foundations (not
including myself) who believe that intuitionistic logic is the
_correct_ logic.  Their work is still foundational.  Some of these
think that the proper notion of what a proof is is unavoidably meshed
with mathematical objects; some of them think a proof _is_ a
mathematical object.

There are mathematicians (including myself) who do not think that the
universal and existential quantifiers _must_ be primitive notions.
They are economically definable in terms of abstraction (of functions;
set comprehension will also work) which can reasonably be taken as a
primitive idea.  "for all x, P" can be understood quite economically
as "(\lambda x)(P) = (\lambda x)(True)", or "{x|P} = V".  I certainly
wouldn't say that it _must_ be understood this way, but it _can_.  We
certainly invite beginning calculus students to accept definition of
functions or sets by abstraction as a primitive.  There are formal
algebraic treatments of logic which are very hard to imagine as
anyone's pre-formal logic (I have in mind such things as cylindrical
algebra and (even worse) Quine's predicate functor logic or calculus
of concepts).  This objection does not apply to the kind of treatment
implemented in categorical foundations (I have been re-reading Lawvere
and Scott on this, since I am not a practitioner (or even an advocate)
of categorical foundations).

I can testify from my own experience that I do in fact regard the
quantifiers (some of the time) as (very simple) composite notions
defined in terms of abstraction; I am usually more comfortable with
equational logic as the root logic.  One mathematician's "formal
algebraic treatment of logic" may be another's actual logic.  It is a
question of psychology what is possible in this area; I know by
introspection that reducing quantifiers to function abstraction can be
"pre-formal".  I doubt very much that cylindrical algebra is anyone's
pre-formal logic.  I think that the analysis of the notion of
abstraction (psychologically primitive for me, at least) in
combinatory logic is mathematically useful in understanding this very
complex notion, but I have to admit that combinators are not
psychologically primitive for me.  (Is combinatory logic f.o.m.?  If
not, why not?)

I think that some people do think naturally in terms of categories (I
don't), just as some people do think naturally in terms of
constructive logic.  There does appear to me to be a foundational
notion under the category theoretical approach, combined with a
methodological stricture.  A category represents a kind of structure
(mathematics can reasonably be regarded as the study of structures);
its objects are the structures themselves and its morphisms are
transformations appropriate to the kind of structure under
consideration.  The methodological stricture is that one does not
investigate the "inside" of a structure; one motivation for such a
stricture can be found in the "abstract data type" considerations
mentioned in an earlier posting of mine and commented on by Friedman;
one only discusses transformations between structures, and one
expresses the properties of a particular kind of structure in terms of
statements about the transformations between its instances.

What kind of structure is captured by topos theory?  Exactly the same
structure that is described by intuitionistic type theory.  The types
in a particular intuitionistic type theory are both implementable as
sets (under a nonstandard logic) and are "structures characterizable
in terms of the properties of the admissable transformations between
them" (my characterization of the primitive notion underlying
categorical theory foundations as I understand them).  There is
nothing to prevent mathematicians with different approaches to the
foundations of mathematics from talking about the same things.

I think that the reason that Friedman doesn't think that category
theory can be foundational is that he doesn't believe that anyone
really can think that way.  I think that one can learn to think
categorically with practice; like Friedman, I prefer to think in terms
of set (or function) theory (I prefer to look at structure from the
inside rather than (or as well as) the outside).

The question of what f.o.m. is appears to be psychological for
Friedman; he admits that it is possible to interpret intuitionistic
higher order logic, which certainly is a candidate foundation for
mathematics, in topos theory; in fact, topos theory is essentially
equivalent in a formal sense to intuitionistic type theory, so the
issue cannot be formal.  Alternatively, Friedman may admit the
possibility of thinking in ways which are deviant from his standpoint,
but regard them as violating a natural hierarchy of concepts to which
we all are supposed to adhere (comments invited?)

It should be remembered that the current foundational scheme in terms
of first-order logic and ZFC is both new (no hint of it existed in
1800, at which time mathematics was already very much a going concern)
and not unanimously accepted (there are still constructivists, for
example).  Thus it is quite doubtful that either human nature or
nature per se requires us to found mathematics on the set concept or
even on first-order logic as currently formulated.

I really wish that some category theorist would take Friedman up on
the challenge regarding presenting axioms for topos theory; it looks
to me from reading Lawvere and Scott as if the list would be only
slightly longer than Friedman's, and logically much simpler
(separation and replacement are _not_ formally simple).  Unfortunately,
while Lawvere provides axioms for a cartesian closed category in
equational form, he doesn't seem to provide the axiom(s) for the
subobject classifier in that form.  Categorical foundations are not to
my taste, but they certainly are foundations, and they can be
interpreted as being based on a coherent concept of what mathematics
is about.

My actual view is that mathematics is "about" formal structures,
concerning which there are objective truths (whether or not the
structures are taken to be abstract objects of a special kind).
Mathematical truth is not truth about human beings (specifically) or
created by human activity.  There is no reason to believe that all
mathematical truths are accessible to human beings.  There are a
variety of ways to approach the study of formal structure; some (such
as set theory) can be taken as subsuming all or most others.  Like
Friedman, I think that set theory is such a universal approach.
Unlike Friedman, I think that there may be other fundamental
approaches, universal or partial, which can be practiced quite
independently of set theory.  A set theorist may find it difficult to
understand what a practitioner of a different approach is doing
without appealing in his/her own mind to set theory, but that does not
mean that the other is doing set theory.

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