FOM: clarity

[Randall Holmes]

I'm Randall Holmes, a professional mathematician specializing in
theories of sets and functions related to Quine's NF and in automated
reasoning.

Steve Simpson said:


I guess by now it's clear to all 280 FOM subscribers that the grossly
exaggerated claims of topos theory qua f.o.m. are bankrupt.  I'm not
sure it's worth continuing this.  Maybe I'll continue it, just to show
everyone the extent of the bankruptcy.

(end quote)

No, that's not clear to me at all.  I don't think that McLarty is
being altogether clear, either, but that's difficult without
preparation (on the part of the audience as well as the speaker).
Almost everyone here has plenty of preparation for a discussion of
set-theoretical foundations and probably rather less for a discussion
of category-theoretical foundations.  Even Friedman and McLarty's
undergraduates have been prepared for a certain view of the
foundations.

I should make it clear that I'm not an advocate of category
theoretical foundations myself.  My response, on finding out that
topos-theoretical foundations are essentially equivalent to
intuitionistic type theory, was relief--I understand intuitionistic
type theory, and I don't need to learn another language in order to
think about it.

Simpson:

What replaces the A-(A-B)=A?

(end quote)

Nothing needs to replace it; this equation isn't intuitionistically
valid (I should also remark that I prefer classical logic; but
constructive foundations ARE foundations, and are certainly not
"intellectually bankrupt").  Of course, it is valid in a Boolean
topos.

Simpson:

What replaces the idea that sets are made of elements?

(end quote)

Sets are certainly not "made of elements", even from a set theoretical
standpoint.  The relation of element to set (whatever it is) is not
the relation of a part to a whole (for example, it is not transitive).
If sets were made of elements, we could not distinguish between {a,b}
and {{a},{a,b}} (to give a complex but obviously important example).
This is a crucial foundational point which is often handled in a
misleading way in teaching.

On a more general topic, the use of "function" as the primary
foundational notion instead of "set" is not especially difficult (and
is not a monopoly of category theory).  It is easier to explain sets
as functions than it is to explain functions as sets: a set is a
function whose values are truth values (it is traditional in analysis
to use 0 and 1 instead of True and False as values of "characteristic
functions").  I think that undergraduates have a better (or at least a
wider) acquaintance with functions than they do with sets, and they do
not understand them as sets of ordered pairs; that's a quite
sophisticated idea.

Foundations using functions can be typed (see Peter Andrews, _An
Introduction to Mathematical Logic and Type Theory, to Truth through
Proof_, for a nice presentation) or untyped.  An untyped presentation
is difficult if one wants to get a theory looking like ZFC. I have
presented NFU + Infinity (Quine's "New Foundations" with urelements,
which is consistent with choice and has known models, unlike NF) as a
lambda-calculus; in that theory (which is entirely adequate as a
foundation) one has the advantage that functions can have universal
domain.  A theory like ZFC in which sets could be interpreted as
characteristic functions is certainly possible, but I'm not aware of a
formal presentation of such a theory.  An approach which I'm fairly
certain would work would be to use functions which are "almost
everywhere constant" (i.e., constant everywhere except on a set in the
usual sense).

An interesting aspect of foundations based on functions is that the
logical notions can be defined in terms of the primitives of
lambda-calculus (the basic formalism for defining functions); the root
logic of a mathematical foundation based on functions does not need to
be first-order logic, but can simply be equational.  See the
development in Andrews's book.


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