Re: [Axiom-developer] Axiom, FriCAS, forks and teeth

[Bill Page]

On 7/11/07, C Y wrote:
> > But the goals of Principia Mathematica
> > (a universal treatment of mathematics) has been shown by
> > mathematicians themselves (e.g. Geodel's theorem) not to be
> > attainable even in principle.
>
> OK.  So then, how DO we work with mathematics? (I don't expect an
> answer - but it's still a reasonable question, unless one wants to
> throw up one's hands.  A universal treatment (whatever that means)
> might not be possible, but what is the best solution (or solutions)
> that ARE possible?)

Perhaps the answer lies in category theory as a foundation for
mathematics and as a model for appropriate formalisms in computer
science.

> ...
>  But can any of those systems take an
> answer and use their internal routines to guide the creation of an
> axiomatic proof of a answer?  Something that could be verified by ANY
> mechanical proof checker that understand the chosen language, or even a
> sufficiently patient human?  Without that, how can we trust the results
> of any system?  Why should scientists depend on a tool they can't know
> is without error and have no hope of verifying?

Well, they do tend to depend on each other, right? ;-)

Seriously, I do not think we are at the stage where we can trust the
output of any system -- certainly not one that is complicated enough
to include arithmetic (ref: Geodel's theorem). I agree that the
marriage of computer algebra and computer aided proof systems is an
interesting concept but it is still at the very early research stage.

> ...
> I would be curious what branch(es) of mathematics you think Axiom will
> be incapable of dealing with, via one form or another of extension?  Is
> there any possible system you feel would be MORE useful?

Category theory, category theory. Any computer algebra system that
makes at least a half way attempt to structure things according to
category theory.

> ...
> Am I nuts?  Probably ;-).  I don't know if even Tim shares my views in
> this respect.  I know I'm not a good fit for FriCAS, perhaps I am not a
> good fit for Axiom.  But what else can we do in a volunteer project but
> pursue our interests?  If those are not compatible with the project, I
> can work on my own - I have no wish to disrupt anything any further
> than it has already been disrupted.

Gee, there must be something (bad vibes?) in the air recently ... ;-)

Certainly you have as much right to be here (or there) as anyone else.
I do not find any of the work you do or your comments at all
disruptive.

Regards,
Bill Page.