nLab propositions as projections

Idea

In intuitionistic type theory the perspective of propositions as types identifies mere propositions with (speaking in categorical semantics) monomorphisms into the given context type. If one instead considers linear type theory then it makes sense to consider those propositions, in this sense, which come from monomorphisms that are split monomorphisms, hence those for which there is a projection from the context to the subobject that represents the proposition. For these one might speak of “propositions as projections”.

For instance in a category of Hilbert spaces, regarded as semantics for bare multiplicative linear type theory, then projections correspond to (closed) linear subspaces. These are just the propositions in the corresponding quantum logic. If we regard a proposition as its corresponding projection, then it is natural to consider it also as being the application of this projection, in that the truth of the proposition is thought of as the image of applying this projection. In terms of quantum physics this relation between propositions (about a quantum mechanical system) and the projection onto the corresponding subspace of the space of quantum states is what is referred to as the “collapse of the wave function”.

References

• Kurt Engesser, Dov Gabbay, Daniel Lehmann, A New Approach to Quantum Logic, vol. 8 of Studies in Logic, College Publications, London, UK, 2007. (pdf)