Re: [Axiom-developer] The Axiom Library and Category Theory

[C Y]

--- Bill Page <address@hidden> wrote:

> The point of category theory as a foundation for mathematics
> is that a lot of mathematics can and should be done long before
> it becomes necessary to define what is meant by "set".

I have seen a few comments to the fact that it should be possible, in
theory, to describe virtually all of mathematics within the framework
of category theory.  If this is true, to me that makes it not only the
obvious foundational choice for The Axiom Library but the essential
one.

> > In fact, I would love to see a system that allows different
> > views. As mathematics can be based on set theory or category
> > theory. 
> 
> Maybe it is just where I live but I think most mathematicians
> since about 1975 or so have agreed that one should not try to
> base mathematics on set theory.

I would be curious as to whether it is possible, even in theory, to
make a CAS that allows multiple foundational design principles.  I
would think it is essential to choose a framework and build within it -
I doubt the mathematics would be "portable" between different
frameworks.  Does anyone know if this "portability" between
foundational concepts is actually possible?  My assumption that it
isn't is one of the major reasons I would like to see a proper Category
Theory at the foundations of Axiom's algebra.

> > > That would not make me nearly as happy as category theory.
> > > :-(
> > 
> > OK, you are responsible to start a library that builds on 
> > category theory.
> 
> Well I have been thinking about and writing about on this email
> list for a few years now... I would very much like to "get my
> head above water" long enough to concentrate on issues like
> these. Unfortunately we are still trying to decide things like
> what source code management system we should be using... :-(

I agree.  In my opinion when we get to the stage of making the Algebra
files truely literate, we will find that the optimal time to re-set the
foundations it builds on.  At that time, I think we should provide
"proper" category theory foundations and build on them, even if it
means re-tuning some of our terminology.  Mathematicians are the target
users for Axiom, and making their "native" vocabulary and Axiom's
terminology the same seem to me to have obvious benefits.  I know that
would be a large amount of work but any proper literate treatment of
Axiom's foundations will involve a similar amount of work - whatever
foundations we build on, we must document all the code and the ideas
behind it.  When we do it, let's do it once and in such a fashion that
(as far as is possible) we won't need to do it ever again.

Unfortunately, before we can get to this (very interesting) stage we
MUST have a firm, well defined, well documented foundation - especially
in terms of Aldor/SPAD programming.  :-(

Cheers,
Cy


       
____________________________________________________________________________________Ready
 for the edge of your seat? 
Check out tonight's top picks on Yahoo! TV. 
http://tv.yahoo.com/