The following discussion was inspired by a comment on Vanessa Kosoy's Shortform regarding affine infradistributions. I expect the results here would not be considered surprising or novel by an expert in quantum logic or lattice theory. In particular [HTZ16^[1]] shows the unsolvability of the problem described below, and [HZ10^[2]] covers many related results as well. However, I haven't found this exact result written down anywhere, and I expect this beginner-friendly and mostly self-contained exposition to be useful for a reader interested in a glance into quantum logic.

Setup

The term "quantum logic" is often used to refer to the structure formed by subspaces of a Hilbert space (thought of as quantum propositions). The analogs of logical 'and', 'or', and 'not' are taken to be the operations of intersection, sum, and complements of subspaces, respectively. We can loosen this structure by dropping the inner product (so downgrading our Hilbert space to just a vector space), and hence the notion of orthogonal complements. We can call the resulting simplified logic "non-unitary" (for the lack of an inner product) quantum logic. We'll restrict our attention to the finite dimensional case. The following is the corresponding syntax and semantics.

Syntax

Let $P$ be a set of propositional variables. We define the set $L$ of well-formed formulas recursively as follows.

• Two special symbols $\top ,\perp \in L$,
• For any $p\in P$, we have $p\in L$,
• For any $\varphi ,\psi \in L$, we have $\varphi \wedge \psi \in L$, and $\varphi \vee \psi \in L$.

A theory $T$ is a subset $T\subset L\times L$. Elements of $T$ are written $\varphi ⊢\psi$. We'll write $\varphi =\psi$ for when both $\varphi ⊢\psi$ and $\psi ⊢\varphi$.

Semantics

For a vector space $V$, let $\mathrm{Sp}\left(V\right)$ denote the set of all linear subspaces of $V$.

Definition 1. A model consists of a finite dimensional vector space $V$, and a map $M:L\to \mathrm{Sp}\left(V\right)$, satisfying the following:

• $M\left(\perp \right)=0$ (the subspace consisting of the zero vector)
• $M\left(\top \right)=V$
• $M(\varphi \vee \psi )=M\left(\psi \right)+M\left(\varphi \right)$
• $M(\varphi \wedge \psi )=M\left(\psi \right)\cap M\left(\varphi \right)$.

We say $M$ models the theory $T$, if $M\left(\varphi \right)\subset M\left(\psi \right)$ for every $\varphi ⊢\psi$ in $T$.

Lattices

