added pointer to

- Vaughan Pratt,
*The second calculus of binary relations*, Mathematical Foundations of Computer Science 1993. MFCS 1993, Lecture Notes in Computer Science**711**, Springer (1993) [doi:10.1007/3-540-57182-5_9]

with this quote:

]]>“Linear logic is seen in its best light as the realization of the Curry-Howard isomorphism for linear algebra”

added pointer to today’s

- Pavlos Kazakopoulos, Georgios Regkas,
*Infinite Permutation Groups and the Origin of Quantum Mechanics*[arXiv:2307.13044]

added pointer to:

- Erhard Scheibe, pp 71 in: _*The logical analysis of quantum mechanics&, Pergamon Press Oxford (1973)

added pointer to:

- Li Zhou, Gilles Barthe, Justin Hsu, Mingsheng Ying, Nengkun Yu,
*A Quantum Interpretation of Bunched Logic for Quantum Separation Logic*, LICS ’21: Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science 75 (2021) 1–14 [arXiv:2102.00329, doi:10.1109/LICS52264.2021.9470673]

I have added further data/links to reference items where missing

while at it, I haved re-arranged the list of references into “Original articles”, “Review and Exposition” and “Further Developments”.

can anyone get hold of an electronic copy of this item:

- G. D. Crown,
*On some orthomodular posets of vector bundles*, Journ. of Natural Sci. and Math.**15**1-2 (1975) 11-25

?

]]>The references by Gleason and by Holland used to be listed as if being about BvN. I have now added pointer to:

- George Mackey, Section 2-2 of:
*The Mathematical Foundations of Quantum Mechanics: a Lecture-note Volume*, Mathematical physics monograph series, Benjamin (1963), Dover (2004) [google books]

and grouped them with that

]]>all along, the quote here used to refer to “Abramsky 2009”, but no such reference was given and the link did not work

I have now found and added the actual reference:

- Samson Abramsky, Bob Coecke,
*Physics from Computer Science: a Position Statement*, International Journal of Unconventional Computing**3**3 (2007) [pdf, ijuc-3-3-p-179-197]

have expanded (here) the above discussion, pointing out how to recover the BvN quantum logic also inside the CCC $Vect_{Set}$ via the “quantum modality” $\mathrm{Q}$.

]]>added publication data to this item:

- Mladen Pavičić,
*Bibliography on quantum logics and related structures*, Int J Theor Phys**31**(1992) 373–455 [doi:10.1007/BF00739999, pdf]

In the section on BvN quantum logic (here) I have expanded out the previously telegraphic notes into a sequence of full sentences and formulas.

But mainly, in the previously even more telegraphic section (whose title I have expanded to) “Linear logic and dependent linear type theory” (here) I have added discussion of how the BvN formulas for logical conjunction and disjunction arise from the internal logic of slices of $FinDimVect$.

]]>Changed “linear space” to “linear span”.

]]>added pointer to:

- Samson Abramsky, Bob Coecke,
*A categorical semantics of quantum protocols*, Proceedings of the 19th IEEE conference on Logic in Computer Science (LiCS’04). IEEE Computer Science Press (2004) (arXiv:quant-ph/0402130)

and added DOI to:

- John Baez, Mike Stay,
*Physics, topology, logic and computation: a rosetta stone*, (arxiv/0903.0340); in “New Structures for Physics”, ed. Bob Coecke, Lecture Notes in Physics**813**, Springer, Berlin, 2011, pp. 95-174 (doi:10.1007/978-3-642-12821-9)

added publication data for

- Samson Abramsky, Ross Duncan,
*A Categorical Quantum Logic*, Mathematical Structures in Computer Science , Volume 16 , Issue 3 , June 2006 , pp. 469 - 489 (arXiv:quant-ph/0512114, doi:10.1017/S0960129506005275)

link to effect algebras

]]>So, as far as I know at the moment, Yetter 1990 (for posets) and Pratt 1992 (more generally) are the earliest sources saying fairly explicitly that quantum logic should be linear logic, to be regarded as the internal logic of suitable tensor categories of quantum state spaces.

