[FOM] constructivism and physics

[Bas Spitters]

On Thursday 09 February 2006 03:34, Neil Tennant wrote:
> The discussion on constructivism and physics appears to be based on the
> common assumption that the constructivist's task would be to serve up as
> (constructive) theorems all those theorems that physicists might have
> occasion to apply when making predictions about, and giving explanations
> of, empirical phenomena.
>
> There is a quite different view, however, that allows the constructivist
> to claim adequacy of constructive mathematics for all possible
> applications in scientific reasoning, and which even explains why it is
> that (in light of this) it is so useful to have classical theorems
> available "off the shelf" for applications in science.

I do not understand your paper entirely, please correct me if I am mistaken. 
Your argument for using classical theorems seems to be that one can translate 
such statements to a constructive statement. However, as far as I know it is 
not obvious that such a technique can by extended to include countable 
(dependent) choice, which of course is used freely in classical mathematics.
See for instance:
Ulrich Berger's nice paper:
http://www.cs.swan.ac.uk/~csulrich/publications.html#OpenInduction
and the references cited therein.
In short, all approaches seem to use some form of bar induction (or open 
induction), which is not accepted in Bishop-style mathematics.

Could you please give a precise example of a classical system and a 
constructive system that you have in mind? For instance, PA and HA would do, 
but that would hardly be a convincing argument for allowing classical 
theorems in mathematical physics, would it?

Am I mistaken?

Bas Spitters

-------------------------------------------------------
Research Group Foundations/ Institute for Computing and Information Sciences
Radboud University Nijmegen www.cs.ru.nl/~spitters/
P.O.box 9010, NL-6500 GL Nijmegen, The Netherlands.
spitters at cs.ru.nl Ph:+31-24-3652631 F:+31-24-3652525 Room: A5024