axiom-developer
[Top][All Lists]

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

 From: Bill Page Subject: Re: [Axiom-developer] Axiom, FriCAS, forks and teeth Date: Wed, 11 Jul 2007 17:20:52 -0400

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

```

reply via email to