* Re: Re: categorical foundations
@ 2009-11-16 14:54 Colin McLarty
2009-11-17 1:39 ` Charles Wells
2009-11-18 12:56 ` Andre.Rodin
0 siblings, 2 replies; 8+ messages in thread
From: Colin McLarty @ 2009-11-16 14:54 UTC (permalink / raw)
To: categories
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/ ]
^ permalink raw reply [flat|nested] 8+ messages in thread
* Re: categorical foundations
2009-11-16 14:54 Re: categorical foundations Colin McLarty
@ 2009-11-17 1:39 ` Charles Wells
2009-11-18 12:56 ` Andre.Rodin
1 sibling, 0 replies; 8+ messages in thread
From: Charles Wells @ 2009-11-17 1:39 UTC (permalink / raw)
To: Colin McLarty, catbb
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/ ]
^ permalink raw reply [flat|nested] 8+ messages in thread
* Re: categorical foundations
2009-11-16 14:54 Re: categorical foundations Colin McLarty
2009-11-17 1:39 ` Charles Wells
@ 2009-11-18 12:56 ` Andre.Rodin
1 sibling, 0 replies; 8+ messages in thread
From: Andre.Rodin @ 2009-11-18 12:56 UTC (permalink / raw)
To: Colin McLarty, categories
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/ ]
^ permalink raw reply [flat|nested] 8+ messages in thread
* Re: pragmatic foundation
@ 2009-11-11 16:38 Colin McLarty
2009-11-12 15:59 ` topos and magic Colin McLarty
` (2 more replies)
0 siblings, 3 replies; 8+ messages in thread
From: Colin McLarty @ 2009-11-11 16:38 UTC (permalink / raw)
To: categories
2009/11/6 Andre Joyal <joyal.andre@uqam.ca>:
writes
> I invite everyone to read the interesting interview of Yuri Manin
> published in the November issue of the Notices of the AMS:
Manin is always entertaining but not very careful about what he says.
André says:
> The foundational framework of Bourbaki is very much in the tradition
> of Zermelo-Fraenkel, Godel-Bernays and Russell.
> I am aware that Bourbaki was more interested in the development of
> mathematics than in its foundation.
I agree. Naturally Bourbaki was in a better situation to make up a
system that would work, since they had the others behind them. And
still their system did not work in fact.
Russell was more concerned with philosophic issues of logic, but his
touchstone for logic was that it should work! (He was very clear
about this by 1919, in his Principles Of Mathematical Philosophy.) He
knew a lot less than Zermelo about what would work for two reasons:
Russell got into it much earlier, and Russell studied math as a
philosopher at Cambridge while Zermelo studied it as a mathematician
with Hilbert in Göttingen and in debates with Poincaré.
All these people sought a foundation that would make sense in itself
and would work. Naturally they had different emphases, partly shaped
by the different resources they could draw on. Russell, Zermelo, and
Gödel all read each other (recalling that Russell was 59 years old,
and two decades past his work on logic, when Gödel published the
incompleteness theorem, and everyone took years absorbing it).
> In the interview, Manin also said that:
>
>>And so I don’t foresee anything extraordinary
>>in the next twenty years.
Of course we do not expect to *foresee* extraordinary things.
>> Probably, a rebuilding of what I call the “pragmatic
>> foundations of mathematics” will continue.
That is a pretty safe bet.
>>By this I mean simply a
>>codification of efficient new intuitive tools, such
>>as Feynman path integrals, higher categories, the
>>“brave new algebra” of homotopy theorists, as
>>well as emerging new value systems and accepted
>>forms of presenting results that exist in the minds
>>and research papers of working mathematicians
>>here and now, at each particular time.
Yes, there will be progress on all of these things.
I myself am also confident that people will calm down and notice that
axiomatic categorical foundations such as ETCS and CCAF work perfectly
well, in formal terms, and relate much more directly to practice than
any earlier foundations. One hundred and fifty years of explicitly
foundational thought has made this progress possible. By now, that
can hardly qualify as "extraordinary"!
best, Colin
[For admin and other information see: http://www.mta.ca/~cat-dist/ ]
^ permalink raw reply [flat|nested] 8+ messages in thread
* Re: topos and magic
2009-11-11 16:38 pragmatic foundation Colin McLarty
@ 2009-11-12 15:59 ` Colin McLarty
2009-11-13 0:42 ` categorical foundations Andre.Rodin
2009-11-13 1:29 ` Colin McLarty
2009-11-13 13:24 ` Colin McLarty
2 siblings, 1 reply; 8+ messages in thread
From: Colin McLarty @ 2009-11-12 15:59 UTC (permalink / raw)
To: categories, Joyal, André
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/ ]
^ permalink raw reply [flat|nested] 8+ messages in thread
* Re: categorical foundations
2009-11-12 15:59 ` topos and magic Colin McLarty
@ 2009-11-13 0:42 ` Andre.Rodin
0 siblings, 0 replies; 8+ messages in thread
From: Andre.Rodin @ 2009-11-13 0:42 UTC (permalink / raw)
To: Colin McLarty, categories
>
> 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/ ]
^ permalink raw reply [flat|nested] 8+ messages in thread
* Re: categorical foundations
2009-11-11 16:38 pragmatic foundation Colin McLarty
2009-11-12 15:59 ` topos and magic Colin McLarty
@ 2009-11-13 1:29 ` Colin McLarty
2009-11-13 9:24 ` Andre.Rodin
2009-11-13 13:24 ` Colin McLarty
2 siblings, 1 reply; 8+ messages in thread
From: Colin McLarty @ 2009-11-13 1:29 UTC (permalink / raw)
To: categories
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/ ]
^ permalink raw reply [flat|nested] 8+ messages in thread
* Re: categorical foundations
2009-11-11 16:38 pragmatic foundation Colin McLarty
2009-11-12 15:59 ` topos and magic Colin McLarty
2009-11-13 1:29 ` Colin McLarty
@ 2009-11-13 13:24 ` Colin McLarty
2009-11-15 19:02 ` Andre.Rodin
2 siblings, 1 reply; 8+ messages in thread
From: Colin McLarty @ 2009-11-13 13:24 UTC (permalink / raw)
To: categories
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/ ]
^ permalink raw reply [flat|nested] 8+ messages in thread
* Re: categorical foundations
2009-11-13 13:24 ` Colin McLarty
@ 2009-11-15 19:02 ` Andre.Rodin
0 siblings, 0 replies; 8+ messages in thread
From: Andre.Rodin @ 2009-11-15 19:02 UTC (permalink / raw)
To: Colin McLarty, categories
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. Im 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 Euclids) 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 Bills 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 doesnt 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 Bills 1966s 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,
doesnt work in the given form independently. Im not quite prepared to defend
any general notion of formal basis - I didnt mean to introduce such a general
notion and didnt 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/ ]
^ permalink raw reply [flat|nested] 8+ messages in thread
end of thread, other threads:[~2009-11-18 12:56 UTC | newest]
Thread overview: 8+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2009-11-16 14:54 Re: categorical foundations Colin McLarty
2009-11-17 1:39 ` Charles Wells
2009-11-18 12:56 ` Andre.Rodin
-- strict thread matches above, loose matches on Subject: below --
2009-11-11 16:38 pragmatic foundation Colin McLarty
2009-11-12 15:59 ` topos and magic Colin McLarty
2009-11-13 0:42 ` categorical foundations Andre.Rodin
2009-11-13 1:29 ` Colin McLarty
2009-11-13 9:24 ` Andre.Rodin
2009-11-13 13:24 ` Colin McLarty
2009-11-15 19:02 ` Andre.Rodin
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).