Re: categorical foundations

[Andre.Rodin@ens.fr]

Selon Colin McLarty <colin.mclarty@case.edu>:


CM: Andre.Rodin@ens.fr Suggests a better take on CCAF than the one he has been
taking.  That would be a take based more on Bill's published work on CCAF, and
less on the philosophical objection that Geoff Hellman used to make about
CCAF.  Geoff himself has given up this objection.


AR: I don't know about Hellman's objection about CCAF and would be grateful for
the reference. Talking about CCAF I mean first of all Bill's 1966 paper
(leaving aside the problem noticed by Isbell as irrelevant to my story), rather
than later versions of CCAF.

I don't quite understand what does it mean a "better take" but if this means my
argument then this argument is based on its own (as, in my understanding, any
philosophical argument should be) but not on  works of other people.


CM: This is the Hilbert conception where axioms are not asserted as true
but offered as implicit definition; and so they are not about any
specific subject matter but may be applied to whatever satisfies them.

Lawvere from 1963 on has always been clear that his first order axioms
ETCS and CCAF can be taken this way for metamathematical study -- but
that he does assert them as true specifically of actual sets and
categories.   (Now Bill is not talking about any idealist truth or
objects.  He takes a dialectical view.  But that is another topic.)


AR: This is an interesting aspect of the issue, about which I didn't think
earlier. It might have a bearing on what I'm saying but so far I cannot see
that it does. I am saying this: the axiomatic method in its modern form  -
which has been pioneered by Hilbert (among other people including Dedikind, et
al. ) and then further developed by Zermelo, Tarski et al.) - involves a
preformal notion of set or collection. Whatever first-order theory is built by
this method objects of such a theory form preformal sets. In particular, when
this method is used for building ETC then primitive objects of this theory
called "morphisms" form preformal sets called "categories". In THIS sense the
preformal notion of set remains a foundation of ETC.
As far as I can see this situation doesn't depend on whether one thinks about
axioms of ETC (or any other first-order theory) as assertive or as implicit
definitions.


CM: But even take the interpretation corresponding to any one object A of
CCAF.  That amounts to specifying X as A in the parametrized
interpretation.  This interpretation does not deal with "the
collection of objects of A" and "the collection of morphism of A".  It
never refers to any such collections.  It deals with categories
A,1,2,3, and functors among them.



AR: Right. This is exactly the reason why I say that CCAF has two
well-distinguishable foundational "layers". At the first layer (ETC) a category
is a collection of morphisms; at the second layer (i.e., in the core fragment
of CCAF called in 1966 paper "basic theory" ), as you rightly notice, a
category is no longer a collection. My problem with this is actually twofold.

(1) The second layer depends on the first but not the other way round. Formally
speaking, this simply amounts to the fact that axioms of ETC are axioms of BT
but not the other way round. In THIS sense, once again preformal sets remain a
foundation of CCAF.

(2) The joint between the two layers remains for me unclear. From a formal
viewpoint this looks trivial: CCAF is ETC plus some other axioms. But this
doesn't explain the switch from thinking about categories as collections to
thinking about categories as identity functors. In Bill's 1966 paper this
switch is described as a new terminological convention made in the middle of
the paper (that cancels the earlier convention). This change of notation points
to but doesn't really addresse the issue, as far as I can see.




CM:  you would do better to notice the novelty of these parametrized
and single-category interpretations of ETC in CCAF and take this as
the kind of major change that you expect to see.


AR: I do see this as a great novelty.  But I claim that this novel approach in
the given setting (i.e. in CCAF) doesn't work *independently* of the older
approach; moreover there is a sense in which the older approach remains basic
while the new one is a "superstructure".


CM: This different axiomatic method is explicit in CCAF, and does work
independently there. Specifically what is supposed to "not work" about it?

AR: To sum up. ETC is built with the older Hilbert-Tarski's method. CCAF as a
whole involves a genuinely new idea of how to build mathematical theories , I
agree with you on this point. But since ETC is indispensible in CCAF - and
morever since ETC is a starting point of CCAF  the new categorical axiomatic
method in the context of CCAF does not work *independently* (I am not saying
that it doesn't work at all.) This is why I say that CCAF is only a half-way to
genuinely categorical foundations of mathematics (that is only natural in case
of such a pioneering work as Bill's 1966's paper).

For a possible development of CCAF into a better categorical foundation my hopes
are for  developing the diagrammatic reasoning of the second layer of CCAF into
a genuine logico-mathematical synatax, which could serve independently of the
usual first-order syntax.
I'm particularly interested in this respect in recent work of Charles Wells,
Zinovy Diskin, Dominique Duval, René Guitart and other people. Actually I would
be quite interested to hear from these people what they think about a possible
relevance of their work to foundations of mathematics and, more specifically,
to CCAF.

A more general point: in my understanding, a dialectical attitude to foundations
amounts to looking at them as a subject of further rebuilding - rather than
looking at them as what is  accomplished in principle and needs only  working
out some further  technical details.


best,
andrei



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