Hilbert Space Explorer Home Page

Hilbert Space Explorer   

The motivation for studying quantum logic (and the related orthomodular lattices) derives from the fact that the set of closed subspaces of Hilbert space, called CH, obeys the properties of an orthomodular lattice. Hilbert space [external] underlies the foundation of quantum mechanics, and there is a strong physical and philosophical motivation to understand its properties. In addition, understanding the properties of Hilbert space is important for understanding what kinds of operations are possible in the new field of quantum computers.

Calcite

Contents of this page How to Follow the Proofs The Axioms Some Definitions Some Theorems The Axiom of Choice Quantum Logic What Next? (Orthoarguesian Law, etc.) References

Related pages Metamath Proof Explorer Home Page Quantum Logic Explorer Home Page Bibliographic Cross-Reference

How to Follow the Proofs    We develop Hilbert space theory as an extension of ZFC set theory, and many steps in various proofs use results from set theory. To understand how to read the proofs, see How Proofs Work on the Metamath Proof Explorer Home Page.

The Axioms    There are several ways to develop the theory of Hilbert spaces. The purest way, philosophically, is simply to define the class of all Hilbert spaces and use only the axioms of ZFC set theory to derive its properties. That way we need to assume only the axioms of ZFC (which in principle is all that is needed for essentially all of mathematics, including the theory of Hilbert spaces). A practical problem with this approach is that the direct definition of a Hilbert space is large and awkward to work with, unless we already have available an underlying theory of vector spaces, etc. (which at this point I do not have).

Instead, here we take a slightly different approach. We postulate the existence of a new primitive fixed object, H~ (chil), called Hilbert space, and add to ZFC set theory explicit axioms for the properties of H~.

(In the future I may convert everything to the pure approach, which will do away with the additional axioms and also allow us to prove more general theorems about Hilbert spaces. The proofs that we show here, though, would remain essentially the same.)

The members of H~ are called vectors, and they have the same properties as the vectors you normally find in any linear algebra textbook, except that the dimension (the number of basis vectors) is not specified and may be infinite. In addition to H~, we postulate the existence and properties of 4 more objects: a fixed zero vector 0v (c0v); the operations of vector addition +v (cva) and scalar multiplication .s (csm); and finally, an inner product operation .i (csp). The five objects H~, 0v, +v, .s, and .i are the complete set of objects needed to describe Hilbert space. We will encounter other objects as well, but all of them are defined either in terms of these five, or as specific sets of set theory. For example, the object CC (the set of complex numbers cc) is defined as a specific set of set theory.

Each axiom below is accompanied by a precise breakdown of its syntax, so by clicking through its links you can break the syntax down into as much detail as you want. Note our use of the notation "(A .i B)" instead of the more common notation "<.A,B>." for inner products; the latter would conflict with our notation for ordered pairs cop.

Axioms for Hilbert Space

