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

[Andre.Rodin]

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


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




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

Re: pragmatic foundation

[Vaughan Pratt]

Eduardo J. Dubuc wrote:
> I wish you (V.P.) were more clear. I can not see what is your point.
> Witty msages for the Illuminati don't serve any pourpose, except
> amusement to some.

Yes, sorry about that.  A couple of others wrote privately with the same
request.

I have no problem with the notion of mathematical truth per se, which I
imagine to be what all mathematicians seek, along with mathematical
tools and a consensus thereon by their colleagues.

What I had in mind by the "haunting" remark is that the implications of
Goedel's incompleteness results don't immediately leap out at one, and
there is a certain optimistic tendency to minimize those implications
and continue to argue the issues as though Goedel's theorems weren't
relevant.

We can't *define* mathematical truth (Tarski may have been the first to
enunciate that implication most clearly), yet we can often recognize it
when we see it.  Learning to do mathematics amounts to learning how to
find and communicate those mathematical truths that are easily
recognized as such by other mathematicians according to community standards.

We imagine that mathematics on Arcturus must be like ours, but
mathematics is an intrinsically cultural subject and I don't see why
Arcturan mathematics should be like ours.  Do Arcturans have logic?  Do
they have algebra?  Do they draw a distinction between the two?  Do they
believe in either?  Add category theory as a third framework and ask the
same questions of it.  Do they know about initial algebras and final
coalgebras, and if so which came first for them?  Do they know about
monads and adjunctions, and if so which came first?

That's surely too brief to be clear.  I'd be happy to engage further in
this sort of speculation on the practice of mathematics as a cultural
issue.  I have less to contribute on the intrinsic nature of mathematics
itself for lack of insight into its scope.

Vaughan Pratt


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

Re: pragmatic foundation

[Eduardo J. Dubuc]

Andre touches an interesting problem.

I wish you (V.P.) were more clear. I can not see what is your point. Witty
messages for the Illuminati don't serve any purpose, except amusement to
some.

I would like Bill (Lawvere) send us his opinion about Maning's views.

e.d.

Vaughan Pratt wrote:
>> Any comments?
>> AJ
>
> Hi Andre.  I read the Manin interview in the AMS Notices with much
> interest myself last week.
>
> With regard to your request for comments, I can only repeat von
> Neumann's remark after Goedel's lecture as cited recently in Logicomix:
> "It's all over."  I couldn't agree more.  Like a rat trap slamming shut
> on a rat that we no longer need fret about.
>
> That the rat's ghost continues to haunt so many is an interesting
> commentary on human nature.
>
> Cheers,
> Vaughan
>
>


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

Re: pragmatic foundation

[Andre.Rodin]

I agree with WHAT Yuri Ivanovitch Manin says about foundations of mathematics
but DISagree when he calls these foundations "pragmatic". I might be mistaken
(in this case, I hope, Yuri Ivanovitch will correct me) but I don't think that
in the given context the word "pragmatic" is supposed to be understood with a
philosophical seriousness. In the given context "pragmatic" is rather
synonymous to "practical" as opposed to "theoretical" - and perhaps also to
"purely mathematical" as opposed to "philosophical". I fully share with Yuri
Ivanovitch his disappointment about what he calls the "normative foundations
that logicists or constructivists tried to impose". But I see a solution in a
new dialectical philosophy of foundations (tightly connected to mathematical
practice), NOT in developing foundations purely "pragmatically" without
theoretical and philosophical grounds. The history teaches us that
philosophical thinking is crucial for what Yuri Ivanovitch calls the
"rebuilding" of foundations, and I don't see any reason why this might cease to
be true today.
On the contrary, I think that the acceleration of mathematical progress
necessitates the acceleration of rebuilding of foundations - and this makes
philosophy more relevant to mathematical research than ever. "Logicists and
constructivists" don't have centuries to come to eternalise their findings by
establishing a new Scholastic tradition in philosophy - even if some of them
would wish it.

Andrei

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

Re: pragmatic foundation

[Vaughan Pratt]

> Any comments?
> AJ

Hi Andre.  I read the Manin interview in the AMS Notices with much
interest myself last week.

With regard to your request for comments, I can only repeat von
Neumann's remark after Goedel's lecture as cited recently in Logicomix:
"It's all over."  I couldn't agree more.  Like a rat trap slamming shut
on a rat that we no longer need fret about.

That the rat's ghost continues to haunt so many is an interesting
commentary on human nature.

Cheers,
Vaughan


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

pragmatic foundation

[Andre Joyal]

Dear category theorists,

I invite everyone to read the interesting interview of Yuri Manin 
published in the November issue of the Notices of the AMS:

http://www.ams.org/notices/200910

http://www.ams.org/notices/200910/rtx091001268p.pdf

One the ideas discussed by Manin is that of a "pragmatic foundation" of
mathematics as opposed to a "normative foundation" by logicists or constructivists. 
He attributes the former to Bourbaki.

I disagree.

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. 
My guess is that the foundation was too problematic to be given a proeminent place 
in the treaty, not for logical reasons but for conceptual reasons.
I claim that nobody truly understand set theory, even today!
The emperor has no clothes!
I mean that the hierarchy of infinite cardinals is so profoundly mysterious 
that it looks pathological.
What is the value of a theory if it leads to meaningless problems and structures? 
Having no good answer to offer, Bourbaki decided to diminish the importance of 
foundation rather than leaving it open. 
It may explain why category theory was not incorporated in the foundation later.

In the interview, Manin also said that:

>And so I don’t foresee anything extraordinary 
>in the next twenty years. Probably, a rebuilding of 
>what I call the “pragmatic foundations of math- 
>ematics” will continue. 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. 

Any comments?


AJ


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