In the topos-theoretic interpretation of Physics by Isham & Doering what role does intuitionistic logic play? 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?
I've also asked this question on Math.Overflow
 A: Given a $C^\ast$-algebra $A$, its "Bohr topos" (see there for a survey) is the presheaf topos on its commutative subalgebras. The idea here is that if we think of $A$ as the algebra of quantum operators of a quantum mechanical system (for instance all the bounded operators on the Hilbert space of states of a system), then the commutative subalgebras correspond to classically simultaneous observables, and a presheaf on these is anything that can be "probed" by all such "classical contexts". Since Niels Bohr in his informal writings propagated the idea that whatever quantum mechanics is, it should be communicatable by classical observations, this has been argued to formalize Bohr's view on quantum physics. 
In any case the types in the internal logic of the Bohr topos, hence the objects of the Bohr topos, are all "observations testable on classical contexts".
The main result of this construction can be summarized as follows: a classical observable internal to the Bohr topos is equivalently a quantum observable on $A$, in the sense of QM formulated in terms of operator algebra. See at kinematics of a Bohr topos for details. This may feel like a satisfactory state of affairs. It is however as yet not quite clear what else this is going to lead to.
One should be careful with overstating what Bohr toposes achieve. Whether they serve as a "foundation of physics" would yet have to be shown. So far they serve to formalize only state spaces of quantum mechanical systems. Effectively they are a way to look at Hilbert spaces such that the notion of quantum observables fits more naturally with that of classical observables.
Already dynamics (e.g. Hamiltonians) is not captured by Bohr toposes as such. My student Joost Nuiten showed how one can formulate the local nets of observables of algebraic QFT in terms of sheaves of Bohr toposes on spacetime. See Nuiten's bachelor thesis. His main result is that the causal locality of quantum field theory is equivalent to a natural descent property of the collection of Bohr toposes assigned to each open subset of spacetime.
This does incorporate quantum field theoretical dynamics into the theory of Bohr toposes. But here, too, it is not quite clear currently what this is going to lead to. While I find this interesting, it is far from being a foundation for all of physics. It may be thought of as a topos-theoretic formulation of AQFT, though. Nice as it is, whether AQFT is even a foundation of all of Lorentzian quantum field theory is debatable.
If one really wants to see foundations of physics, one needs to dig a bit deeper, I would say. A fairly detailed proposal for how to go about this I have been describing at Synthetic Quantum Field Theory and in the articles linked to from there. 
Incidentally, Joost Nuiten is just today defending his master thesis on this more comprehensive topic. See at master thesis Nuiten his work "Cohomological quantization of local prequantum boundary field theory". I gave a talk about this two days ago at the "Geometry and Physics XI"-workshop in Pittsburgh, see Motivic quantization of local prequantum field theory.
This describes a story where one starts in infinity-topos theory and discovers in there all of local prequantum field theory and eventually its motivic quantization to local quantum field theory. The examples-section of Nuiten's thesis shows how ordinary quantum mechanics is reproduced this way, the quantization of Poisson manifolds, of Poisson-model topological strings, of type II strings and of heterotic strings, reproducing in partcicular the Witten genus partition function of the heterotic 2d sigma-model field theory. If nothing else, this shows at least that there is non-trivial genuine physics captured by this formalization.
A: Looking at the first paper in their series, A Topos Foundation for Physics: I. Formal Languages for Physics
Given a closed physical system, a theory for it is a higher-order typed intuitionistic logic $L$, which has  $\Sigma$, the state space type; and $R$, the quantity-value type; and the higher types are observables $A:\Sigma \rightarrow R$. Propositions about the system are subtypes of $\Sigma$ which will form a Heyting algebra, and which are assigned truth values via the Truth type $\Omega$, that is the sub-object identifier.
Then, a representation of $L$ in a topos $T$ is a concrete physical theory.
When the topos $T$ is $Set$, this reduces to the classical realist description, where they explain propositions about the system are handled by Boolean logic, rather than the intuitionistic logic of the topos.  
They justify the introduction of a quantity-type by critiquing the assumption that quantities should be real-valued. As for intuitionistic logic, they say
in a foot-note:

The main diﬀerence between theorems proved using Heyting logic and those using Boolean logic is that proofs by contradiction cannot be used in the former. In particular, this means that one cannot prove that something exists by arguing that the assumption that it does not leads to contradiction; instead it is necessary to provide a constructive proof of the existence of the entity concerned. Arguably, this does not place any major restriction on building theories of physics.

One could argue this is intuitionistic logic viewed from a physical point of view, in as much the same way physicists play fast & loose with calculus & limiting arguments.
