Re: pragmatic foundation

Re: pragmatic foundation

[Colin McLarty]

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

Re: pragmatic foundation

[Vaughan Pratt]

Colin McLarty wrote:
> [responding to Manin thoughts] 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.

Thanks, Colin.  There I was nicely calmed down and then you got me all
worked up again.  :)

I prefer the Euclidean plane over sets as a suitable starting point for
understanding mathematics.  What advantage is there to making geometry
rest on set theory as opposed to vice versa?

What is wrong with starting from a geodesic space as a place where it is
always determined, given two points, what is the next one, subject to
some simple equational principles?  This is a common basis for the
second postulate of Book I of Euclid's *Elements*, Newton's first law
of motion, Einstein's theory of general relativity that a falling body
is merely following a geodesic in a space curved by a nearby mass, and
the notion of Hamiltonian flow of a vector field for an energy function
defined on the cotangent space of a manifold as an expression of the
principle of least action.

In this framework a *set* is simply a geodesic space where the next
point after x and y is x.  (So if I ask what is the next element in the
sequence 3,4,... the answer is 3, not 5.)

More on this at http://boole.stanford.edu/pub/consgeom.pdf .  A geodesic
space or geode, aka kei, is related to a quandle (see
http://en.wikipedia.org/wiki/Quandle ), the difference being that for
abelian groups, quandles are merely sets whereas flat geodes (those
satisfying Euclid's 5th postulate) form a symmetric monoidal closed
category fully and reflectively extending Set (properly of course).
Moreover its subdirect irreducibles are those of Ab except for those of
even order as per the last slide.  Quandles are for knot theory, not
geometry.

The difference between sets and geodesic spaces in foundations is like
the difference between scales and Fur Elise for piano students.  Both
are good ways to get started but the second is more interesting.
(Apologies again to Eduardo for my impenetrable writing, in this case I
can only counsel patience since these ideas seem to come with a certain
viscosity that inhibits any royal road of the kind Eduardo would like.)

Best,
Vaughan


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

topos and magic

[Andre Joyal]

Dear Colin,

I thank you for your interesting comments and observations.
I just realised that ETCS means <Elementary Theory of the Category of Sets> 
and that CCAF means <Category Theory as a Foundation>.

I am convinced that categorical logic, which was wholly invented by Lawvere, 
is the most important developpement of logic during the second half of the 20th century. 
I find the notion of elementary topos absolutly extraordinary, almost magical.
Like every important mathematical discovery, it stands out as a colorful gem on a bed of grey stones.
A classical example of gem is the field of complex numbers. 
The numbers were introduced by Cardan as a trick for computing the root of third degree equations 
in a case where his formula was not working.
The idea of inventing a square root of -1 to solve the problem was crazy but it worked.
The fact that the new system of numbers turns out to be algebraically closed
was proved by Lagrange and Gauss but it could not be foreseen by Cardan.
Equally unexpected is the role of complex numbers in quantum physics.
Similarly, 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.

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.

best, Andre

-------- Message d'origine--------
De: categories@mta.ca de la part de Colin McLarty
Date: mer. 11/11/2009 11:38
À: categories@mta.ca
Objet : categories: Re: pragmatic foundation
 
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/ ]

Re: topos and magic

[Vaughan Pratt]

Andre Joyal wrote:
> I find the notion of elementary topos absolutly extraordinary, almost magical.
> Like every important mathematical discovery, it stands out as a colorful gem on a bed of grey stones.
> A classical example of gem is the field of complex numbers.

Historically these two gems emerged as entirely independent
developments.  However they are arguably facets of a single gem, the
abelian-topos categories Peter Freyd wrote about on this list in
November 1997, archived at
http://blog.gmane.org/gmane.science.mathematics.categories/day=19971031
or on Karel Stokkerman's topic-indexed archive at
http://www.mta.ca/~cat-dist/catlist/1999/atcat
and
http://www.mta.ca/~cat-dist/catlist/1999/prattsli

The complex numbers live within the ring M(2,R) of 2x2 real matrices as
a subring of M(2,R) that happens to form a field.  (The general linear
group GL(2,R) is a larger *skew* field in M(2,R), but is there a larger
*field* than the complex numbers therein?)  M(2,R) in turn forms a
one-object full subcategory of the abelian category Vct_R, with matrix
multiplication (hence complex number multiplication) realized as
composition.  So the complex numbers form a subcategory of an abelian
category.

As Peter's treatment makes clear, abelian categories are a quite minor
variant on toposes.  An abelian category (resp. topos) is an
abelian-topos category all of whose objects X are of type A (resp. T),
meaning that the first (resp. second) projection of Xx0, namely from Xx0
to X (resp. 0), is an iso.  This difference is expressed as a very
simple elementary (first-order) predicate whose intuitive meaning is
clear: simply multiply X by zero and see whether it remains X or
collapses to zero.

So within the relatively small universe of abelian-topos categories (by
comparison with *all* categories) we find lurking therein both the field
of complex numbers and the toposes (and hence in particular the
effective topos, yet another gem Andre mentioned).

Over on the Foundations of Mathematics mailing list, FOMers would
presumably connect complex numbers to set theory by observing that the
complex numbers form a set which lives within the universe of sets
axiomatized by the Zermelo-Fraenkel axioms.  To me the path from complex
numbers to toposes via matrices and abelian categories seems somehow
more intimate.  Simply calling the complex numbers a set seems dry as
dust (literally).

(Peter J., are abelian-topos categories in the Elephant?  They seem an
obvious candidate yet I couldn't find them in either the table of
contents or the index.)

Vaughan Pratt


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

Re: topos and magic

[Colin McLarty]

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

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

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]

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

