[FOM] Re: A new foundation for abstract mathematics

[Bill Taylor]

I think a fascianting post and a wonderful start have been made by
Michael Makkai <makkai at math.mcgill.ca>, who writes:

> As to the language, first, the *object-*language has to be fully
> explicit: it has to be  *formal*. (The metalanguage is quite optional,
> of course: one is free to discuss metalinguistically the System in any way
> one wants to.) Secondly, and just as importantly, the language has to be
> *right*, that is, expressive: merely *coding* what we have in mind is
> no good; we have to *say* what we mean. I would like to refer to
> what was said in this paragraph as *Frege's imperative".

I hadn't realized this was a core theme of Frege, though now that you
mention it, it does seem very plausible.

And anyway, I like your expression of it.  Good paragraph!

> The basic characteristics of type theory is the acceptance of the presence
> of fundamentally different kinds of the entities, whose relations to each
> other are mediated by a substantial additional equipment. The language
> of type-theory is burdened with "type-discipline": an ever-present need
> to acknowledge the specific types of entities the discourse is about.
> Type theory gives up the hope that the world can be explained
> as consisting of elements ultimately of the same nature.
> It resigns itself in the irreducible variety of the world,
> and tries to find solace in the unfolding panorama of this variety.

This is an excellent description of type theory, and a very nice summary
of the attitudes involved in adopting it.   Thanks for that.

> One may say that type theory is a "physical theory" of the abstract:

Beautiful!  This is good enough to steal for a sig, and I will in due
course adapt it so.  Mind you, I think your sentence could be applied
not just to Type Theory, but to Formalism as a whole!

> "physical" in that it accepts abstract entities as given in and by
> the world, rather than generated by idealized mental acts. In contrast,
> the conception of totality as *class*: as the result of *comprehending*
> entities that answer a description (have a property) into a totality,
> would have place in a "conceptual", "non-physical", attitude.

This is also clearly presented, but I'm not quite so sure I'd go along
with distinguishing "sets-with-only-urelements" and "comprehension-sets"
as typifying "physical" and "abstract".  Perhaps "mathematical" v "logical",
or just "C19" v "C20" would be better?

> I think, in one way or another, all of us are still in the shock from
> the crash, exemplified by the Russell paradox, of the unbridled conceptual
> attitude.  Type theory is shock management: it is an inherently cautious,
> piecemeal approach. It does have its satisfactions though.

Wonderfully well put.

> Abstract sets are well-known to logicians: they are sets consisting of
> *urelements* (atoms, points) alone. I think, this notion of "set" is
> the "original" idea of set. (It is something distinct from the concept
> of "class": see above. Modern set theory fuses the original concepts
> of "set" and "class", to separate them again at a new dividing line.)

Yes; moving from "sets-with-only-urelements" to "cumulative-sets"
(with its implied inclusion of well-foundedness) was perhaps the defining
moment of the acceptance of these new ideas as part of standard math.

And as you imply, the new division, between well-founded cumulative sets
on one side, and classes by unbridled comprehension on the other,
has never really been smoothed over enough for the latter to gain full
acceptance by the math community.  Russell nervousness still haunts us!


If I have any criticism, perhaps I may note that the more nitty-gritty
matters you started on, involving Set El Eq and so on, seem a little bit
cumbersome somehow; but that is probably partly inevitable in any Type
approach, maybe exacerbated by writing out in full, thereexists, forall etc

But still, a very good start, and I warmly encourage you to continue with
the projected articles.

------------------------------------------------------------------------------
        Bill Taylor                     W.Taylor at math.canterbury.ac.nz
------------------------------------------------------------------------------
             Formalism:  the physical theory of abstract objects.
------------------------------------------------------------------------------