The set $\mathrm{Sp}\left(V\right)$ forms a lattice under '$\cap$' and '$+$', with partial order given by '$\subset$'. Thus the map $M$ defining the model factors through the lattice quotient of the language $L$ (this is the free bounded lattice generated by the propositional variables, which we'll also call $L$ by abuse of notation).

Given a theory $T$, we can take the quotient of the lattice $L$ by the relations specified in $T.$ More precisely we quotient by the congruence relation $\theta$ generated by $T$ as follows. We can replace each $\varphi ⊢\psi$ by $\varphi \wedge \psi =\varphi$, so we can assume $T$ only contains equalities. Then we define the congruence relation $\theta$ as the smallest congruence relation for which $\varphi {\sim }_{\theta }\psi$ whenever $\varphi =\psi$ is in $T$. Taking the quotient by this congruence relation we end up with a lattice corresponding to $T$, which we'll denote $L\left(T\right)=L/\theta$. If $M$ models $T$, then $M$ factors as a lattice homomorphism $L\left(T\right)\to \mathrm{Sp}\left(V\right).$

Example

For example, if $T$ consists of $a\wedge b=\perp$, and $a\vee b⊢c$, we end up with the following lattice $L\left(T\right)$:

Classical vs Quantum Logic

In classical (Boolean) logic, a model would be a lattice homomorphism from $L$ to $P\left(X\right)$, the lattice of subsets of a set $X$, while in quantum logic we use the lattice of subspaces of a vector space. The key characteristic of classical logic is the distributive property: 

 and its dual.

Note that any classical model of a theory also gives rise to a quantum model by taking the vector space $V$ with basis the set $X$, and composing with the lattice homomorphism $P\left(X\right)\to \mathrm{Sp}\left(V\right)$ given by span.

Example: the double slit experiment

It's educational to consider an example of a non-classical quantum logic. Consider 3 events $A$, $B$, and $C$ (can be thought of as a particle passing through the first slit, passing through the second slit, and hitting the screen at a given point, respectively), whose corresponding propositions form the following non-distributive lattice (called $M_3$):

It is easy to see that $M_3$ cannot be represented as a lattice of subsets due to the failure of distributivity. However, we can model $M_3$ as three distinct lines in the lattice of subspaces of the plane.

Consistency in Quantum Logic

We call a theory $T$ consistent if it has a non-trivial (i.e. where $M\left(\top \right)\ne M\left(\perp \right)$) model. Boolean consistency (or satisfiability) is well-know to be NP-hard, so it's natural to ask about the complexity of deciding consistency in the quantum setting.

One immediate necessary criterion for consistency can be seen as follows. If $M:L\left(T\right)\to \mathrm{Sp}\left(V\right)$ is a lattice homomorphism, then by taking the dimension of subspaces, we get a map $d=\dim \left(M\right):L\left(T\right)\to N$ satisfying the following properties:

• $d\left(\perp \right)=0$, and $d\left(\top \right)=\dim \left(V\right)>0$
• $d\left(a\right)\le d\left(b\right)$ whenever $a\le b$
• $d\left(a\right)+d\left(b\right)=d(a\vee b)+d(a\wedge b)$.

We might wonder whether the existence of such a $d$ is sufficient.

Conjecture 2. Given a dimension function $d$ as above, there exists a linear representation of $L\left(T\right)$ with dimensions as specified by $d$.

If this conjecture were true, that would mean the existence of a polynomial time algorithm to check quantum satisfiability (since finding such a $d$ is a linear programming problem). As it turns out, the conjecture is false, which we show in Counterexample 2. Hence the proposed simple polynomial time algorithm to check quantum consistency doesn't work. Indeed, quantum consistency turns out to be unsolvable^[1].

Lattice Theory Prerequisites

Modular lattices

Vector subspaces have the property that if $U\subset V$ and $\dim \left(U\right)=\dim \left(V\right)$ then $U=V$. So any linear representation of the lattice $L\left(T\right)$ would factor through the quotient lattice where if $a\le b$ and $d\left(a\right)=d\left(b\right)$ we identify $a$ and $b$. The resulting quotient lattice $\overline{L\left(T\right)}$ and the induced map $\overline{d}$ would satisfy a stronger version of the properties 1-3 above, where in 2 we now have $d\left(a\right)<d\left(b\right)$ whenever $a<b$. It turns out that lattices with such a function $\overline{d}$ are exactly the modular lattices (with the additional property of every bounded chain being finite). These results are spelled out in point 7 and Theorem 9 of Chapter V in [Bir40^[3]].

Thus Conjecture 2 boils down to whether these modular lattices always have non-trivial linear representations. This seems somewhat unlikely at first glance, since linear subspace lattices need to satisfy additional properties, e.g. the arguesian property (discussed further in the "Arguesian lattices" section), and indeed in Counterexample 9 we show that this is not the case.

Definition 3. For $a,b\in L$ in a lattice, the quotient (also called the interval) $\left[a/b\right]$ is the sublattice 

Definition 4. For any $x,y\in L$ in a lattice we say the quotients $[x\vee y/y]$ and $[x/x\wedge y]$ are projective (to each other). So being projective is the equivalence relation generated by these pairs of quotients.

Definition 5. A quotient $\left[a/b\right]$ is called prime if $b<a$, but there's no $x$ such that $b<x<a$.

Lemma 6. A modular lattice of finite length is simple (i.e., without proper congruence relations) if and only if all its prime quotients are projective (to each other). Note that being simple means having no proper non-trivial quotients.

Proof. This is Corollary 1 in Chapter V, Section 7 of [Bir40^[3]]. We only need the simpler "if" direction here, which is fairly straightforward to see directly as follows. If $\theta$ is a congruence relation on $L$, then $x{\sim }_{\theta }x\vee y$ implies $x\wedge y{\sim }_{\theta }(x\vee y)\wedge y=y$, and the dual claim also holds. So if a certain quotient is annulled by $\theta$ (i.e. made equivalent) then so is every projective quotient.

Now assume $\theta$ is non-trivial, so $x{\sim }_{\theta }y$ for some $x\ne y$. Then also $x\vee y{\sim }_{\theta }y{\sim }_{\theta }x\wedge y$. Since $L$ is finite length, there is some $x\wedge y\le \tilde{x}\le x\vee y$ with $[x\vee y/\tilde{x}]$ prime (and $x\vee y{\sim }_{\theta }\tilde{x}$). Then by the above every prime quotient is annulled by $\theta$, which in a finite length lattice implies that $\theta$ annuls everything. ◻

Arguesian lattices

Definition 7. A modular lattice $L$ is called arguesian if for any $a_i,b_i\in L$ ($i=0,1,2$), 

 implies 

 where $c_i=(a_j\vee a_k)\wedge (b_j\vee b_k)$ ($\{i,j,k\}=\{0,1,2\}$).

This is the lattice-theoretic formulation of Desargues' theorem, considering the incidence lattice of a projective space:

Lemma 8. For any ring $R$, the lattice of submodules $L\left(M\right)$ of a (left) $R$-module $M$ is an arguesian lattice. In particular any sublattice of $L\left(M\right)$ is also arguesian.

Proof. Let $A_i$, $B_i$ be submodules such that the assumption in the arguesian property 

 is satisfied. Let $C_i=(A_j+A_k)\cap (B_j+B_k)$. We want to show that $C_2\subset C_0+C_1$. Let ${\gamma }_2\in C_2$, so by definition 

 for ${\alpha }_i\in A_i$, and ${\beta }_i\in B_i$. Now 

 so by (1) we have $x\in A_2+B_2$, i.e. $x={\alpha }_2+{\beta }_2$ for ${\alpha }_2\in A_2$ and ${\beta }_2\in B_2$. But then 

 and 

 so 

 as required. ◻

A Counterexample

Counterexample 9. Conjecture 2 fails for the incidence lattice $L$ of a finite non-Desarguesian projective plane. Note that the smallest such plane has $91$ points, which corresponds to a theory $T$ on $91$ propositional variables.

Proof. The lattice $L$ is modular (an explicit dimension function $d$ can be defined by $d\left(point\right)=1$, and $d\left(line\right)=2$ for all points and lines). Being the incidence lattice of a non-Desarguesian plane, $L$ is not arguesian. This lattice also turns out to be simple (i.e. without any smaller non-trivial quotients), and so by Lemma 8 it cannot have a non-trivial linear representation. The fact that $L$ is simple follows from Lemma 6 after showing that all prime quotients are projective for this incidence lattice.

First consider a point $p$ in the projective plane, and let ${\ell }_1,{\ell }_2,{\ell }_3,\dots$ be the distinct lines through $p$. Then by definition (using ${\sim }_p$ here to denote intervals projective to each other) $\left[\top /{\ell }_i\right]{\sim }_p\left[{\ell }_j/p\right]$, and $\left[\top /{\ell }_j\right]{\sim }_p\left[{\ell }_i/p\right]$ for any $i\ne j$. Since there are at least three lines through $p$, this then implies all of $\left[\top /{\ell }_i\right]$, and $\left[{\ell }_i/p\right]$ are projective to each other for all $i$ by transitivity.

Now let $q$ be a point distinct from $p$, and let $\ell$ be the line through $p$ and $q$. Then from the above $\left[\top /\ell \right]$ is projective to both $\left[\ell /p\right]$ and $\left[\ell /q\right]$, which in turn are projective to $\left[p/\perp \right]$ and $\left[q/\perp \right]$.

Putting all of these together, since any line contains at least one point, we can deduce that in fact all prime quotients are projective to each other in the incidence lattice. ◻

To construct a theory $T$ from Counterexample 9, we can introduce propositional variables $P_i$ corresponding to the points $p_i$ of the projective plane, $L_i$ corresponding to the lines ${\ell }_i$, and let $T$ contain all the following:

• $P_i\wedge P_j=\perp$ for $i\ne j$
• $L_i\vee L_j=\top$ for $i\ne j$
• $P_i⊢L_j$ if the point $p_i$ lies on the line ${\ell }_j$
• $P_i\vee P_j=L_k$ if ${\ell }_k$ is the line through $p_i$ and $p_j$ for $i\ne j$
• $L_i\wedge L_j=P_k$ if $p_k$ is the point of intersection of ${\ell }_i$ and ${\ell }_j$ for $i\ne j$.

1. ^{^}

   Christian Herrmann and Yasuyuki Tsukamoto and Martin Ziegler. On the consistency problem for modular lattices and related structures, 2016

2. ^{^}

   Christian Herrmann and Martin Ziegler. Computational Complexity of Quantum Satisfiability, 2010

3. ^{^}

   [Bir40] Garrett Birkhoff. Lattice Theory. American Mathematical Society, New
   York, 1940