I've asked this question on Physics.SE but was advised to ask it here.

Isham & Doering have written a series of papers exploring how to ground physics in topoi. Now the internal logic of topoi is higher order typed intuitionistic logic. In their theory what role is played by intuitionistic logic? What are the types in their theory?

Crossposted from physics.se. Please post answers there.$\endgroup$ – François G. Dorais♦ Aug 26 '13 at 4:27Bohr topos(ncatlab.org/nlab/show/Bohr%20topos) associated with a $C^\ast$-algebra are the "presheaves on classical contexts", hence all things that can be "probed" by commuting subalgebras of the given $C^\ast$-algebra of quantum operators. This is, so far, a proposal only for how to formulate phase spaces of quantum states in topos theory. For a synthetic formulation of quantum field theory comprehensively in higher toposes see ncatlab.org/schreiber/show/Synthetic+Quantum+Field+Theory $\endgroup$ – Urs Schreiber Aug 26 '13 at 7:08