Last month’s post was about probability theory. This month’s post will cover something completely different. Most people have heard about quantum mechanics and its implications for technology (in the form of quantum computing). What is less well known is the logical structure of the propositions that can be considered in quantum mechanics. ‘Quantum logic’, which is the type of logic that should come out of this consideration, has been studied since the days that quantum mechanics was formalized. However, pay attention to the word ‘should’ in the previous sentence. It turns out that the naive logic that one would extract is actually quite ill behaved.

Overview

$\newcommand{\dualampersand}{\,\style{display: inline-block; transform: rotate(180deg)}{\&}\,}$

This post is structured as follows:

  1. Primer on quantum information theory
  2. Birkhoff–Von Neumann logic a.k.a. quantum logic
  3. Primer on Gentzen’s sequent calculus
  4. Linear logic
  5. Interpretation in terms of resources
  6. Categorical semantics of (linear) logic

In the first section, a short introduction to quantum information theory is given: quantum states, entanglement and some remarkable theorems. Considering the natural structure of quantum mechanics quickly leads to a generalization of classical logic, which is the subject of the second section.

For the readers that are primarily interested in quantum mechanics, the first two sections are the most relevant. Section 3 and onwards are of a more mathematical flavour but introduce a different type of logic that can be obtained when incorporating the core results of quantum information theory.

Although the naive generalization of classical logic coming out of quantum mechanics might seem natural at first, it has some serious downsides and a different approach is followed in section 4, with the necessary mathematical background being introduced in Section 3. After the core ideas of linear logic have been introduced, Section 5 reformulates these concepts in terms of ‘resources’ and ‘processes’ as to shed a different, more practical light on the matter. To finish the main body of this post, Section 6 covers my personal favourite, the categorical semantics.

Primer on quantum information theory

In quantum mechanics, everything revolves around state vectors $\lvert\psi\rangle$ in Hilbert spaces $\mathcal{H}$ and the operators $\widehat{O}\in\mathrm{End}(\mathcal{H})$ that act on them. An important construction in quantum mechanics and quantum information theory is the tensor product, which assembles separate quantum systems into one composite system:

\[\mathcal{H}_1,\mathcal{H}_2,\cdots,\mathcal{H}_n\longrightarrow\mathcal{H}_1\otimes\mathcal{H}_2\otimes\cdots\otimes\mathcal{H}_n\,.\]

Associated to this construction and the unitarity of quantum mechanical evolution (the Schrödinger equation), there are two very important theorems: the no-cloning and no-deleting1 theorems.

Consider a Hilbert space $\mathcal{H}$. There exists no unitary operator $\widehat{U}\in\mathrm{Aut}(\mathcal{H}\otimes\mathcal{H})$ such that

\[\widehat{U}\bigl(\lvert\phi\rangle\lvert\psi\rangle\bigr) = e^{i\alpha(\phi,\psi)}\lvert\phi\rangle\lvert\phi\rangle\]

for any two (normalized) states $\lvert\phi\rangle,\lvert\psi\rangle\in\mathcal{H}$.2

Consider two Hilbert spaces $\mathcal{H},\mathcal{H}'$, where the latter can be interpreted as representing the 'machine'. If a unitary operator $\widehat{U}\in\mathrm{Aut}(\mathcal{H}\otimes\mathcal{H}\otimes\mathcal{H}')$ satisfies $$\widehat{U}\bigl(\lvert\psi\rangle\lvert\psi\rangle\lvert A\rvert\bigr) = \lvert\psi\rangle\lvert0\rangle\lvert A_\psi\rangle$$ for all initial states $\lvert\psi\rangle\in\mathcal{H}$ and initial ancilla states $\lvert A\rangle\in\mathcal{H}'$, then the operation $\lvert A\rangle\mapsto\lvert A_\psi\rangle$ on the ancilla space is an isometric embedding, i.e. the second physical state can only be deleted, if the information is stored in the ancilla state.

?? FINISH ??

Birkhoff–Von Neumann logic

In classical logic, the set of propositions forms a Boolean algebra. This means that one has a conjunction and disjunction (the logical ‘and’ $\land$ and ‘or’ $\lor$), a negation or complement ($\lnot$) and two constants ($\top$, $\bot$), representing truth and falsity. These constants and operations satisfy a number of conditions such as distributivity (or, in logic, de Morgan’s laws):

