# 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

-
The intersection of the set of physicists and the set of people who understand topos theory is small. I suspect you'll be much more likely to get a good response if you post this on mathoverflow.net. If you do, please link to it, because I'd like to follow it (to the extent that my expertise allows). –  Ben Crowell Aug 26 '13 at 1:40
@crowell: thanks for the tip. –  Mozibur Ullah Aug 26 '13 at 1:48
It's generally poor form to cross-post on two sites simultaneously. Your best bet is to try one site first, and if it doesn't work after a few days, try the other. –  tpg2114 Aug 26 '13 at 1:56
@tpg2114: sure, but as Crowell points out there are few people conversant in both physics and topoi, so in this case, I think its justified. –  Mozibur Ullah Aug 26 '13 at 2:05

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.

-
I wasn't sure from this what the connection is between Ishams & Doerings approach to Spitters Bohrification. But in the intro to Nuitens BA thesis, he writes: "A decade ago, it was suggested by Buttereld and Isham that topos theory could provide a better framework for formulating something like quantum logic. In particular, they noticed that while a quantum phase space does not exist as an ordinary topological space, it does exist as a topos with an internal `space', or locale. –  Mozibur Ullah Aug 26 '13 at 14:47
This perspective allowed them to give a geometric formulation of the Kochen-Specker theorem, which then precisely stated that this internal phase space had no global points. Inspired by this, Spitters et al. described a quantum phase space as a topos with an internal locale, using a procedure they called Bohrication". –  Mozibur Ullah Aug 26 '13 at 14:48
@Mozibur, the difference is that Isham-Doering look at contravariant functors on commutative subalgebras with inclusions between them, while Heunen-Landsman-Spitters look at covariant functors. The basic statements about observables work in both formulations. Sander Wolters has a a bit of discussion of the relation between the two in "A Comparison of Two Topos-Theoretic Approaches to Quantum Theory" arxiv.org/abs/1010.2031 . In the perspective of Heunen-Landsman-Spitters the Bohr toposes are naturally ringed toposes (ncatlab.org/nlab/show/ringed+topos) which makes them... –  Urs Schreiber Aug 26 '13 at 16:31
...which makes them fit nicely in the broader context of algebraic and higher/derived geometry, which is all about modelling spaces by ringed toposes (ncatlab.org/nlab/show/structured+(infinity,1)-topos). In Nuiten's discussion of quantum field theory by Bohr toposes it is crucial that the causal locality axiom is encoded as a descent condition of such ringed toposes. So for that application to QFT I tend to prefer them, but for basic statements one can just as well use the other model. –  Urs Schreiber Aug 26 '13 at 16:33

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.

-