Added to *finite quantum mechanics in terms of dagger-compact categories* a brief paragraph titled “quantum logic” reading as follows:

]]>Symmetric monoidal categories such as †-compact categories have as internal logic a fragment of linear logic and as type theory a flavor of linear type theory. In this fashion everything that can be formally said about quantum mechanics in terms of †-compact categories has an equivalent expression in formal logic/type theory. It has been argued (Abramsky-Duncan 05, Duncan 06) that this linear logic/linear type theory of quantum mechanics is the correct formalization of “quantum logic”. An exposition of this point of view is in (Baez-Stay 09).

the entry that used to be titled *quantum mechanics in terms of dagger-compact categories* I have renamed into *finite quantum mechanics in terms of dagger-compact categories* (with a “finite” up front) and I have added to the first sentence the qualifier “finite” and “finite-dimensional” a bunch of times.

I am currently at “Quantum Physics and Logic 2012” in Brussels, and every second speaker advertizes the formalism of what they call “categorical quantum theory”. It’s all fine for the majority of the audience which is all into *quantum information* theory, where one is only interested in shuffling a finite bunch of qbits around, but it is rather misleading from an ordinary perspective on quantum physics. Already the particle on the line is not a finite quantum system.