3
$\begingroup$

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?

$\endgroup$
4
  • 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$ Commented Aug 26, 2013 at 2:47
  • 1
    $\begingroup$ Crossposted from physics.se. Please post answers there. $\endgroup$ Commented Aug 26, 2013 at 4:27
  • $\begingroup$ John Baez has written a bit about this work here: math.ucr.edu/home/baez/week257.html $\endgroup$ Commented Aug 26, 2013 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$ Commented Aug 26, 2013 at 7:08

0