\[p\land (q\lor r) = (p\land q)\lor(p\land r) \qquad\qquad p\lor (q\land r) = (p\lor q)\land(p\lor r)\,.\]

All these propositions (and the associated Boolean structure) can be represented using sets, namely the set $S_p$ representing the proposition $p$ is given by all elements that satisfy $p$. In quantum mechanics, one does not simply work with sets, but with subspaces, since, by the projection axiom of quantum mechanics, performing a measurement projects the state vector onto the subspace associated to the obtained eigenvalue.

Now, following Birkhoff and Von Neumann, if one considers the $\{0,1\}$-valued measurements as propositions in quantum theory, one finds that propositions are represented by projection operators, i.e. $\Pi^2=\Pi$. It can be shown that the set of projection operators or, equivalently, closed subspaces of Hilbert spaces forms a generalization of a Boolean algebra: an orthomodular lattice. However, because these lattices are nondistributive, it is hard to introduce a notion of implication or deduction and, as such, this gives rise to a very ‘non-logic’ theory. Moreover, there is no clear way to pass from this propositional form to a predicative form. A third issue, related to the probabilistic predictions of quantum mechanics through the Born rule, is that although the crisp statements about the value of a measurement cannot be made, the orthomodular lattice of quantum propositions does satisfy the law of the excluded middle.

To circumvent these issues, one needs a different, more general, type of logic!

Primer on sequent calculus

Gentzen, building on the work of Heyting, realized a very interesting fact. Intuitionistic logic could be recovered as a fragment of classical logic by removing the weakening and contraction rules on the right-hand side of sequents, i.e. by only considering sequents of the form

\[\Gamma_1,\ldots,\Gamma_n\vdash\Theta\,.\]

For linear logic, which will be introduced in the next section, weakening and contraction are completely removed.

Will be completed!

Linear logic

Whereas, as noted in the previous section, the sequent $\Gamma_1,\ldots,\Gamma_m\vdash\Theta_1,\ldots,\Theta_n$ to $\Gamma_1\land\cdots\land\Gamma_m\vdash\Theta_1\lor\cdots\lor\Theta_n$ in classical logic, this will become

\begin{gather} \label{general_sequent} \Gamma_1,\ldots,\Gamma_m\vdash\Theta_1,\ldots,\Theta_n \iff \Gamma_1\otimes\cdots\otimes\Gamma_m\vdash\Theta_1\dualampersand\cdots\dualampersand\Theta_n \end{gather}

in linear logic (i.e. the multiplicative connectives govern the basic rules).

The basic constructs of linear logic are as follows:

  • Negation: If $P$ is a proposition, so is $P^\ast$.

    (Although $\lnot P$ is a more common notation in logic, the asterisk will be used in this post. Both to highlight the difference between classical and linear logic and because of the categorical semantics which will be discussed further below.)

  • Connectives: If $P,Q$ are propositions, then
    • Additive conjunction: $P\& Q$ is a proposition. (Read: $P$ with $Q$.)
    • Additive disjunction: $P\oplus Q$ is a proposition. (Read: $P$ plus $Q$.)
    • Multiplicative conjunction: $P\otimes Q$ is a proposition. (Read: $P$ times $Q$.)
    • Multiplicative disjunction: $P\dualampersand Q$ is a proposition. (Read: $P$ par $Q$.)
    • Exponential conjunction: $!P$ is a proposition. (Read: of course $P$.)
    • Exponential disjunction: $?P$ is a proposition. (Read: why not $P$.)
  • Constants:
    • Additive truth: $\top$,
    • Additive falsity: $\mathbf{0}$,
    • Multiplicative truth: $\mathbf{1}$, and
    • Multiplicative falsity: $\bot$.

To derive logical statements, the following inference rules are deemed valid:3 (The variables $\Gamma,\Lambda,\Theta$ and $\Delta$ indicate general contexts.)

  • Identity*: If $P$ is a proposition, then $P\vdash P$.
  • Exchange*: Sequents remain valid under permutations:
\[\begin{aligned} &\Gamma,\Lambda\vdash\Theta\\ \hline &\Lambda,\Gamma\vdash\Theta \end{aligned}\]

and, conversely,

