MathOverflow is a question and answer site for professional mathematicians. Join them; it only takes a minute:

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

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?

share|cite|improve this question

closed as off-topic by François G. Dorais Aug 26 '13 at 4:27

  • This question does not appear to be about research level mathematics within the scope defined in the help center.
If this question can be reworded to fit the rules in the help center, please edit the question.

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? – François G. Dorais Aug 26 '13 at 2:47
Crossposted from Please post answers there. – François G. Dorais Aug 26 '13 at 4:27
John Baez has written a bit about this work here: – Evan Jenkins Aug 26 '13 at 4:40
The types in the internal logic of a Bohr topos ( 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 – Urs Schreiber Aug 26 '13 at 7:08