[FOM] constructivism and physics
dvanhorn@cems.uvm.edu
dvanhorn at cems.uvm.edu
Sun Feb 12 07:44:37 EST 2006
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
More information about the FOM
mailing list