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

Re: categorical foundations

[Andre.Rodin]

Hi Colin,
here are my answers to questions you asked me in your last two postings (living
now our terminological misunderstanding aside).


CM: Do you mean that every formalized axiom system uses arithmetical
notions such as "finite string of symbols."  This is why that formal
axioms cannot be the real basis of our knowledge of math, but it has
no more bearing on categorical axioms than any others.

AR: No I did not mean this. Agree that this argument has no more bearing, etc.


CM: Or do you think that pre-formal notions of "set" or "collection" are
all based on iterated membership and Zermelo's form of the axiom of
extensionality, so that CCAF is less basic than ZFC?  That is a common
belief among logicians who have not read Zermelo's critique of Cantor
(where Zermelo points out that Cantor did not hold these beliefs) and
who know a great deal more of ZFC than of other mathematics.


AR: No. I certainly do NOT think that pre-formal notions of "set" or
"collection" are all based on iterated membership and Zermelo's form of the
axiom of extensionality. I explain in the next entry what I do think about this
matter.



CM: In fact, long before mathematicians could analyze the continuum into a
discrete set of points plus a topology, they were well aware of
collections like the collection of rigid motions of the plane -- and
that "collection" is a category.  It is not just a ZFC set of motions
but comes with composition of motions and with an object that the
motions act on.


AR: True, the most general notion of “collection” one can imagine may cover
“category” and whatnot. But, I claim, the preformal notion of colection
*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. The idea of *this* axiomatic method (not to
be confused with other versions of axiomatic method like Euclid’s) is, very
roughly, this. One thinks of collection of “bare” unrelated individuals and
then introduces certain relations between these individuals through axioms.
Objects of a theories obtained in this way are sets provided with relations
between their elements, i.e. “structured sets” (or better to say “structured
collections”.

The principal feature of the preformal notion of collection involved here is
that elements of such a collection are unrelated. Because of this feature the
collection in question is not a general category. (It might be perhaps thought
of as a discrete category but this fact has no bearing on my argument.)
The idea of building theories *of sets* using the version of axiomatic method
just described is in fact controversial: it amounts to thinking of sets as bare
preformal sets provided with the relation of membership. I mention this latter
problem (which is not relevant to my argument) only for stressing that the
notion of set or collection I have in mind talking about categorical foundation
is NOT one that has any specific relevance to ZFC or any other axiomatic.

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). The notion of collection involved in this construction  is MORE BASIC
than the resulting notion of category simply because this very axiomatic method
is designed to work similarly in different situations - for doing axiomatic
theories of sets and of whatnot. 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.

CM: What is a "formal basis" of a theory T?  

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 BC. BC is ETC plus
some other axioms. Conceptually the order of introduction of these axioms
matters. My point (or rather guess) is that BC involves a prototype of a new
axiomatic method (different from one I described above), which, however,
doesn’t work in the given form independently. I’m not quite prepared to defend
any general notion of formal basis - I didn’t mean to introduce such a general
notion and didn’t think about a general rule.

CM: The Eilenberg-MacLane axioms are a subtheory of CCAF and also have a
natural, conceptually central interpretation in CCAF.  I consider this
an insight, Bill's insight, and I do not see how it becomes any kind
of objection to CCAF.

AR: The subtheory you are talking about is what I call ETC in these postings,
right? I hope I understand it coorectly what you mean by "natural, conceptual
central interpretation in CCAF" - the fact that any object in CCAF is a model
of ETC, right? Now, the objection is this:
ETC involves the preformal notion of collection that can NOT be thought of as a
category (for the reason I tried to explain above).

In addition to the above argument my conclusion about CCAF is also based on the
following historical observation.  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.) But ETC (and, formally
speaking, the whole of CCAF) relies on the old Hilbert-Tarski-style axiomatic
method.

best,
Andrei






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

Re: categorical foundations

[Colin McLarty]

Sorry.  I did misunderstand that.  But I still do not understand it.

What is a "formal basis" of a theory T?  Is any subtheory of T?  Or is
it any conceptually significant subtheory?  (In the latter case I
would not call it a "formal" basis.)