infinity

[Andre Joyal]

Dear Colin,

The Templeton foundation

http://en.wikipedia.org/wiki/John_Templeton_Foundation

is presently supporting a 2 years research program in set theory called
THE INFINITY PROJECT at the CRM in Barcelona:

http://www.crm.cat/InfinityProject/

There seem to be an endless number of projects
with the same name:

http://www.infinity-project.org/

http://fusionanomaly.net/tip.html

We some luck, we may be able to convince the Templeton Foundation
to support a research project in higher category theory and 
homotopy theory:

http://ncatlab.org/nlab/show/infinity-category

http://ncatlab.org/nlab/show/A-infinity-algebra

http://ncatlab.org/nlab/show/E-infinity-ring

http://ncatlab.org/nlab/show/L-infinity-algebra

http://ncatlab.org/nlab/show/%28infinity%2C1%29-operad

On the serious side, I think that we should make an effort 
to find a better terminology in higher category theory. 
I confess that I do not particularly cherish the name "quasi-category", 
although I am responsible for introducing it.
It seems better than "weak Kan complex" because the theory of these objects 
behaves very much like category theory. 
The name "infinity-category" is no better than "quasi-category".

infinity=endless
 
Jacob Lurie has expressed the same concern in a private discussion with me.  

best,
Andre



-------- Message d'origine--------
De: categories@mta.ca de la part de Colin McLarty
Date: jeu. 12/11/2009 20:29
À: categories@mta.ca
Objet : categories: Re: categorical foundations
 
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

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

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: pragmatic foundation

[Eduardo J. Dubuc]

Colin McLarty wrote:
> 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.
>

Well, the fact that he is not very careful is precisely what makes his saying
meaningful, interesting, fresh and enjoyable. He does not place himself within
any philosophical or political frame. He feels free to say what it crosses his
mind just as it comes. beautiful !


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

Re: pragmatic foundation

[Zinovy Diskin]

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

Hm, Manin is never just entertaining: he wrote several papers
concerning physics, linguistics, psychology, and his  thinking is an
example of how a true mathematical mind works in complex areas like
the humanities, generates unexpected views, reveals deep connections
etc. If the results are readable and enjoyable, it just shows the
literary talent of the author... :)

I also wouldn't say that Manin is not very careful about what he says.
The parts of the interview about foundations and physics say,
basically, this. After Bourbaki, a correct mathematical text should
consist of two parts:
(a) definition of the structure  in question (structure in the sense
of Bourbaki),
(b) deductions about this structure in some logic (perhaps, non-classical).
Manin says that texts generated by physicists do have (b) but not (a).
These are deductions about something that has not been defined and
hence, for a mathematician, that does not exist at all  (the Eiffel
Tower is in the air). This situation is not unique, of course: Manin
mentions Cantor's set theory at the time of invention, and it was and
is so for engineering theories. Software engineering should be of
special interest for this list because modern software executes
deductions about categorical structures.

It is not in the interview explicitly, but the following model of a
mathematical text would be probably close in spirit to what Manin
says. Mathematical texts form a span:
PM <--- MM --->FM
with
PM -- the universe of "physical" mathematical texts (physics, computer
science, engineering etc),
MM -- the mathematician's universe of mathematical texts; they are
written in a special subset of the natural language (nowadays, in
accordance with Bourbaki or category theory),
FM -- the universe of formal (machine-readable) mathematical texts.

A physicist is interested in the left foot, a logicist  -- in the
right one, but mathematics is about the entire span (well, for a true
mathematician, P stands for Platonic rather than Physics). If you
want: the logicist view is more normative because it insists on the
right right leg, but Bourbaki concerned about the entire span and did
not want to fix neither right nor the left legs (unless P is for
Platonic). So, they proposed a reasonable structure for MM for which
the left and right sides of the whole could be added (if needed). It's
indeed more about practical foundations...

After all, Eduardo said it best:

> Well, the fact that he is not very careful is precisely what makes his
> saying
> meaningful, interesting, fresh and enjoyable. He does not place himself
> within
> any philosophical or political frame. He feels free to say what it crosses
> his
> mind just as it comes. beautiful !
>


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

Re: pragmatic foundation

[Vaughan Pratt]

Eduardo J. Dubuc wrote: [regarding Manin]
> He does not place himself
> within
> any philosophical or political frame. He feels free to say what it
> crosses his
> mind just as it comes. beautiful !

Right, but clearly we cannot extend the same freedom to the hoi polloi,
who cannot be trusted not to abuse it.

Vaughan Pratt


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

Re: pragmatic foundation

[Eduardo J. Dubuc]

Vaughan Pratt wrote:
>
> Eduardo J. Dubuc wrote: [regarding Manin]
>> He does not place himself
>> within
>> any philosophical or political frame. He feels free to say what it
>> crosses his
>> mind just as it comes. beautiful !
>
> Right, but clearly we cannot extend the same freedom to the hoi polloi,
> who cannot be trusted not to abuse it.
>
> Vaughan Pratt
>

of course, only a few can make of such freedom a meaningful discourse  e.d.


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

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