[FOM] When is it appropriate to treat isomorphism as identity?

[Andrej Bauer]

On Wed, May 20, 2009 at 8:55 PM, Monroe Eskew <meskew at math.uci.edu> wrote:
> The fact that a physicist uses a result without
> understanding the mathematical theory behind it, does not impugn the
> mathematical theory.  By your reasoning, the physicists may as well go
> along with memorizing formulas and ignoring proofs.

You misunderstand my implication. I would say it is presumptuous of
mathematicians to claim that physicists "use results without
understand the mathematical theory behind it". Physics has always been
a great source of new mathematics, and good physicsts have often had
important mathematical ideas. So I would put it the other way:
physicists have a definite mathematical intuition about infinitesimals
that is worth exploring. A mathematician who is telling them that
dx/dy is just a shorthand for something else, that in reality The
Right Way is the epsilon-delta way, is performing a methodological
error, and is missing an opportunity to discover new math. The fact
that even after 150 years of epsilon-delta domination the physicists
still use dx and dy should be a sign to the mathematicians that there
just might be a mathematical idea there.

Hendrik says physics students thought dx and dy was black magic. So
did I when I first saw them. But it does not have to be that way. The
infinitesimals can be directly axiomatized so that they make sense.
Many distinctions (such as continuous vs. uniformly continuous) never
show up (but others do). I am not saying epsilon-delta analysis is
useless. I am just saying that physicists have a (mathematical) point.

> Lastly, why would you want to expand your ontology unnecessarily with
> infinitesimals?  It seems very un-constructive.

Speaking as a physicist my answer would be: because I work with
infinitesimals every day.

I can ask a similar question about classical analysis: why would I
want to expand my ontology with silly functions, such as a function
which is continuous precisely at all irrational points? As a
physicist, what use do I have for such things? I'd rather have my
infinitesimals, thank you very much.

> If one keeps in mind that existence does not imply computability, one
> avoids such errors.

And one lives in constant doubt about which of the things that "exist"
actually can be computed. If I mostly care about computation, then I
might be happier with a notion of "exists" that coincides with "can be
computed".

> Of course the natural question for the
> constructivist is, "Why care about things we can't compute?"  Again
> with the example of approximation, one may have a classical result
> that X is approximated increasingly well by a countable recursive
> sequence Y_i.  It may not be (easily) computable exactly how far down
> in the sequence we have to go do achieve a desired degree of accuracy.
>  However, we may let a computer iterate the approximation process for
> however long we want.  We may not know how long it will take, but the
> abstract classical theory tells us that the process will eventually
> come to an accurate enough approximation.  This might be usefully
> applied.

You are talking about Markov principle in a roundabout way. In my
experience this principle, which incorporates a little bit of
classical logic into constructive logic, is immensely useful in
computation. So I'd say it makes sense to assume it (and I don't care
if that's not "constructively pure").

> I was merely pointing out that the dominance of classical mathematics
> in math departments has hardly hindered research in the theory of
> computation.

We're lucky if that's the case.

With kind regards,

Andrej