nLab quantum logic



Type theory

natural deduction metalanguage, practical foundations

  1. type formation rule
  2. term introduction rule
  3. term elimination rule
  4. computation rule

type theory (dependent, intensional, observational type theory, homotopy type theory)

syntax object language

computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory

logicset theory (internal logic of)category theorytype theory
predicatefamily of setsdisplay morphismdependent type
proofelementgeneralized elementterm/program
cut rulecomposition of classifying morphisms / pullback of display mapssubstitution
introduction rule for implicationcounit for hom-tensor adjunctionlambda
elimination rule for implicationunit for hom-tensor adjunctionapplication
cut elimination for implicationone of the zigzag identities for hom-tensor adjunctionbeta reduction
identity elimination for implicationthe other zigzag identity for hom-tensor adjunctioneta conversion
truesingletonterminal object/(-2)-truncated objecth-level 0-type/unit type
falseempty setinitial objectempty type
proposition, truth valuesubsingletonsubterminal object/(-1)-truncated objecth-proposition, mere proposition
logical conjunctioncartesian productproductproduct type
disjunctiondisjoint union (support of)coproduct ((-1)-truncation of)sum type (bracket type of)
implicationfunction set (into subsingleton)internal hom (into subterminal object)function type (into h-proposition)
negationfunction set into empty setinternal hom into initial objectfunction type into empty type
universal quantificationindexed cartesian product (of family of subsingletons)dependent product (of family of subterminal objects)dependent product type (of family of h-propositions)
existential quantificationindexed disjoint union (support of)dependent sum ((-1)-truncation of)dependent sum type (bracket type of)
logical equivalencebijection setobject of isomorphismsequivalence type
support setsupport object/(-1)-truncationpropositional truncation/bracket type
n-image of morphism into terminal object/n-truncationn-truncation modality
equalitydiagonal function/diagonal subset/diagonal relationpath space objectidentity type/path type
completely presented setsetdiscrete object/0-truncated objecth-level 2-type/set/h-set
setset with equivalence relationinternal 0-groupoidBishop set/setoid with its pseudo-equivalence relation an actual equivalence relation
equivalence class/quotient setquotientquotient type
inductioncolimitinductive type, W-type, M-type
higher inductionhigher colimithigher inductive type
-0-truncated higher colimitquotient inductive type
coinductionlimitcoinductive type
presettype without identity types
set of truth valuessubobject classifiertype of propositions
domain of discourseuniverseobject classifiertype universe
modalityclosure operator, (idempotent) monadmodal type theory, monad (in computer science)
linear logic(symmetric, closed) monoidal categorylinear type theory/quantum computation
proof netstring diagramquantum circuit
(absence of) contraction rule(absence of) diagonalno-cloning theorem
synthetic mathematicsdomain specific embedded programming language

homotopy levels


Quantum systems

quantum logic

quantum physics

quantum probability theoryobservables and states

quantum information

quantum computation

quantum algorithms:



Broadly speaking, quantum logic is meant to be a kind of formal logic that is to traditional formal logic as quantum mechanics is to classical mechanics: a formal framework which is supposed to be able to express the statements whose semantics is the totality of all what is verifiable by measurement in a quantum system (quantum measurement).

In its traditional and default meaning due to (Birkhoff-vonNeumann 1936) “quantum logic” refers specifically to the orthocomplemented lattice of closed linear subspaces of a Hilbert space of quantum states. Later it was proposed (Yetter 90, Pratt 92, Abramsky-Duncan 05, Girard 11) that a better way to think of the BvN quantum lattices is as the propositions in linear logic (Girard 87), the categorical logic of symmetric monoidal categories.

There is also the proposal (Heunen-Landsman-Spitters 07) that quantum logic should be understood as being the internal logic of Bohr toposes.

In quantum computing the quantum analog of classical logic gates are called quantum logic gates.

History and Critique

Typically in the literature the term “quantum logic” is taken to refer very specifically to the first proposal for such a formalization due to Birkhoff-von Neumann 1936. In this proposal, given a quantum mechanical system with a Hilbert space of states, the logical propositions about the system are taken to correspond to (the projections to) closed subspaces, with implication given by inclusion of such subspaces. Hence Birkhoff-von Neumann quantum logic is given by the lattice of closed linear subspaces of Hilbert spaces (regarded as a Hilbert lattice).

