Re: topos and magic

[Colin McLarty <colin.mclarty@case.edu>]

I get to André Rodin's comments, and the redoubtable John Mayberry, below.


2009/11/12 Joyal, André <joyal.andre@uqam.ca>:

Writes what I entirely agree with:

> I am convinced that categorical logic, which was wholly invented by Lawvere,
> is the most important development of logic during the second half of the 20th century.
> I find the notion of elementary topos absolutely extraordinary, almost magical.

I only mean it is not extraordinary that with enough time the
developments become generally known.

> Like every important mathematical discovery, it stands out as a colorful gem on a bed of grey stones.

This imagery makes perfect sense to me, for many great examples such
as the complex numbers as André described.  But I don't know if I
could convey it to many philosophers of mathematics even in the most
general terms -- let alone convince them anything to do with category
theory is an example.   Most philosophers, so far as I know, still
consider the complex numbers far-fetched and "impossible to visualize"
(which I find incredible).

> I find astonishing that ETCS should be closely related to topos theory
> via the notion of an elementary topos.
> It is also surprising that the internal logic of a topos
> should be formally identical to intuitionistic set theory.
> The construction by Hyland of the realizability topos is also extraordinary
> because of the connection with recursive function theory.

Yes.

And I agree with what André said earlier that there is room here for
possible further insights into what remain profound mysteries about
the hierarchy of infinite cardinals.  (I do not claim to currently
have those insights!)


> One may argue that there is nothing magical in mathematics,
> since mathematics is rational by nature. I disagree.
> We are far from understanding completely the natural world,
> and mathematics is not a pure construction of the rational mind.
> Mathematicians are probing in the depth of a highly structured unkown.
> If we are patient and lucky enough we may catch a gem.
> The gem has a structure of its own and we can learn from it.
> This is were the magic is.

I am not happy to call it "magic" -- I collected rocks as a teenager
and once did catch a "gem" (a thick tuft of pink-grading-to-green
byssolite hairs with bright pyrite crystals suspended in them, 4 feet
down a gray rock crevice that I could barely crawl into) but I do not
call that "magic" either.  Perhaps this is mostly a difference over
words.


2009/11/12  <Andre.Rodin@ens.fr>:

writes

> I do NOT believe that ETCS and CCAF "work perfectly well". Each of these involve
> two foundational "layers", namely, the classical "bottom" and a categorical
> "superstructure". By the classical bottom I mean NOT an underlying Set theory
> but the "Elementary theory of categories" (ETC), i.e. a theory of categories
> using the usual First-Order Logic (FOL) and relying on the standard
> Hilbert-Tarski-style axiomatic method. I agree with John Mayberry and some
> other people who argue that this aximatic method alone assumes a basic notion
> of set or collection.

Mayberry says two things about this.  The first, which has taught me a
lot, is his stress that no formalization can be the basis of our
actual knowledge of mathematics.  This applies to all formalized
foundations.  Mayberry's point is precisely the reason why I say that
ETCS and CCAF " work perfectly well, in formal terms."  It is a plain
fact that these axioms work as well as the formal ZFC axioms --- while
Mayberry is right that formalized axioms cannot be the real basis of
our knowledge.

I believe John has underrated the dialectical relation between
formalization and "the real basis of our knowledge."    I have often
discussed this with him and I am not sure exactly what he thinks about
it now.   Formal investigation of ZFC has changed our actual beliefs
about sets.  Category theory has further changed our actual beliefs
about mathematics, and formal investigation of ETCS and CCAF has been
part of this.

But the key point is that ETCS and CCAF are not only formal axioms,
any more than ZFC is.  All are formalizations *of* our real beliefs
about sets and categories.

These real beliefs do not "assume a basic notion of set or collection"
but rather *include* or *express* a basic notion.

The next thing John says is that our basic notion of collection is
best captured by ZFC.  (Or, rather, he used to say that prior to
developing his finitary set theory as an alternative foundation.)   I
say ETCS formalizes almost the same idea of set, but better than ZFC.
The ETCS formalization is rather like the ZFC one, but omitting a lot
of irrelevancies about transfinitely iterated membership.  Zermelo and
then Fraenkel and Skolem found these in the first attempts at
axiomatization and I don't say i could have done better in 1908 or
1922.  I say Eilenberg and MacLane's work of 1945 enabled Lawvere to
do better in 1963.

But even before Bill did that he had already seen that our basic
notion of collection is not so much like that.  It is typified by,
say, the continuum, or the collection of Euclidean motions of the
plane, and such.  Our basic notion of the continuum is not that the
discrete collection of points on it is equinumerous with the powerset
of the natural numbers, and it is equipped with a lattice of open
subsets -- our "basic notion" of it is rather a somewhat open-ended
notion of continuous translation.

The basic notions are in fact not very articulate in themselves, and
throughout the history of mathematics it has taken further ideas to
articulate them.  Bill saw how to articulate these and many more,
quite directly, in categorical terms not assuming any prior set
theory.  That articulation works even if you do not take it as
foundational.  But it gets a natural foundational character in the
framework of the category of categories -- thus CCAF, the axiomatic
theory of the category of categories as a foundation.

best, Colin





Unlike Mayberry I don't think that this fact implies that
> the project of categorical foundations, as a alternative to and replacement for
> set-theoretic foundations, is futile. Recall that the axiomatic method we are
> talking about (which is, of cause, quite different from Euclid's method and
> other earlier versions of axiomatic method) emerged together with Set theory.
> In order to make categorical foundations into a viable alternative of
> set-theoretic foundations we still need to provide Category theory with a new
> axiomatic method rather than use the older axiomatic method as do ETCS and
> CCAF. Elements of this prospective axiomatic method are found in what I just
> called the "categorical superstructure" of ETCS and CCAF but as far as these
> theories are concerned the classical background (FOL+ETC) is indispensable.
> This is why I say that ETCS and CCAF do NOT work perfectly weel as categorical
> foundations.
> Building of "purely categorical" foundations remains an open problem. It is not
> a matter of a ideological purity but a matter of complete "rebuilding" (Manin's
> word) of foundations: in my view, such a rebuilding is healthy and refreshing
> in any circumstances (unless it clashes severely with practice).

>
> best, Andre
>

[For admin and other information see: http://www.mta.ca/~cat-dist/ ]