Re: Re: categorical foundations

Re: Re: categorical foundations

[Colin McLarty]

2009/11/15  <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: True, the most general notion of “collection” one can imagine may cover
> “category” and what not. But, I claim, the preformal notion of collection
> *relevant to the axiomatic method in its modern form* is more specific, and
> does NOT cover the preformal notion of category. I’m talking about “systems of
> things” in the sense of Hilbert 1899 rather than sets in the sense of ZFC or of
> any other axiomatic theory of sets.

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.)

> In ETC (the Elementary Theory of Categories in the sense of Bill’s 1966 paper)
> categories are conceived as collections of things called “morphisms” provided
> with relations called “domain”, “codomain” and “composition” (I hope I nothing
> forgot).

This is one use of ETC, and indeed a use made daily in mathematics.
But it is not the use in CCAF.  The fragment of CCAF you are calling
ETC is asserted of specific things.  Bill says it deals with: "the
category whose maps are ‘all’ possible functors, and whose objects are
‘all’ possible (identity functors of) categories. Of course such
universality needs to be tempered somewhat."  The requisite tempering
is very like that familiar in set theory, and Bill describes it.  (The
quote is his dissertation p. 26 of the TAC reprint.)


> Even if there are pragmatic reasons to build
> theories of sets like ETCS and other mathematical theories on the basis of ETC
> rather than use axiomatic theories of sets like ZFC for doing category theory
> and the rest of mathematics, this doesn’t change the above argument.

What does change it though, is the interpretation of ETC in CCAF. That
interpretation does not use The "Hilbert conception."

Actually, it is best regarded as a single interpretation with a
parameter: interpret "object" in the ETC axioms as "functor from 1 to
X" where X is a fixed free variable of identity functor type in CCAF,
interpret "morphism" as "functor from 2 to X" and so on always with
the same free variable X.  Interpreting the ETC axioms in CCAF this
way is not at all treating them in the Hilbert way.

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.

If you want to push this line:

> Every major historical shift in foundations
> of mathematics so far involved a major change of the notion of axiomatic
> method. (I can substantiate the claim if you'll ask.)

Then 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 called ETC “formal basis” of BT (“Basic Theory of Categories” in the
> sense of Bill’s 1966’s paper) meaning the two-level structure of BT. BT is ETC
> plus some other axioms. Conceptually the order of introduction of these axioms
> matters. My point (or rather guess) is that BT involves a prototype of a
> new axiomatic method (different from one I described above), which, however,
> doesn’t work in the given form independently.

This different axiomatic method is explicit in CCAF, and does work
independently there.

Specifically what is supposed to "not work" about it?  Is it supposed
to be formally inadequate to interpreting mathematics?  (That is a
non-starter, and even Feferman only made vague hints that it was so
and never tried to fill them in.)   Is it not really comprehensible?
(Bill comprehended it already around 1960, and so do many of us now.
Feferman argues well that he does not comprehend it, but falsely
concludes that no one can.)

best, Colin


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

Re: categorical foundations

[Charles Wells]

This is the right attitude toward doing math.

You can work away with the axioms for categories without caring about
models of the axioms, unless you try to do certain things such as for
example take a limit over all the diagrams of a certain kind in the
category.  Then you have to think about foundations.

You can check what logical constructs you have used in a mathematical
argument, and then maybe you will see you have not used the axiom of
choice or excluded middle, so your models can live in many toposes.

And so on.

This is "just in time" foundations: think about foundations when you
have to, not before.  That is really what most of us do most of the
time.

Charles Wells

On Mon, Nov 16, 2009 at 8:54 AM, Colin McLarty <colin.mclarty@case.edu> wrote:

>
> 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.


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

Re: categorical foundations

[Andre.Rodin]

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/ ]