This formalization is often understood as being the default meaning of “quantum logic”. But the proposal has later been much criticised, for its lack of key properties that one would demand of any formal logic.

For instance in Abramsky 2009 it is called a “non-logic”:

The term quantum logic is usually understood in connection with the 1936 Birkhoff-von Neumann proposal to consider the (closed) linear subspaces of a Hilbert space ordered by inclusion as the formal expression of the logical distinction between quantum and classical physics. While in classical logic we have deduction, the linear subspaces of a Hilbert space form a non-distributive lattice and hence there is no obvious notion of implication or deduction. Quantum logic was therefore always seen as logically very weak, or even as a non-logic. In addition, it has never given a satisfactory account of compound systems and entanglement.

Here by “no deduction” is meant “no deduction theorem”.

And for example in (Heunen-Landsman-Spitters 07, p. 4) it says the following.

Attractive and revolutionary as this spatial quantum “logic” may appear it faces severe problems. The main logical drawbacks are:

  1. Due to its lack of distributivity, quantum ‘logic’ is difficult to interpret as a logical structure.

  2. In particular, despite various proposals no satisfactory implication operator has been found (so that there is no deductive system in quantum logic).

  3. Quantum ‘logic’ is a propositional language; no satisfactory generalization to predicate logic has been found.

Quantum logic is also problematic from a physical perspective. Since (by various theorems and wide agreement) quantum probabilities do not admit an ignorance interpretation, [0,1][0, 1]-valued truth values attributed to propositions by pure states via the Born rule cannot be regarded as sharp (i.e. {0, 1}-valued) truth values muddled by human ignorance. This implies that, if X=[aΔ]X = [a \in \Delta] represents a quantum-mechanical proposition, it is wrong to say that either xx or its negation holds, but we just do not know which of these alternatives applies. However, in quantum logic one has the law of the excluded middle in the form xx =1x \vee x^\perp = 1 for all xx. Thus the formalism of quantum logic does not match the probabilistic structure of quantum theory responsible for its empirical content.

But notice that one may argue that the first three points here are squarely resolved by thinking of BvN-quantum logic as embedded into linear logic, we come back to this in a moment. Concerning the last point one might argue that the propositions in BvN-quantum logic concern the quantum measurement-outcomes (only), for which, at least in some interpretations, it does make sense to speak of a definite result.

In Girard 2011, page xii it says:

Among the magisterial mistakes of logic, one will first mention quantum logic, whose ridiculousness can only be ascribed to a feeling of superiority of the language – and ideas, even bad, as soon as they take a written form – over the physical world. Quantum logic is indeed a sort of punishment inflicted on nature, guilty of not yielding to the prejudices of logicians… just like Xerxes had the Hellespont – which had destroyed a boat bridge – whipped.

For more and more objective criticism see Girard 2011, section 17.

Girard had introduced the class of formal logic systems called linear logic and it has been argued that linear logic and more generally linear type theory does faithfully capture the essence of quantum mechanics (Yetter 90. Pratt 92, Abramsky-Duncan 05, Duncan 06), see (Baez-Stay 09 for an introductory exposition). This is due to the fact that the categorical semantics of linear logic is in symmetric monoidal categories such as those used in the description of finite quantum mechanics in terms of dagger-compact categories. In particular the category of (finite dimensional) Hilbert spaces whose subobjects/propositions form the Birkhoff-von Neumann style quantum logic does interpret linear logic.

This is stated explicitly for instance in (Pratt 92, p.4):

These objections are overcome in the extension of quantum logic to linear logic as a dynamic quantum logic.

Notice that the subobjects in a category of (finite dimensional) Hilbert spaces, and hence the propositions in the categorical logic of Hilbert spaces, are the (closed) linear subspaces. Therefore Birkhoff-von Neumann quantum logic is indeed subsumed as a fragment of linear logic. This (obvious) fact was highlighted in Crown 1975 and then later with more of categorical logic in place and emphasizing dagger-structures in Heunen 2008, Harding 2008 Heunen-Jacobs 2009, Coecke-Heunen-Kissinger 2013. Also CCGP 09, section 9.3):

both orthologic (or weakenings thereof) and linear logic share the failure of lattice distributivity. In particular, the fragment of linear logic that includes just negation and the additive connectives is nothing but a version of the paraconsistent quantum logic PQL.

