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?

  • 1
    $\begingroup$ It's unclear what you are asking. Are you asking for the internal logic of a specific topos? A family of topoi? All topoi? Do you have one paper in mind or do you expect us to read them all? $\endgroup$ – François G. Dorais Aug 26 '13 at 2:47
  • $\begingroup$ Crossposted from physics.se. Please post answers there. $\endgroup$ – François G. Dorais Aug 26 '13 at 4:27
  • $\begingroup$ John Baez has written a bit about this work here: math.ucr.edu/home/baez/week257.html $\endgroup$ – Evan Jenkins Aug 26 '13 at 4:40
  • $\begingroup$ The types in the internal logic of a Bohr 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