Is it supposed to be a general rule that if a theory T has a "formal
basis" then T cannot be a satisfactory foundation?

The Eilenberg-MacLane axioms are a subtheory of CCAF and also have a
natural, conceptually central interpretation in CCAF.  I consider this
an insight, Bill's insight, and I do not see how it becomes any kind
of objection to CCAF.

best, Colin



2009/11/13  <Andre.Rodin@ens.fr>:
> Selon Colin McLarty <colin.mclarty@case.edu>:
>
>> 2009/11/12  <Andre.Rodin@ens.fr>:
>>
>> writes
>>
>> >  ETCS is the formal basis of CCAF.
>>
>
>
> I did NOT write this. I wrote "ETC is the formal basis of CCAF", please check my
> message. By ETC I mean the Elementary Theory of Categories. (You might take my
> ETC for a typo perhaps.)
>
> best
> Andrei
>


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

Re: categorical foundations

[Andre.Rodin]

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

> 2009/11/12  <Andre.Rodin@ens.fr>:
>
> writes
>
> >  ETCS is the formal basis of CCAF.
>


I did NOT write this. I wrote "ETC is the formal basis of CCAF", please check my
message. By ETC I mean the Elementary Theory of Categories. (You might take my
ETC for a typo perhaps.)

best
Andrei


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

Re: categorical foundations

[Colin McLarty]

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

writes

>  ETCS is the formal basis of CCAF.

This is simply false.  On some versions ETCS is a part of CCAF but
even then it is in no sense prior to other parts.

> ETCS relies on a pre-formal
> notion of set or collection just like ZF or any other axiomatic theory built
> with Hilbert-Tarski axiomatic method.

Do you mean that every formalized axiom system uses arithmetical
notions such as "finite string of symbols."  This is why that formal
axioms cannot be the real basis of our knowledge of math, but it has
no more bearing on categorical axioms than any others.

Or do you think that pre-formal notions of "set" or "collection" are
all based on iterated membership and Zermelo's form of the axiom of
extensionality, so that CCAF is less basic than ZFC?  That is a common
belief among logicians who have not read Zermelo's critique of Cantor
(where Zermelo points out that Cantor did not hold these beliefs) and
who know a great deal more of ZFC than of other mathematics.

In fact, long before mathematicians could analyze the continuum into a
discrete set of points plus a topology, they were well aware of
collections like the collection of rigid motions of the plane -- and
that "collection" is a category.  It is not just a ZFC set of motions
but comes with composition of motions and with an object that the
motions act on.

> Elements of a new properly categorical
> method of theory-building are present in the "basic theory" (BC) that follows
> ETC. (I mean, in particular, the "redefinition" of functor in BC as 2-->A, etc.
> The standard definition of functor given earlier in ETC never reappears in BC.)

The "standard" definition of functor appears as the definition of a
small category in the category of sets.

> However in CCAF these new features are not yet developed into an autonomous
> axiomatic method - or into a new way of formalisation of pre-formal concepts,
> if you like.

Well, yes, they are developed into one.  That was Bill's achievement
with CCAF.

best, Colin


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

Re: categorical foundations

[Andre.Rodin]

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

I agree with you about generalities concerning pre-formal and formal
concepts. A reason why I say CCAF is not a satisfactory categorical foundation
is different. ETC is the formal basis of CCAF and ETC relies on a pre-formal
notion of set or collection just like ZF or any other axiomatic theory built
with Hilbert-Tarski axiomatic method. Elements of a new properly categorical
method of theory-building are present in the "basic theory" (BC) that follows
ETC. (I mean, in particular, the "redefinition" of functor in BC as 2-->A, etc.
The standard definition of functor given earlier in ETC never reappears in BC.)
However in CCAF these new features are not yet developed into an autonomous
axiomatic method - or into a new way of formalisation of pre-formal concepts,
if you like. In my understanding, such a method should meake part of
categorical foundations deserving the name.  CCAF remains in this sense
eclectic, it is a half-way to categorical foundations.

best,
andrei






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