\[\begin{aligned} &\Gamma\vdash\Delta,\Theta\\ \hline &\Gamma\vdash\Theta,\Delta \end{aligned}\,.\]
  • Restricted weakening*: If $P$ is a proposition, then
\[\begin{aligned} &\Gamma\vdash\Theta\\ \hline \Gamma,&!P\vdash\Theta \end{aligned}\]

and, dually,

\[\begin{aligned} &\Gamma\vdash\Theta\\ \hline \Gamma&\vdash\Theta,?P \end{aligned}\,.\]
  • Restricted contraction*: If $P$ is a proposition, then
\[\begin{aligned} !P&,!P\vdash\Theta\\ \hline &!P\vdash\Theta \end{aligned}\]

and, dually,

\[\begin{aligned} \Gamma&\vdash?P,?P\\ \hline &\Gamma\vdash?P \end{aligned}\,.\]
  • Negation: If $P$ is a proposition, then
\[\begin{aligned} &\Gamma\vdash\Theta,P\\ \hline &\Gamma,P^\ast\vdash\Theta \end{aligned}\]

and, conversely,

\[\label{quantum_information:negation_rule} \begin{aligned} &\Gamma,P\vdash\Theta\\ \hline &\Gamma\vdash\Theta,P^\ast \end{aligned}\,.\]

Note that these negation rules allow to write any sequent in a one-sided form, e.g. $\vdash\Gamma^\ast,P$. Moreover, these two rules also imply that $P\cong P^{\ast\ast}$.

  • Additive conjunction: If $P,Q$ are propositions, then

\begin{gather} \label{additive_conjunction} \begin{aligned} &P\vdash\Theta\\
\hline P&\& Q\vdash\Theta \end{aligned} \qquad \begin{aligned} &Q\vdash\Theta\\
\hline P&\& Q\vdash\Theta \end{aligned} \end{gather}

and, conversely,

\[\begin{aligned} \Gamma\vdash&P\qquad\Gamma\vdash Q\\ \hline &\Gamma\vdash P\&Q \end{aligned}\,.\]
  • Additive disjunction: If $P,Q$ are propositions, then

\begin{gather} \label{additive_disjunction} \begin{aligned} &\Gamma\vdash P\\
\hline \Gamma&\vdash P\oplus Q \end{aligned} \qquad \begin{aligned} &\Gamma\vdash Q\\
\hline \Gamma&\vdash P\oplus Q \end{aligned} \end{gather}

and, conversely,

\[\begin{aligned} P\vdash&\Theta\qquad Q\vdash\Theta\\ \hline &P\oplus Q\vdash\Theta \end{aligned}\,.\]
  • Multiplicative conjunction: If $P,Q$ are propositions, then
\[\begin{aligned} P,Q&\vdash\Theta\\ \hline P\otimes Q&\vdash\Theta \end{aligned}\]

and, conversely,

\[\begin{aligned} \Gamma\vdash&P\qquad\Lambda\vdash Q\\ \hline \Gamma,&\Lambda\vdash P\otimes Q \end{aligned}\,.\]
  • Multiplicative disjunction: If $P,Q$ are propositions, then
\[\begin{aligned} &\Gamma\vdash P,Q\\ \hline \Gamma&\vdash P\dualampersand Q \end{aligned}\]

and, conversely,

\[\begin{aligned} P\vdash&\Delta\qquad Q\vdash\Theta\\ \hline P&\dualampersand Q\vdash\Delta,\Theta \end{aligned}\,.\]

Note that the four rules above imply both

\begin{gather} \label{two_tensors} \begin{aligned} P\vdash\Delta\qquad Q\vdash\Theta\\
\hline P\otimes Q\vdash\Delta\otimes\Theta\ \end{aligned} \qquad\text{and}\qquad \begin{aligned} P\vdash\Delta\qquad Q\vdash\Theta\\
\hline P\dualampersand Q\vdash\Delta\dualampersand\Theta\ \end{aligned}\,, \end{gather} i.e. the two multiplicative connectives could be interchanged (this fact will be recalled in the section on categorical semantics).

  • Truth and falsity:
