[FOM] constructivism and physics

[dvanhorn@cems.uvm.edu]

Quoting Bas Spitters <spitters at cs.ru.nl>:
> 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.

Jean-Louis Krivine has done this in the form of a machine for lambda terms
extended with a call/cc instruction (realizing Peirce's law) and an instruction
for the axiom of dependent choice.

See:
http://www.pps.jussieu.fr/~krivine/articles/Luminy04.pdf

David