ax-hilex	|- H~ e. V
ax-hvaddcl	|- ((A e. H~ /\ B e. H~) -> (A +v B) e. H~)
ax-hvcom	|- ((A e. H~ /\ B e. H~) -> (A +v B) = (B +v A))
ax-hvass	|- ((A e. H~ /\ B e. H~ /\ C e. H~) -> ((A +v B) +v C) = (A +v (B +v C)))
ax-hvzercl	|- 0v e. H~
ax-hvaddid	|- (A e. H~ -> (A +v 0v) = A)
ax-hvmulcl	|- ((A e. CC /\ B e. H~) -> (A .s B) e. H~)
ax-hvmulid	|- (A e. H~ -> (1 .s A) = A)
ax-hvmulass	|- ((A e. CC /\ B e. CC /\ C e. H~) -> ((A x. B) .s C) = (A .s (B .s C)))
ax-hvdistr1	|- ((A e. CC /\ B e. H~ /\ C e. H~) -> (A .s (B +v C)) = ((A .s B) +v (A .s C)))
ax-hvdistr2	|- ((A e. CC /\ B e. CC /\ C e. H~) -> ((A + B) .s C) = ((A .s C) +v (B .s C)))
ax-hvmulzer	|- (A e. H~ -> (0 .s A) = 0v)
ax-hicl	|- ((A e. H~ /\ B e. H~) -> (A .i B) e. CC)
ax-his1	|- ((A e. H~ /\ B e. H~) -> (A .i B) = (*`(B .i A)))
ax-his2	|- ((A e. H~ /\ B e. H~ /\ C e. H~) -> ((A +v B) .i C) = ((A .i C) + (B .i C)))
ax-his3	|- ((A e. CC /\ B e. H~ /\ C e. H~) -> ((A .s B) .i C) = (A x. (B .i C)))
ax-his4	|- ((A e. H~ /\ A =/= 0v) -> 0 < (A .i A))
ax-hcompl	|- (F e. Cauchy -> E.x e. H~F ~~>v x)

Comments on the axioms. The first axiom just says that the primitive class H~ exists (is a member of the universe of sets V). The next 11 axioms are the axioms for any vector space with an unspecified dimension; they are the same as those you would find in any linear algebra book, except for the notation and possibly their precise form.

The next 5 axioms show the properties of the special inner product .i. The official name for this inner product is a "sesquilinear Hermitian mapping". (Sesquilinear means "one-and-a-half linear," i.e., antilinear in the first argument and linear in the second.) The symbol * in Axiom ax-his1 is the complex conjugate (cjvalt). See Notation for Function Values for an explanation of why we use this notation rather than the standard superscript asterisk used in textbooks; this will help you understand some of our other non-standard notation as well.

The last axiom, which is the most important and also the most complicated, is called the Completeness Axiom, and is shown above using abbreviations. You can click on its links to expand the abbreviations. It basically says that the limit of any converging ("Cauchy") sequence of vectors in Hilbert space converges to a vector in Hilbert space. To understand what completeness means, consider this analogy: the sequence 3, 3.1, 3.14, 3.1415, 3.14159... converges to pi. This is a converging sequence of rational numbers, but it converges to something that is not a rational number, meaning the set of rational numbers is not complete. The set of real numbers, on the other hand, is complete, because all converging sequences of real numbers converge to a real number.

Definitions for Hilbert Space    Here are some definitions you will encounter in our Hilbert space proofs. Definitions that are part of general set theory are not included in this table, but you can always open up a syntax page (listed at the bottom of proofs) to expand the definition of any symbol you do not understand. Here are the definitions in their general form which sometimes looks unnecessarily complicated, but if you click on them their Description usually points to simpler theorems showing their values or other properties. For example, the vector subtraction operation -v is formally a set of ordered pairs as shown below, but its value is just A +v (-u1 .s B) as can be seen from theorem hvsubval.

Definitions for Hilbert Space

The vector subtraction operation df-hvsub	|- -v = {<.<.x,y>.,z>. | ((x e. H~ /\ y e. H~) /\ z = (x +v (-u1 .s y)))}
The norm of a vector df-hnorm	|- norm = {<.x,y>. | (x e. H~ /\ y = (sqr`(x .i x)))}
The set of all Cauchy sequences df-cauchy	|- Cauchy = {f | (f:NN-->H~ /\ A.x e. RR(0 < x -> E.y e. NNA.z e. NNA.w e. NN((y <_ z /\ y <_ w) -> (norm`((F`z) -v (F`w))) < x)))}
The limit of a vector sequence df-hlim	|- ~~>v = {<.f,w>. | ((f:NN-->H~ /\ w e. H~) /\ A.x e. RR(0 < x -> E.y e. NNA.z e. NN(y <_ z -> (norm`((f`z) -v w)) < x)))}
The set of all subspaces of Hilbert space df-sh	|- SH = {h | ((h (_ H~ /\ 0v e. h) /\ (A.x e. hA.y e. h(x +v y) e. h /\ A.x e. CCA.y e. h(x .s y) e. h))}
The set of all closed subspaces of Hilbert space df-ch	|- CH = {h | (h e. SH /\ A.fA.x((f:NN-->h /\ f ~~>v x) -> x e. h))}
The sum of two subspaces df-shsum	|- +H = {<.<.x,y>.,z>. | ((x e. SH /\ y e. SH) /\ z = {w e. H~ | E.v e. xE.u e. yw = (v +v u)})}

Some Theorems    First we show some basic properties of vectors. These are laws in any vector space, not just Hilbert spaces, so they should be familiar if you've taken a linear algebra course.

Some Basic Properties of Vectors

hvsubclt	|- ((A e. H~ /\ B e. H~) -> (A -v B) e. H~)
hvnegid	|- A e. H~   =>    |- (A +v (-u1 .s A)) = 0v
hvmul0t	|- (A e. CC -> (A .s 0v) = 0v)
hvsubidt	|- (A e. H~ -> (A -v A) = 0v)
hvsubeq0	|- A e. H~   &   |- B e. H~   =>    |- ((A -v B) = 0v <-> A = B)

Next we show some basic properties of the special inner product defined for Hilbert space.

Theorems Involving Inner Product

his5	|- ((A e. CC /\ B e. H~ /\ C e. H~) -> (B .i (A .s C)) = ((*`A) x. (B .i C)))
his6	|- (A e. H~ -> ((A .i A) = 0 <-> A = 0v))
his7	|- ((A e. H~ /\ B e. H~ /\ C e. H~) -> (A .i (B +v C)) = ((A .i B) + (A .i C)))

Next we show some theorems involving norms. Note our use of the notation "(norm`A)" instead of the more common notation "||A||" - see Notation for Function Values.

Theorems norm-i, norm-ii (triangle inequality), and norm-iii show that the basic properties expected of any norm hold for the norm we defined for Hilbert space. Theorem normpyth is an analogy to the Pythagorean theorem, and theorem normpar is the parallellogram law. Theorem bcs is the Bunjakovaskij-Cauchy-Schwarz inequality.

Theorems Involving Norms

norm-i	|- A e. H~   =>    |- ((norm`A) = 0 <-> A = 0v)
norm-ii	|- A e. H~   &   |- B e. H~   =>    |- (norm`(A +v B)) <_ ((norm`A) + (norm`B))
norm-iii	|- A e. CC   &   |- B e. H~   =>    |- (norm`(A .s B)) = ((abs`A) x. (norm`B))
normpyth	|- A e. H~   &   |- B e. H~   =>    |- ((A .i B) = 0 -> ((norm`(A +v B))^2) = (((norm`A)^2) + ((norm`B)^2)))
normpar	|- A e. H~   &   |- B e. H~   =>    |- (((norm`(A -v B))^2) + ((norm`(A +v B))^2)) = ((2 x. ((norm`A)^2)) + (2 x. ((norm`B)^2)))
bcs	|- A e. H~   &   |- B e. H~   =>    |- (abs`(A .i B)) <_ ((norm`A) x. (norm`B))

Next we show some basic theorems about sequences. Theorem hlimcau shows any converging sequence is a Cauchy sequence and hlimuni shows that the limit of a converging sequence is unique. The theorem pjth is the important Projection Theorem; it shows any vector can be decomposed into a pair of "projections" on a subspace and the orthocomplement of the subspace (see below for the definition of the orthocomplement _|_).

Theorems Involving Limits and Subspaces

hlimcau	|- A e. V   &   |- F e. V   =>    |- (F ~~>v A -> F e. Cauchy)
hlimuni	|- A e. V   &   |- B e. V   &   |- F e. V   =>    |- ((F ~~>v A /\ F ~~>v B) -> A = B)
pjth	|- A e. H~   &   |- H e. CH   =>    |- E.x e. HE.y e. (_|_`H) A = (x +v y)

The Axiom of Choice    The example here is rather technical and not very interesting in itself (it is used to prove the Projection Theorem pjth), except that it shows how a seemingly innocent, simple assertion in a textbook proof, "Let f be a vector sequence such that..." has, implicit under it, a rather complex proof that such a sequence f actually exists. (If it didn't exist, the rules of logic would not allow us to state "Let f be...") In fact it appears impossible to prove it without invoking the Axiom of Choice - at least I could not do it. But the textbook author does not mention this. This is a disadvantage of Metamath - it won't let you gloss over hand-waving textbook arguments, so a lot of hard work may be needed to come up with a correct and complete proof. But if you want mathematical rigor, then that is an advantage.

In the proof, the Axiom of Choice is referenced in the step with ac6.

A Lemma Using the Axiom of Choice

projlem17

|- A e. H~   &   |- H e. CH   &   |- S = {u e. RR | E.v e. Hu = -u(norm`(v -v A))}   &   |- R = -usup(S,RR, < )   =>    |- E.f(f:NN-->H /\ A.w e. NN((R - (1 / w)) < (norm`((f`w) -v A)) /\ (norm`((f`w) -v A)) < (R + (1 / w))))

I think it is philosophically interesting that, in order to prove certain laws concerning the physical universe, we may need the Axiom of Choice. The Axiom of Choice can have bizarre consequences. One of them is the Banach-Tarski paradox, which shows it is possible to break up a 3-dimensional sphere into finitely many pieces, then by moving those pieces in rigid motions (rotations and translations) reassemble them to form two copies of the sphere. Of course that makes no sense from a physical point of view. Otherwise we could put a bar of gold in our Banach-Tarski reassembler and turn it into two!

(For a less simplistic discussion of the Banach-Tarski paradox, see A Home Page for the Axiom of Choice [external]. Also, the Banach-Tarski paradox cannot be derived from the weak derivative of the Axiom of Choice, called "Countable Choice," used in the proof of projlem17).

Quantum Logic   

The set of closed subspaces of Hilbert space obey the laws of a simple equational algebra called "orthomodular lattice algebra." This algebra is sometimes called "quantum logic," and it can be used as the basis for a propositional calculus that resembles but is somewhat weaker than standard (classical) propositional calculus. This is explained in greater detail in the Quantum Logic Explorer. Our purpose here is to show that the orthomodular lattice laws hold in Hilbert space. This provides a rigorous justification for the axioms of the Quantum Logic Explorer.

The the advantage of the Quantum Logic Explorer is that it lets us work with a simpler axiomatic structure. But in principle, all the theorems of the Quantum Logic Explorer could be proved directly in Hilbert space, using the theorems below as the starting point. In fact in a few cases we do this, because sometimes we need the Hilbert space version to help prove theorems that exploit Hilbert space properties beyond those provided by the orthomodular lattice laws alone. For example, compare the proofs of the Hilbert Space Explorer theorem fh1 and the Quantum Logic Explorer version fh1. If you ignore the steps with an "e." in the Hilbert space version, you'll see the proofs are almost identical except for notation. You can see why the Quantum Logic Explorer is simpler to work with for these kinds of things: we don't need the "e. CH" hypotheses, and we don't have to keep proving operation closure over and over.

To derive the orthomodular lattice postulates, first we define two new operations on members of CH (the set of closed subspaces of Hilbert space). The orthocomplement of a subspace is the set of vectors orthogonal to all vectors in the subpace. It is analogous to logical NOT. The join of two subspaces is the closure (i.e. the double orthocomplement) of their union. It is analogous to logical OR.

Lattice Definitions for CH

Orthocomplement chocval	|- A e. CH   =>   |- (_|_` A) = {x e. H~ | A.y e. A (x .i y) = 0}
Join chjval	|- A e. CH   &   |- B e. CH   =>   |- (A vH B) = (_|_` (_|_` (A u. B)))

Next we show that with these operations, we can derive the Hilbert space versions of the axioms for the Quantum Logic Explorer. You can see that these axioms correspond directly to the 10 theorems below. This provides a physical justification for the study of quantum logic (since quantum physics is based on Hilbert space) and gives us a rigorous mathematical link for quantum logic all the way from the axioms of ZFC set theory and Hilbert space. If you think of the logical OR / logical NOT analogy, you can see that these laws are a subset of the laws that hold in a Boolean algebra. They provide us with a rich and very challenging logical structure to study.

Derivation of Properties of Orthomodular Lattices (for Quantum Logic)

qlax1	|- A e. CH   =>   |- A = (_|_` (_|_` A))
qlax2	|- A e. CH   &   |- B e. CH   =>   |- (A vH B) = (B vH A)
qlax3	|- A e. CH   &   |- B e. CH   &   |- C e. CH   =>   |- ((A vH B) vH C) = (A vH (B vH C))
qlax4	|- A e. CH   &   |- B e. CH   =>   |- (A vH (B vH (_|_` B))) = (B vH (_|_` B))
qlax5	|- A e. CH   &   |- B e. CH   =>   |- (A vH (_|_` ((_|_` A) vH B))) = A
qlaxr1	|- A e. CH   &   |- B e. CH   &   |- A = B   =>   |- B = A
qlaxr2	|- A e. CH   &   |- B e. CH   &   |- C e. CH   &   |- A = B   &   |- B = C   =>   |- A = C
qlaxr4	|- A e. CH   &   |- B e. CH   &   |- A = B   =>   |- (_|_` A) = (_|_` B)
qlaxr5	|- A e. CH   &   |- B e. CH   &   |- C e. CH   &   |- A = B   =>   |- (A vH C) = (B vH C)
qlaxr3	|- A e. CH   &   |- B e. CH   &   |- C e. CH   &   |- (C vH (_|_` C)) = ((_|_` ((_|_` A) vH (_|_` B))) vH (_|_` (A vH B)))   =>   |- A = B

What Next?    At the time quantum logic was first defined, the orthomodular lattice equations for CH were the only ones that were known, and so "orthomodular lattice" and "quantum logic" became almost synonymous. Since then, equations that strengthen the system have been discovered: the orthoarguesian law [GodowskiGreechie] [click for Quantum Logic Explorer page] found by Alan Day in 1975, a family of equations discovered by Godowski in 1981, and several equations found by Mayet in 1986 [Mayet2]. It has also been proved that there are infinitely many more, but no one knows what they look like nor how to find them. From [Mayet]: "An open problem is to determine all equations satisfied by hilbertian lattices [i.e. CH], which would make possible the separation of the 'purely logic' part from the above axiomatics. It is not known if this problem is solvable, for it is not certain that these equations form a recursively enumerable set."

Recently myself and M. Pavicic [MegillPavicic] have proved that all equations appearing in the literature that are stronger than orthomodularity but valid in CH can be derived from either the 4-variable orthoarguesian equation or one of the Godowski equations. In addition we recently discovered [MegillPavicic] a family of n-variable equations generalizing the orthoarguesian equation (which can be expressed with 4 variables) that are strictly stronger than it for all members with 5 or more variables. Below we show the 5-variable member of this family (expressed as an equivalent 8-variable inference below) and also show the 3-variable Godowski equation, backed by their complete formal proofs.

5-Variable Orthoarguesian Equation (browser note: large proof, 750K)

5oa	|- A e. CH   &   |- B e. CH   &   |- C e. CH   &   |- D e. CH   &   |- F e. CH   &   |- G e.