On Eq, was Re: [Haskell-cafe] When to use fancy types [Re: NumberTheory library]

karczma at info.unicaen.fr karczma at info.unicaen.fr
Sat May 14 19:58:21 EDT 2005

Jacques Carette answer to Lennart Augustsson's comment of: 

>>> Such people have the nasty habit of also thinking that ALL
>>> functions are continuous!  You might think they were constructivists 
>>> or something.

>> Why would a constructivist think that all functions are continuous?

> That would be a theorem of construtive mathematics!  All *constructible* 
> functions are continuous.  See
> http://plato.stanford.edu/entries/mathematics-constructive/

J. referenced this in his answer to my own doubts, where I confessed that
I knew physicists who sympathise with constructivists, yet they 'somehow'
accept that quantum scattering amplitudes must have branch cuts...
According to Jacques this cannot hold, since a True Constructivist rejects
the equality of reals. 


Well, I read once in Drexler Mathematical Forum (was it Barr?) that Bishop
himself didn't consider the claim that all functions are continuous as
theorem. This is not provable.
A kind of auto-trap? I am lost.
In Recursive Constructive Math there is a theorem of Kreisel-Lacombe-
Shoenfield-Tsejtin that total function within separable metric spaces are
continuous, but the assumptions are quite strong... 

All this is very far from my everyday soup, and I respect True
Mathematicians who split the hair infinitely very much (and also
constructivists and intuitionists who refuse this splitting as a
non-constructive, infinite process...) 

But, since the notion of function and of reals differs somehow from the
classical counterparts, as far as a poor physicist speaks about entities
which belong to the REAL WORLD, the problem remains, since even Master Yoda
doesn't know which should be the structure of math relevant to the reality.
I mean the 'true' math. And of course, with True meaning of the word 'true',
provided we know what does it mean the word 'meaning'. 

Thank you truly. 

Jerzy K.
(Kafka created at least two heroes named K., in The Trial, and in
The Castle. I feel like both of them together...) 

More information about the Haskell-Cafe mailing list