[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.



More information about the FOM mailing list