Metamath Home 
Quantum Logic Explorer Home Page  First > Last > 
Quantum Logic Explorer You are about to enter uncharted territory. Unlike elementary Set Theory which is polished and mature mathematics, Quantum Logic is wild and barely explored. An ornery, intractable logic, nobody even knows if it's decidable! (In other words no one knows if an algorithm is even possible that tells you if a given expression is a theorem, much less what such an algorithm might look like.) These pages contain a collection of around 1,000 proofs of my own, my colleague Mladen Pavičić [external], and others. My own proofs are experiments to scout out new terrain, often finding it barren but occasionally stumbling on a small gem or two. All proofs are complete and correct though, verified by the Metamath program with the database file ql.mm. 
Contents of this page 
Related pages

There are other slightly different, but related, definitions of quantum logic. Some authors use "quantum logics" to mean orthomodular posets [external], whose equations are weaker than those for orthomodular lattices and therefore apply to a larger class of algebras. (An algebra is a set of elements together with operations on those elements. The class of all algebras that obey a given set of equations is called an equational variety.) Other authors mean a propositional calculus based on orthomodular lattices. Below we show how to translate our quantum logic equations to and from this propositional calculus, which is similar to translating the equations for Boolean algebras to and from ordinary classical propositional calculus.
Does quantum logic have anything to do with qubits or quantum computing? The brief answer is "no," and if that's what you are interested in you have probably come to the wrong place. However, there is a connection  our quantum logic, with some additional axioms, determines an infinite dimensional Hilbert space over the field of complex numbers (proved by Maria Solèr in 1995 and refined by René Mayet in 1998 [MegPav2000]). Hilbert space, in turn, provides the theoretical foundation for quantum mechanics and thus quantum computing. But a theory that allows our quantum logic results to be exploited in a practical sense for quantum computing has so far remained an elusive unsolved problem.
Quantum logic together with the additional axioms needed for Solèr's theorem is called the theory of Hilbert lattices. Hilbert lattices and Hilbert space provide dual and equivalent foundations for quantum mechanics, just as the frequency domain and the time domain provide dual descriptions of electrical signals. Just as Fourier transforms have led to greater insight into the nature of electrical signals, it may be possible that, via Solèr's theorem, quantum logic and Hilbert lattices will lead to new results in quantum mechanics. Since Solèr's theorem is so new, very little is known, making the theory of Hilbert lattices an interesting and exciting topic to explore.
The first two sets of axioms are show below in this section, and the stronger axioms are discussed in the section Stronger Systems below. Whereas the first two sets of axioms have been widely studied, only a few of the stronger axioms, such as the Godowski and orthoarguesian equations discussed below, are known; it is known that they are infinite in number, but it is not known whether they are recursively enumerable.
The theory of ortholattices is decidable, meaning that given any equation, there is an algorithm that will either find a proof for it or show that it is not a theorem. (William McCune wrote a program called olfilter [external] that implements Brun's decision procedure for ortholattices.) It is not known whether the theory of orthomodular lattices, as well as the theories involving the stronger axioms, are decidable, although equations with only two variables are decidable. (The program beran implements the decision procedure for orthomodular lattice equations with two variables. The program lattice is a handy preliminary filter that tests orthomodular lattice conjectures with three or more variables against a collection of useful counterexamples.)
All axioms involve two primitive operations: a negationlike unary postfix operation called orthocomplementation wn (), and an ORlike binary operation called join (or disjunction or supremum) wo (). (The join should not be confused with the union operation of set theory. The symbol is a traditional one used in this field.) Formally, an ortholattice or an orthomodular lattice is an algebra A, , where A is the base set, is a binary operation, and is a unary operation, obeying the axioms below for an ortholattice or orthomodular lattice respectively.
The axioms for an ortholattice are the following equations and inferences. For completeness, we include axioms for equality that are necessary for any algebra. The and are informal symbols indicating the relationship between hypotheses and conclusion.
axa1  
axa2  
axa3  
axa4  
axa5  
axr1  
axr2  
axr4  
axr5 
To these we add the orthomodular law, which turns the equational system for ortholattices into the stronger equational system for into orthomodular lattices.
axr3 
Some convenient definitions are equivalence (or biconditional or identity), meet (or conjunction or infimum or AND), unit (or true), and zero (or false). Note that the theorem tt justifies our definition of the unit (needed since there is a free variable on the righthand side that is not on the lefthand side).
dfb  
dfa  
dft  
dff 
With these definitions, the orthomodular law can be rewritten more compactly:
r3a 
For the complete list of syntax and definitions, see the definition list.
Only relatively recently it was discovered that equations stronger than just the orthomodular lattice axioms hold in this algebra. An important open problem is identifying all such equations.
id  
or1  
an1  
oridm 
Any theorem that is equivalent to the orthomodular law axiom axr3 (in the presence of the ortholattice axioms) is called an orthomodular law (OM law). Without axr3, quantum logic is decidable; with it decidability is unknown. The following version of the OM law, derived using axr3, is frequently used.
oml 
An outstanding feature of quantum logic compared to ordinary Boolean algebras is that the distributive law of conjunction (AND) over disjunction (OR) fails, i.e., the system lacks this law. The FoulisHolland theorems (proved independently by Foulis and Holland) provide weak but very useful versions of the distributive law. The relation " ", defined as " ", is read " commutes with " (see dfc1).
fh1  
fh2  
fh3  
fh4 
There are several interesting "exchange theorems" involving the "commutes" relationship. One of them is GudderSchelp's Theorem, later strengthened by Beran.
gsth2 
Another remarkable distributive law was discovered by Marsden and Herman. The hypotheses for this law state that the variables form a commutative "chain."
mh2 
One consequence of the MarsdenHerman law is the following interesting distributive law involving the biconditional. Previously it was known only that this law followed from the stronger Godowski equations [MegPav2001]; here we show a new proof [MegPav2003a] that requires only the axioms for orthomodular lattices.
distid 
The complete list of theorems in the Quantum Logic Explorer database is provided by the theorem list.
dfi1  
dfi2  
dfi3  
dfi4  
dfi5 
Attempts to justify the "true" implication has been a topic of much investigation and philosophical debate. So we were surprised to discover [PavMeg1998b] that they can all be unified into one, allowing a quantum logic axiom system to be devised with a "universal" implication (which could be any one of the five) and negation as the only primitives.
The way this is done is as follows. We show that disjunction is equivalent to (and thus can be defined by) a structural formula with an arbitrary implicational connective that could be any one of the five. We then use this formula for disjunction to replace the disjunction symbol in a formulation (axiom system) of quantum logic with disjunction and negation as the only primitives. This gives us an axiom system with only implication and negation as the only primitives, where the implication can be any one of the five.
Here are the structurally identical formulas for disjunction in terms of implication. Pretty neat, don't you think? Their proofs are quite tedious, though  take a peek at them.
ud1  
ud2  
ud3  
ud4  
ud5 
axwom  
woml6  
ka4ot 
In a WOM system we can prove a set of theorems that are isomorphic to (structurally resemble) the axioms and rules of orthomodular lattices. The analogous theorem is created by replacing "" with "" in an orthomodular lattice theorem, then suffixing it with " ". This means that the axiom system for for orthomodular lattices can effectively be embedded in a strictly weaker subset of itself! In particular, decidability of the weaker system implies decidability of the stronger one and viceversa. (The decision problem is one of the most important unsolved problems in quantum logic.) Counterintuitively, wr3, which is the structural analog for the orthomodular law axr3, can be proved with only the ortholattice axioms and does not require even the WOM law (whereas axr3 is the OM law). However, the structural analogs for an ortholattice's axr2 and axr5 (which are really nothing more than equality laws holding in any algebra) do require the WOM law. In each particular case, the axioms used for the proof are shown below the proof in the page referenced by the hyperlink; note that axr3 is not used for any of them.
wa1  
wa2  
wa3  
wa4  
wa5  
wr1  
wr2  
wr3  
wr4  
wr5 
These structural analogs to the orthomodular lattice axioms come in handy for proving various properties of weakly orthomodular systems. We can prove a theorem in the normal way with the standard axioms, then mimic the proof with the structural analogs above to obtain the weakly orthomodular analog. For example, we can derive weakly orthomodular analogs of the FoulisHolland theorems: wfh1, wfh2, wfh3, and wfh4. Note that for each of these, axr3 is never required for the proof, but only axwom.
A very interesting result [PavMeg1998a] is that we can derive the structural analog of the OM law oml without referring even to axwom! In the past it seems it was believed that this law supplied the orthomodular property for quantum propositional calculus axiomatizations called "unary logics," but instead it turns out to be a law of pure ortholattice theory. Thus we call it the "faux orthomodular law." In fact, the (weakly) orthomodular property for such logics is hidden in the innocentlooking wr5, which has the appearance of a simple equality axiom. Such are the surprises to be found in quantum logic.
woml 
What is particularly interesting is that quantum propositional calculus can be modeled by any WOM lattice. The class of WOM lattices includes all orthomodular lattices but some nonorthomodular ones as well. For example, a hexagonalshaped WOM lattice called O6 is nonorthomodular, but is still a model for quantum propositional calculus. This apparently was not known prior to 1998 [PavMeg1998a] [PavMeg1999].
Quantum propositional calculus can be formalized with modus ponens as its sole rule of inference,and negation and implication as its sole primitive connectives, as long as we use for the implication either (wi0) or (wi3). Kalmbach proved that these are the only two implications that work. We prove soundness for her axiom system as theorems ska1, ska2 (500K), ska3, ska4, ska5, ska6, ska7, ska8, ska9, ska10, ska11, ska12, ska13, ska14, ska15, and (for the two possible rules) skr0 and skmp3. In the soundness proofs, we never use the orthomodular law axr3, but only the weaker WOM law axwom, so these theorems provide a rigorous proof that the full strength of orthomodular lattice theory is not needed for quantum propositional calculus.
Classical propositional calculus has nonBoolean lattice models Related to this and even more surprising is that classical propositional calculus can be modeled by a nonBoolean lattice [PavMeg1999], a fact apparently overlooked for over 100 years! Common intuition is that classical propositional calculus and Boolean algebras go handinhand. Lattice O6 is a counterexample that shows this intuition is false. Specifically, lattice O6 is a model for classical propositional calculus, but it violates the axioms for Boolean algebras (the distributive law fails). This is proved as follows. If we define ab as ab, then the 3 axioms of classical propositional calculus evaluate to 1 (true), and modus ponens is sound. So O6 is a model for classical propositional calculus. However, the distributive law x(yz)=(xy)(xz) fails in this lattice: Let x=a, y=b, z=b. Then x(yz)=a(bb)=a1=a, but (xy)(xz)=(ab)(ab)=b0=b. Therefore lattice O6 is a nondistributive model for classical propositional calculus.
More generally, classical propositional calculus can be modelled by a class of algebras known as "weakly distributive ortholattices" (WDOLs), which in general are nonBoolean. In particular, O6 is a WDOL. The WDOL axiom (which when added to an ortholattice, provides an equational base for WDOLs) is axwdol. The theorems from there to the end of the database are currently (as of 16Mar2006) WDOL theorems.
It turns out that Hilbert space obeys not only the equations of orthomodular lattices but some stronger equations as well. This was not known until 1975, when Alan Day discovered the "orthoarguesian law," an equation closely related to a famous law of projective geometry discovered by Desargues in the 1600's as part of an effort to help artists, stonecutters, and engineers.
The orthoarguesian (4OA) law can be added as an additional axiom to orthomodular lattices to obtain an axiom system that is stronger than that for orthomodular lattices but still true in . This axiom system is still weaker than that for Boolean algebras because the distributive law does not hold, so the resulting axioms fall somewhere between those for orthomodular lattices and those for Boolean algebras. We have studied the 4variable 4OA law as well as a weaker 3variable consequence called 3OA [MegPav2000]. The 3OA law was originally found by Godowski and Greechie and is easier to work with. Many of the properties of 3OA can be easily generalized to 4OA, and that is one of the reasons to investigate 3OA as well as the more general 4OA. (See wle for the notation "".)
ax3oa  
ax4oa 
The original discovery of Alan Day was an inference rule involving 6 variables. Our 4OA equation is equivalent to it in the presence of the orthomodular lattice axioms. Below we show the original orthoarguesian law as a theorem derived from 4OA.
oa6 
Using the orthoarguesian law we can derive distributive laws that are stronger than those provided by the FoulisHolland theorems. Below we show two of them, derived respectively from 3OA and 4OA. In fact, they can be shown to be equivalent to 3OA and 4OA respectively. Theorem d4oa, not shown here, derives 4OA from the second distributive law below. (See wi0 for the notation "".) While the hypotheses for these laws are complex and nonintuitive, look at the conclusion  there you will see the distributive law.
oadistd  
4oadist 
Recently [MegPav2000] we found an infinite series of even stronger orthoarguesianlike laws that hold in Hilbert space, that we call 5OA, 6OA, 7OA... with 5, 6, 7... variables. We proved that 5OA is strictly stronger than 4OA [MegPav2000] and more recently that 6OA is strictly stronger than 5OA and that 7OA is strictly stronger than 6OA (a task that took many CPU years of computer time on a supercomputer cluster). The status of the higherorder ones is unknown but they are conjectured to be even stronger.
There are currently no theorems involving 5OA and up in the Quantum Logic Explorer, but a proof that 5OA holds in Hilbert space is shown in the Hilbert Space Explorer. A proof that 5OA is strictly stronger than 4OA is provided by orthomodular lattice L467 (found by our computer search), shown in the form of a "Greechie diagram" in the figure. Lattice L467 provides a counterexample that holds in 4OA but not in 5OA. (Greechie diagrams provide a compact way of representing orthomodular lattices. Reference 9, PDF file p. 13 has a tutorial explaining how they correspond to lattices. The Greechie diagram for L467 represents a 46node lattice.)
As n increases, the formula for nOA grows quite long and is inconvenient to work with directly. In the box below we show an abbreviated notation for nOA used in Reference 7.
Another set of stronger equations that hold in Hilbert space is derived from the properties strong states on a Hilbert lattice. One family of these was discovered by Godowski in 1981. The simplest one is the 3variable Godowski equation. In the Quantum Logic Explorer, we prove that two equations from the literature, gomaex3 and gomaex4, apparently believed to be independent of Godowki's, in fact follow from them [MegPav2000]. Recently we found a series of new equations related to strong states, holding in the set of closed subspaces of Hilbert space, that are independent from Godowski's. These have not been published yet. The simplest one is shown below.
(See also the References for the Hilbert Space Explorer.)
This
page was last updated on 8Jun2014. Your comments are welcome: Norman Megill Copyright terms: Public domain 
W3C HTML validation [external] 