That seems to make much of the above-listed criticism appear in a different light. For instance there is also a natural notion of dependent linear type theory and that does yield a well-behaved kind of predicate logic with quantifiers for linear logic.


Birkhoff-von Neumann quantum logic

Birkhoff & von Neumann 1936 is based on the setting the Hilbert lattice (of closed suspaces of a Hilbert space) to represent the set of propositions of quantum system.

conjunction is given by intersection of two linear subspaces

disjunction however is given by forming the linear space of two linear subspaces. Hence quantum states in the conjunction ABA \vee B may be linear combinations of states in AA and BB. This is an incarnation of superposition principle of quantum mechanics.

as a result, the BvN disjunction does not distribute over conjunction, and hence the BvN lattice is not a distributive lattice.

negation is given by forming orthogonal complement

Hilbert lattice

Logic of Quantales

On top of the above lattice of linear subspaces, take into account that it carries naturally a tensor product. That makes it a quantale.

Linear logic

More generally, if we do not just consider the monoidal poset (quantale) but more generally symmetric monoidal categories then this is linear logic, linear type theory


quantum computing.


The linearity of the logic, hence the absence of a diagonal in its categorical semantics, corresponds to the no-cloning theorem of quantum physics

Bohr toposes

See at Bohr topos for more.


General introductions and surveys:

A bibliography of hundreds of works up to 1992 is

  • Mladen Pavičić, Bibliography on quantum logics and related structures, pdf.

The original article on quantum logic:

Further discussion:

  • A. Gleason, Measures on the closed subspaces of a Hilbert space, Journal of Mathematics and Mechanics 6: 885-893 (1957)

  • Samuel S. Holland Jr., Orthomodularity in infinite dimensions; a theorem of M. Solèr, Bull. Amer. Math. Soc. (N.S.) 32 (1995) 205-234, arXiv:math.RA/9504224

Discussion of categorical logic in symmetric monoidal categories and hence of linear logic as quantum logic is in

  • G.D. Crown, On some orthomodular posets of vector bundles. Journ. of Natural Sci. and Math., 15(1-2):11–25, 1975.

(Girard 87 introduces linear logic nad suggests a possible relation to quantum physics, but remains undecided on thatM on p. 7 it says: “One of the wild hopes that this suggests is the possibility of a direct connection with quantum mechanics… but let’s not dream too much!”)

  • David Yetter, Quantales and (noncommutative) linear logic, Journal of Symbolic Logic 55 (1990), 41-64.

(Yetter 90) observes the the relation of linear logic to quantales, which have otherwise been proposed as providing a quantum logic.)

  • Vaughan Pratt, Linear logic for generalized quantum mechanics, in Proc. of Workshop on Physics and Computation (PhysComp’92) (pdf, web)

(Pratt 92 is maybe the first to really say that linear logic is a good kind of quantum logic.

(This highlights more linear type theory and its use in quantum theory.)

That therefore in particular categories of cobordisms (the domains of functorial quantum field theory) interpret quantum logic qua linear logic has been highlighted in

  • Sergey Slavnov, From proof-nets to bordisms: the geometric meaning of multiplicative connectives, Mathematical Structures in Computer Science / Volume 15 / Issue 06 / December 2005, pp 1151 - 1178

  • John Baez, Mike Stay, Physics, topology, logic and computation: a rosetta stone, (arxiv/0903.0340); in “New Structures for Physics”, ed. Bob Coecke, Lecture Notes in Physics 813, Springer, Berlin, 2011, pp. 95-174 (doi:10.1007/978-3-642-12821-9)

Discussion of Fock space-type free quantum field theory in linear logic is in

  • Marcelo Fiore, Differential Structure in Models of Multiplicative Biadditive Intuitionistic Linear Logic (web)

The proposal that the internal logic of Bohr toposes is a good notion of quantum logic is made in

See also

  • Yuri Manin, A course in mathematical logic, Springer

  • Д.И. Блохинцев, Принципиальные вопросы квантовой механики, 1966, 162 с.

  • A. Sudbery, Quantum mechanics and the particles of nature, An outline for mathematicians, Camb. Univ. Press 1986

  • Stanford Encyclopedia of Philosophy, qm: von Neumann vs. Dirac,

Last revised on October 25, 2022 at 12:09:32. See the history of this page for a list of all contributions to it.