I see (only) now that both these are mentioned back in TWF 40. (Would have seen that earlier, but neither is cited in Baez-Stay 09).

]]>This article

- David Yetter,
*Quantales and (noncommutative) linear logic*, Journal of Symbolic Logic 55 (1990), 41-64.

(predating Pratt’s “linear logic is quantum logic” by two years) interprets linear logic in $\ast$-autonomous posets, hence in quantales and makes some remarks in passing about relation to logic of quantum systems.

I have added a pointer to that article to *quantum logic*, to *linear logic* and to *quantale*. Moreover, in all three of these entries I have added brief paragraphs mentioning the relation of the three and containing hyperlinks.

Deserves to be further expanded.

]]>I have found more references that explicitly state the (obvious, I would say) fact that BvN lattices are just the subobject lattices hence the categorical propositions in the linear logic of categories of Hilbert spaces. (Thanks to Ross Duncan for some of these!) I am relieved to see, finally, that this was noticed already back in 1975. The entry *quantum logic* now reflects this in the following paragraph:

Notice that the subobjects in a category of (finite dimensional) Hilbert spaces, and hence the propositions in the categorical logic of Hilbert spaces, are the (closed) linear subspaces. Therefore Birkhoff-vonNeumann quantum logic is indeed subsumed as a fragment of linear logic. This (obvious) fact was highlighted in (Crown 75) and then later with more of categorical logic in place and emphasizing dagger-structures in (Heunen 08, Heunen-Jacobs 09, Coecke-Heunen-Kissinger 13). Also (CCGP 09, section 9.3):

both orthologic (or weakenings thereof) and linear logic share the failure of lattice distributivity. In particular, the fragment of linear logic that includes just negation and the additive connectives is nothing but a version of the paraconsistent quantum logic PQL,

Before that I have added one more citation under BvN criticism, namely Abramsky talking about BvN as “quantum non-logic”.

]]>Thanks. I skimmed that Engesser at al. volume many times when I was considering one cowboy thesis in the BvN problematics but did not pay attention to that paper.

]]>Section 9.2 in

- Gianpiero Cattaneo, Maria Luisa Dalla Chiara, Roberto
Giuntini and Francesco Paoli, section 9 of
*Quantum Logic and Nonclassical Logics*, p. 127 in Kurt Engesser, Dov M. Gabbay, Daniel Lehmann (eds.)*Handbook of Quantum Logic and Quantum Structures: Quantum Logic*, 2009 North Holland {#CCGP09}

has an explicit and rather detailed discussion of how linear logic reduces to/subsumes BvN quantum logic. I have added a pointer at *quantum logic*.

added explicit pointers from the text to

- Vaughan Pratt,
*Linear logic for generalized quantum mechanics*, in Proc. of*Workshop on Physics and Computation (PhysComp’92)*(pdf, web)

which makes the statement “linear logic is the better BvN quantum logic” explicitly on his page 4 (and is years before the other citations to this extent that we had so far)

]]>I have tried to do some minimum of further editing at the “History”-section to reflect the above discussion. Please check critically, this can probably be said much better than what I jotted down for the moment.

]]>I must see how this relates to the Bayesian interpretation (see Wikipedia, while it lasts).

]]>I just noticed

- Michel Feldmann,
*Information-theoretic interpretation of quantum formalism*, arxiv/1312.7551

]]>We propose an information-theoretic interpretation of quantum formalism based on Bayesian probability and free from any additional axiom. Quantum information is construed as a technique of statistical estimation of the variables within an information manifold. We start from a classical register. The input data are converted into a Bayesian prior, conditioning the probability of the variables involved. In static systems, this framework leads to solving a linear programming problem which is next transcribed into a Hilbert space using the Gleason theorem. General systems are introduced in a second step by quantum channels. This provides an information-theoretic foundation to quantum information, including the rules of commutation of observables. We conclude that the theory, while dramatically expanding the scope of classical information, is not different from the information itself and is therefore a universal tool of reasoning.