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

[Monroe Eskew]

Andrej,

Your responses seem to come from a pragmatist perspective.  So I have
a few questions.

1) Why bother with foundations?  You even dismiss such concerns as too
puritan in the discussion about approximation processes.  If your goal
is to just do whatever works "as a physicist," then it would seem
unnecessary to have some formal foundation for infinitesimal numbers,
or to reform the semantics of existential quantification.

2) Aren't the epsilon-delta notions of limits practical?  I know that
in experimental science, one wants to approximate and compute all the
time, and it is also of interest to do so within a margin of error.
This means a FINITE margin of error, since infinitesimal error is not
available in the real world.

Best,
Monroe


On Wed, May 20, 2009 at 2:33 PM, Andrej Bauer <andrej.bauer at andrej.com> wrote:
> Hendrik says physics students thought dx and dy was black magic. Sodid I when I first saw them. But it does not have to be that way. Theinfinitesimals can be directly axiomatized so that they make sense.Many distinctions (such as continuous vs. uniformly continuous) nevershow up (but others do). I am not saying epsilon-delta analysis isuseless. I am just saying that physicists have a (mathematical) point.
> Speaking as a physicist my answer would be: because I work withinfinitesimals every day.
> I can ask a similar question about classical analysis: why would Iwant to expand my ontology with silly functions, such as a functionwhich is continuous precisely at all irrational points? As aphysicist, what use do I have for such things? I'd rather have myinfinitesimals, thank you very much.
> And one lives in constant doubt about which of the things that "exist"actually can be computed. If I mostly care about computation, then Imight be happier with a notion of "exists" that coincides with "can becomputed".
> You are talking about Markov principle in a roundabout way. In myexperience this principle, which incorporates a little bit ofclassical logic into constructive logic, is immensely useful incomputation. So I'd say it makes sense to assume it (and I don't careif that's not "constructively pure").