\[\begin{aligned} \Gamma\vdash\top &\qquad \mathbf{0}\vdash\Theta\\ \begin{aligned} \Gamma&\vdash\Theta\\ \hline \Gamma,&\mathbf{1}\vdash\Theta \end{aligned} &\qquad \vdash\mathbf{1} \\ \begin{aligned} &\vdash\Theta\\ \hline &\vdash\Theta,\bot \end{aligned} &\qquad \bot\vdash\,. \end{aligned}\]
  • Exponential conjunction: If $P$ is a proposition, then
\[\begin{aligned} P&\vdash\Theta\\ \hline !P&\vdash\Theta \end{aligned}\]

and, conversely, whenever $\Gamma$ consists solely of $!$-propositions and $\Theta$ consists solely of $?$-propositions,

\[\begin{aligned} \Gamma&\vdash P\\ \hline \Gamma&\vdash!P \end{aligned}\,.\]
  • Exponential disjunction: If $P$ is a proposition, then
\[\begin{aligned} \Gamma&\vdash P\\ \hline \Gamma&\vdash?P \end{aligned}\]

and, conversely, whenever $\Gamma$ consists solely of $!$-propositions and $\Theta$ consists solely of $?$-propositions,

\(\begin{aligned} P&\vdash\Theta\\ \hline ?P&\vdash\Theta \end{aligned}\,.\)

The inference rules with an asterisk are the structural rules. Note that a cut-elimination theorem holds and, hence, the identity and cut rules for general propositions can be derived from the rules above.

Linear implication is characterized as follows:

\[P\vdash Q \iff \vdash P^\perp\dualampersand Q \iff \vdash P\multimap Q\,.\]

Will be completed!

The relation between linear logic and quantum logic and, more specifically, the no-cloning and no-deletion theorems is given by the absence of the weakening and contraction rules. The contraction rule implies that given a sequent $\Gamma\otimes\Gamma\vdash\Theta$ also the sequent $\Gamma\vdash\Theta$ holds. Especially with the next section in mind, this means that if one needs two copies of $\Gamma$ to derive $\Theta$, the contraction rule would imply that one copy actually suffices. Hence, a copy operation should exist, which is exactly forbidden in quantum mechanics by the no-cloning theorem.

Similarly, the weakening rule would imply that one can freely adjoin any proposition to a sequent, i.e. $\Gamma\vdash\Theta$ would imply $\Gamma\otimes P\vdash\Theta$. However, this means that, although $P$ is not required, it is still ‘used up’ and, hence, discarded during the process. In quantum mechanics, this would violate the no-deleting theorem. Do not that the following inference is valid:

\[\begin{aligned} \Gamma\vdash&\Theta \qquad\qquad P\vdash P\\ \hline &\Gamma\otimes P\vdash\Theta\otimes P\,, \end{aligned}\]

where the proposition $P$ is simply passed along. (This follows from the rules for identities and multiplicative conjunction.)

The exponential modalities change this behaviour. The modal types $!P$ and $?P$ (or rather $(?P)^\ast$) behave like (classic) intuitionistic propositions in that contraction and weakening hold on the left-hand side of sequents. This means that these can be copied (or discarded) as many times as one needs.

Resource interpretation

So, one has four connectives: $\otimes$, $\dualampersand$, $\&$ and $\oplus$. Although they satisfy vaguely similar rules compared to conjunction and disjunction in classical logic, it would be nice to give a more hands-down interpretation. This will be achieved through the notion of ‘resources’. Especially the ‘linear’ aspect will be elucidated this way.

To this end, one can interpret a proposition $P$ as a ‘basket of resources’, e.g. 1kg of apples or 1 dollar. The inference rules for the logical connectives can then be interpreted as follows:

  • Additive conjunction Eq. $\eqref{additive_conjunction}$: If one can use either of the resources $P,Q$ to produce $\Theta$, then having a storage with both of them is also sufficient to produce $\Theta$. The connective $\&$ signifies that both resources are separately available.
  • Additive disjunction Eq. $\eqref{additive_disjunction}$:
  • Multiplicative conjunction:
  • Multiplicative disjunction:

Will be completed!

Extras

Will be completed! (The Bohr topos will be introduced here. Yes, that means more category theory!)

References
Footnotes

  1. Also called the ‘no-erasure’ theorem. ↩

  2. The phase factor $e^{i\alpha(\phi,\psi)}$ is a consequence of the projective nature of quantum mechanics. ↩

  3. The form of these rules heavily depends on the exchange rule (the second item). Care must be taken if this rule is weakened. ↩