Distribution:

Followup-To:

Organization:

Keywords:

Graham Matthews said:

Quote:

>The problem is that all the examples you cite are really very simple

>in some sense. I don't mean to belittle the software you cite. I am sure

>all the things you cite are excellent and complicated pieces of software,

>but they are all examples where you do not have to model complicated

>relations between mathematical objects.

One problem is that mathematicans generally use the Axiom of Choice,

which is non-constructive. Given a relation on a set the Axiom

of Choice says that there is a function which "agrees" with it.

But, unless the set be finite, there's no way that a relation

(represented say as a boolean function) can be used to define

a function from the first argument of the relation to the second.

Such problems of non-computability of mathematical operations

occur everywhere. For example, an accurate representation of the

reals can be sought by representing a real as a function from

an arbitrary-precision representation of the reals to an

arbritrary precision representation of the rationals. But,

with this representation, equality of reals becomes undecidable,

and thus so do basic questions of cartesian geometry, such

as whether a point is on a line.

Robin.