Not signed in (Sign In)

Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

  • Sign in using OpenID

Discussion Tag Cloud

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).

nLab > Latest Changes: quantum logic

Bottom of Page

1 to 50 of 50

  1.  
    • CommentRowNumber1.
    • CommentAuthorUrs
    • CommentTimeDec 23rd 2013

    have expanded the Idea-section at quantum logic to now read as follows:

    Broadly speaking, quantum logic is meant to be a kind of formal logic that is to traditional formal logic as quantum mechanics is to classical mechanics.

    The first proposal for such a formalization was (Birkhoff-vonNeumann 1936), which suggested that given a quantum mechanical system with a Hilbert space of states, the logical propositions about the system are to correspond to (the projections to) closed subspaces, with implication given by inclusion of such subspaces, hence that quantum logic is given by the lattice of closed linear subspaces of Hilbert spaces.

    This formalization is often understood as being the default meaning of “quantum logic”. But the proposal has later been much criticized, for its lack of key properties that one would demand of a formal logic. For instance in (Girard 11, page xii) it says:

    Among the magisterial mistakes of logic, one will first mention quantum logic, whose ridiculousness can only be ascribed to a feeling of superiority of the language – and ideas, even bad, as soon as they take a written form – over the physical world. Quantum logic is indeed a sort of punishment inflicted on nature, guilty of not yielding to the prejudices of logicians… just like Xerxes had the Hellespont – which had destroyed a boat bridge – whipped.

    and for more criticisms see (Girard 11, section 17).

    Therefore later other proposals as to what quantum logic should be have been made, and possibly by “quantum logic” in the general sense one should understand any formal framework which is supposed to be able to express the statements whose semantics is the totality of all what is verifiable by measurement in a quantum system.

    In particular it can be argued that flavors of linear logic and more generally linear type theory faithfully capture the essence of quantum mechanics (Abramsky-Duncan 05, Duncan 06, see (Baez-Stay 09) for an introductory exposition) due to its categorical semantics in symmetric monoidal categories such as those used in the desctiption of finite quantum mechanics in terms of dagger-compact categories. In particular the category of (finite dimensional) Hilbert spaces that essentially underlies the Birkhoff-vonNeumann quantum logic interprets linear logic.

    Another candidate for quantum logic has been argued to be the internal logic of Bohr toposes .

    In quantum computing the quantum analog of classical logic gates are called quantum logic gates.

    • CommentRowNumber2.
    • CommentAuthorzskoda
    • CommentTimeDec 24th 2013

    Though I like your discussion and criticism, it does not really belong to an idea section, rather a historical account. It is called an idea section but it is a conglomerate of buzz words (categorical semantics, form al logic, proposal, interprets), people names and historical facts, no single line of reasoning on quantum mechanics and logic. Where is the idea ?

    • CommentRowNumber3.
    • CommentAuthorUrs
    • CommentTimeDec 24th 2013
    • (edited Dec 24th 2013)

    the idea is that in the first line

    quantum logic is meant to be a kind of formal logic that is to traditional formal logic as quantum mechanics is to classical mechanics.

    and then in the paragraph after the criticism of Birkhoff-vonNeumann

    possibly by “quantum logic” in the general sense one should understand any formal framework which is supposed to be able to express the statements whose semantics is the totality of all what is verifiable by measurement in a quantum system.

    It seems to me in this particular entry one has to proceed with a critical historical discussion after this, due to the special state of the convention in the literature. Most authors will mean by “quantum logic” the Birkhoff-vonNeumann logic. That’s why people go around and say “quantum logic is bad”, they mean the Birkhoff-vonNeumann proposal, not the general idea of a logic that is to classical logic as quantum physics is to quantum. The entry has to say this. In its previous form the entry was misleading, a reader only knowing the previous version of the nLab entry and then Girard’s polemic would have been utterly confused.

    Therefore I feel the Idea section here must proceed roughly as it currently does

    1. the general intention in a few words

    2. the traditional notion of Birkhoff-vonNeumann

    3. indication of the shortcoming of this notion and the Idea that more general notions would also deserve to be called “quantum logic”.

    Therefore I think the general thrust of the current Idea-section is justified. But of course, as usual, there is plenty of room to improve it further.

    • CommentRowNumber4.
    • CommentAuthorUrs
    • CommentTimeDec 24th 2013

    I have edited the second paragraph at quantum logic slightly in order to make it clearer that this refers to the traditional default notion.

    • CommentRowNumber5.
    • CommentAuthorTobyBartels
    • CommentTimeDec 24th 2013

    Perhaps make the first paragraph of the current #Idea section the whole of the #Idea section and make the rest a #History section?

    • CommentRowNumber6.
    • CommentAuthorUrs
    • CommentTimeDec 25th 2013
    • (edited Dec 25th 2013)

    I won’t insist, but just to make the point clear that I think needs to be taken care of, let me re-iterate:

    The common understanding of “quantum logic” does not agree with the first paragraph of the current #Idea section!

    Commonly “quantum logic” is understood as “Birkhoff-vonNeumann quantum logic”. That’s why Girard and others say “quantum logic sucks, linear logic is the right thing to describe logic in the quantum context”. The nnLab (and Abramsky-Duncan) now say: well, if that’s the case then we should just change convention and say “quantum logic” for “linear logic” and not for “Birkhoff-von Neuman logic”.

    But this is not the widely understood idea (not yet, at least). Therefore if the nnLab just says “quantum logic is the logic of quantum physics, for instance linear logic” then readers who just see this will be confused to see Girard and others say “quantum logic sucks, linear logic is better”.

    I think that the idea section needs to sort out this issue of traditional terminology against reasonable terminology.

    • CommentRowNumber7.
    • CommentAuthorTobyBartels
    • CommentTimeDec 25th 2013

    The common understanding of “quantum logic” does not agree with the first paragraph of the current #Idea section!

    Right, but I don't think that we need that to infect our #Idea section.

    At best, add to that section a brief note that the term is often used in a very restricted sense, but leave the fuller discussion for the #History section.

    (Or so I suggest; I have made no changes yet.)

    • CommentRowNumber8.
    • CommentAuthorUrs
    • CommentTimeDec 25th 2013

    Okay, I won’t insist. But I won’t make the change myself ;-)

    Maybe to steer this discussion into a more constructive direction:

    if we follow the sentiment that the “right” quantum logic is a flavor (“fragment”, if you wish) of linear logic, then the next question is: which flavor?

    I think it is clear that the flavor that Abramsky and Duncan consider (as cited at quantum logic) should certainly be included, but is just as certainly not general enough.

    Possibly “quantum homotopy type theory” is easier to capture than “quantum logic”. A good candidate here seems to be that whose semantics is given by parameterized stable homotopy types with tensor product. But maybe one wants to add some other condition, too. Not sure yet.

    • CommentRowNumber9.
    • CommentAuthorspitters
    • CommentTimeDec 25th 2013

    This sounds interesting. Could you say a bit more how that relates to the C*-algebra picture?

    Also, I happened to notice that anyonic quantum computation builds on Witten-Chern-Simons theory. The latter can be formulated in cohesive HoTT, how about the former?

    • CommentRowNumber10.
    • CommentAuthorzskoda
    • CommentTimeDec 25th 2013
    • (edited Dec 25th 2013)

    then we should just change convention and say “quantum logic” for “linear logic”

    Hilbert space is not what we can measure, the measured propositions are not there; Birkhoff-von Neumann has not have this problem – it was only about propositions of measured. The problem with BvN s that their logic does not have IMPLICATION; rule of inference. There are some frameworks which put this inside, I had once come across a variant of BvN which axiomatizes the logic with 3 different rules of inference and complicated relations among them. Now the idea section should have some reasoning why would linear logic qualify. Saying monoidal category of Hilbert space like entities and alike is not an argument as this is not what is measured. I would like to see the idea directly from what we know about quantum mechanics, what we measure, not a wish list, we like linear logic, there are examples related to Hilbert spaces, and let’s say by intimidation of an impressive framework. Linear logic is linear logic. It becomes a quantum logic only if it is derived from rethinking the quantum measurement. Idea section does not have a single line on this derivation.

    I agree that idea section should say that the conventional terminology is BvN and that there are works on foundation of QM which try to find a more satisfactory replacement and candidates could be brefly listed wth some idea why those. The rest and especially vague rambling by Girard (which does not reason about quantum mechanics directly) should be in my opinion in separate historical section.

    • CommentRowNumber11.
    • CommentAuthorUrs
    • CommentTimeDec 25th 2013

    Zoran, I am not sure what you are after in your first paragraph. Everything structurally that can be said about quantum mechanics follows from the structure of certain monoidal categories and linear logic expresses precisely this. This is a technical fact, whereas philosophical sentiments about measurement are hard to capture by anything.

    Yes, the quote by Girard does not contain arguments, just the polemic. His arguments are in his section 17, I had added a pointer. Another list of defects of BvN has been given by Heunen-Landsman-Spitters, I have now added the following to the entry:

    For instance in (Heunen-Landsman-Spitters 07, p. 4) it says the following.

    Attractive and revolutionary as this spatial quantum “logic” may appear it faces severe problems. The main logical drawbacks are:

    • Due to its lack of distributivity, quantum ‘logic’ is difficult to interpret as a logical structure. • In particular, despite various proposals no satisfactory implication operator has been found (so that there is no deductive system in quantum logic). • Quantum ‘logic’ is a propositional language; no satisfactory generalization to predicate logic has been found.

    Quantum logic is also problematic from a physical perspective. Since (by various theorems and wide agreement) quantum probabilities do not admit an ignorance interpretation, [0,1][0, 1]-valued truth values attributed to propositions by pure states via the Born rule cannot be regarded as sharp (i.e. {0, 1}-valued) truth values muddled by human ignorance. This implies that, if X=[a∈Δ]X = [a \in \Delta] represents a quantum-mechanical proposition, it is wrong to say that either xx or its negation holds, but we just do not know which of these alternatives applies. However, in quantum logic one has the law of the excluded middle in the form x∨x ⊥=1x \vee x^\perp = 1 for all xx. Thus the formalism of quantum logic does not match the probabilistic structure of quantum theory responsible for its empirical content.

    • CommentRowNumber12.
    • CommentAuthorUrs
    • CommentTimeDec 25th 2013
    • (edited Dec 25th 2013)

    Bas,

    concerning the first question, how linear logic relates to the logic of Bohr toposes, I think of it this way. By homotopy linear logic we obtain quantization linear over the KUKU-spectrum, as described in Joost Nuiten’s thesis. It so happens that parts of KUModKU Mod are modeled by KK-theory (in that there is a functor KK⟶KUModKK \longrightarrow KU Mod with some good properties) and this is how C *C^\ast-algebra technology serves to present KUKU-linear logic.

    concerning the second question, if we have topological quantum computing in cohesive HoTT: once you complete the quantization step in HoTT you are to end up with a local TQFT given as a cobordism representation. For Chern-Simons that will contain all the structure used in CS topological computing.

    But notice that we haven’t quite completed the quantization of CS in HoTT. What we have is the local pre-quantum theory and some indications of how the quantization should work in some higher analog of the KUKU-linear theory.

    • CommentRowNumber13.
    • CommentAuthorzskoda
    • CommentTimeDec 26th 2013

    Everything structurally that can be said about quantum mechanics follows from the structure of certain monoidal categories and linear logic expresses precisely this.

    I do not see this, nor understand at all. Given a concrete physical system there is an agreement what can and what can not be measured, and if do this measurement what can be measured after that and not. Not every fact about abstract Hilbert space is however physical.

    This is a technical fact, whereas philosophical sentiments about measurement are hard to capture by anything.

    It s not about philosophical interpretation. Proposition are about events in nature, quantum logic about events in quantum physical world, not about nonphysical events in abstract Hilbert space.

    Quantum ‘logic’ is a propositional language; no satisfactory generalization to predicate logic has been found.

    I was talking about it: no implication in the “logic”. There are however some complicated systems with simultaneous 3 types of implications in the literature which extend BvN logic. I do not like it, but the claim above is not entirely true due this fact.

    What we have is the local pre-quantum theory and some indications of how the quantization should work in some higher analog of the KU-linear theory.

    Thanks for sharing cohesive point of view t si exciting. But it does not give itself the answer to my question, what is the idea which goes from quantum physics to linear logic. All this is about some hi level point of view on quantizaton which should include very complicated theories. But everybody knows how to quantize the few simplest physical systems and also knows analysis of simples thought experiments like two slit experiment, Aharonov-Bohm effect and so on. How to get linear logic whose interpretation will be exactly the physical statements about such systems ? This is the only real question, everything else is avoiding the substance.

    Quantum logic should not be about a particular formalism of quantum mechanics but logic of physical statements which come out of any of the formalisms. Does not matter if we use path integral approach or Heisenberg picture or anything else.

    • CommentRowNumber14.
    • CommentAuthorzskoda
    • CommentTimeDec 26th 2013
    • (edited Dec 26th 2013)

    Take a simple harmonic oscillator. How do you get the linear logic for this system and how do you interpret the statements of that linear logic as physical statements about the world of observing physics of the harmonic oscillator ?

    • CommentRowNumber15.
    • CommentAuthorzskoda
    • CommentTimeDec 26th 2013
    • (edited Dec 26th 2013)

    You see, if I read intro to any book which supports BvN logic I can then come to a knowledgeable theoretical physicist and explain too him why this is quantum logic and also why I do not like it. The idea section should give me he same ability for a flavour of linear logic eventually; I do not mind requiring more category theory, I mind if I do not get/understand the argument myself.

    • CommentRowNumber16.
    • CommentAuthorUrs
    • CommentTimeDec 27th 2013
    • (edited Dec 27th 2013)

    Hey Zoran,

    a Hamiltonian HH via its propagotors exp(iℏtH)\exp(\frac{i}{\hbar} t H) is an equivalence V⟶≃VV \stackrel{\simeq}{\longrightarrow} V of the given Hilbert space VV and appears as this function in the linear logic which is the internal language of the given category of Hilbert spaces.

    You see, this is a tautological statement: quantum mechanics is expressed in terms of constructions in certain tensor categories, and linear logic is just the internal logic of these categories, just another perspective of speaking about these categories.

    You know how Abramsky and Cooke have been emphasizing no end how a vast chunk of quantum physics is formally encoded just in properties of tensor categories, as reviewed at finite quantum mechanics in terms of dagger-compact categories. The proposal that the corresponding fragment of linear logic is hence a good notion of “quantum logic” in

    is therefore essentially a tautology: by computational trinitarianism it is just a change of perspective, different but equivalent.

    But if you are unhappy with this remark, maybe rather than trying to make me write the Idea-section that you’d like to see, better to go ahead yourself and write some paragraphs yourself. Then we can talk about that.

    Finally, here is one observation and/or question which I am wondering about: doesn’t the perspective of linear logic as quantum logic fully subsume the BvN picture? Because the internal linear logic of the category of Hilbert spaces involves as subobject lattices just those lattices of subspaces of Hilbert spaces.

    • CommentRowNumber17.
    • CommentAuthorzskoda
    • CommentTimeDec 27th 2013
    • (edited Dec 27th 2013)

    OK, so now it is clear, I did not even suspect this basic thing which I now understood (from your last post). Their quantum logic does not even try to talk about physical statements, it talks about abstract Hilbert spaces regardless what can be measured, and not about propositions of the real quantum world. Thanks. (You see the problem is buzzplay of WORDS like quantum logic and not saying the objective clearly, without recourse to vague analogies and weak connections).

    It can not subsume BvN as BvN statements are only about the measured ones and not a MODEL of laws followed. One thing is to model physics and another is to talk (logic talks about real events in the world and all the fuss about BvN is to be careful on what is real in quantum world). It is like saying that classical logic subsumes intuitionistic. In classical logic you can talk and infer things which you can not in intuitionistic. Intuitionstic restricts what you can do. Similarly propositions about measurement restrict what you can say, while the abstract models of Hilbert space etc. do not have this restriction. Hilbert space is external from the point of view of measurement, it is only a metalanguage, and quantum logic is supposed to be internal, something what a living being in quantum world can say about its surrounding. In some sense external world of course can express laws which internal beings living n a model can observe. But the question what internally can be said is legitimate, important, even fundamental. We live internally in a quantum world, what are the true statements in our world ?? I can not imagine a more important statement. Law of quantum evolution in Hilbert space is just a law which models the world, and has extra data which are non-physical, sort of hidden variables.

    My impression (is it right ??) is that linear logic gives external language. It is internal to some abstract mathematical model but from the point of view of clear distinction of observer point of view it seems to me external. If I understood your words. (“it is just a change of perspective, different but equivalent.” – I conclude – to external model of quantum mechanics via Hilbert space and abstract evolution – hence inappropriate to the internal observer).

    Even if we do not trust in Copenhagen interpretation and find it incomplete, it is well known model. The flexible theory should be able to give eventually answer what is the predicate logic behind the Copenhagen interpretation of QM. And, in particularly, the space of propositional phrases in the logic of simplest quantum systems like harmonic oscillator, two slit experiment system and alike.

    • CommentRowNumber18.
    • CommentAuthorzskoda
    • CommentTimeDec 27th 2013

    In other words, if understood (maybe I did not), BvN and linear logic are not different proposals for the search for quantum logic, they are proposals to solutions of entirely different problems. Only the word seems to be in common.

    • CommentRowNumber19.
    • CommentAuthorzskoda
    • CommentTimeDec 27th 2013
    • (edited Dec 27th 2013)

    This being said, I like Duncan’s thesis at first sight. We just need down to Earth distinctions in nLab entry on quantum logic. This nice references missing at entanglement which is its basic topic.

    • CommentRowNumber20.
    • CommentAuthorUrs
    • CommentTimeDec 27th 2013

    Zoran I don’t follow the complaint about “buzzwords”. In an entry on a topic in formal logic, the words “formal logic” and “categorical semantics” are hardly “buzzwords”.

    Let’s stick to the technical content for a moment. Consider the categorical semantics of Abramsky-Duncan linear logic given by the category of finite dimensional Hilbert spaces. Given one such, the propositions about it correspond to its subobjects. These are its linear subspaces. They are automatically closed, due to finite dimensionality. Agreed? So that’s BvN, isn’t it.

    • CommentRowNumber21.
    • CommentAuthorzskoda
    • CommentTimeDec 27th 2013

    Agreed? So that’s BvN, isn’t it.

    Sounds OK

    • CommentRowNumber22.
    • CommentAuthorzskoda
    • CommentTimeDec 28th 2013

    External can always describe internal, in the language of 19; opposite is usually impossible. My understanding was that it seemed to me that there are also external propositions which are not about closed subspaces, what would be illegitimate. Like you say that linear logic is equivalent to the usual QM at external point of view. But from BvN, even reconstruction of the Hilbert space from the whole theory (not only from the concrete internal data, but from all possible configurations of BvN) is rather complicated theorem and its possibility really depends on ground field. Even then, from the internal point of view one can not describe the evolution in the Hilbert space.

    But let us see other way around. BvN does not have implications. If the propositions are about the same objects as in the linear logic (in the case of finte dimensional Hilbert space) as you say, then we could easily transfer the implication rules to the BvN. This would solve a long standing problem.

    • CommentRowNumber23.
    • CommentAuthorTobyBartels
    • CommentTimeDec 28th 2013
    • (edited Dec 28th 2013)

    The last paragraph quoted from Heunen–Landsman–Spitters in #11 seems philosophically confused to me.

    When they say that there is no ignorance interpretation of quantum probabilities, [edit: crucial missing word coming up] IF they mean that quantum indeterminacy cannot be reduced to classical indeterminacy (where, as a good Bayesian, I endorse the ignorance interpretation of classical probability), then this is correct; but how can it follow from this that excluded middle must fail in a quantum logic? Yes, excluded middle is true in classical probability; but just because quantum probability is not classical probability, that doesn't mean that a particular logical law that holds in one cannot also hold in the other! So when I want to decide whether excluded middle holds in quantum logic as in classical probability theory, I have to consider the question directly to decide. (And when I do that, I imagine an observable proposition, consider what it means to take its negation and what it means to take the disjunction of these, find myself thinking very much like BvN whether I intend to or not, and conclude that excluded middle holds!)

    Of course, excluded middle also holds in linear logic, in the form 1⊢p⅋p ⊥1 \vdash p \parr p^\perp (but p⅋p ⊥⊢1p \parr p^\perp \vdash 1 fails; it's ⊤\top that's entailed in any context).

    • CommentRowNumber24.
    • CommentAuthorTobyBartels
    • CommentTimeDec 28th 2013

    To understand quantum probability, we must understand classical probability. People (including such physicists as Richard Cox and Edwin Jaynes) have done well by thinking of probability as a generalization of boolean logic, but does it have a good notion of implication?

    • CommentRowNumber25.
    • CommentAuthorUrs
    • CommentTimeDec 28th 2013

    Toby, re #23. Yes, I agree, we should edit the entry further to discuss this. This maybe connects also to what Zoran was saying re measurement: the projections in BvN are measurement outcomes, after all, and for them it does make sense to say it’s either this way or that way.

    Also, I agree with your “find myself thinking very much like BvN whether I intend to or not,” I came to that at the end of #16: despite the way the discussion started, it seems that linear logic is more a strenghtening/refinement of BvN than a rejection of it.

    It seems strange that this hasn’t been discussed much. I don’t see lots of followups of Abramsky-Duncan. Not that any of this is a big deal technically, but it would be nice to have these concepts sorted out neatly.

    • CommentRowNumber26.
    • CommentAuthorzskoda
    • CommentTimeDec 29th 2013

    It seems we are converging somewhere :)

    • CommentRowNumber27.
    • CommentAuthorzskoda
    • CommentTimeJan 3rd 2014

    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.

    • CommentRowNumber28.
    • CommentAuthorTobyBartels
    • CommentTimeJan 3rd 2014

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

    • CommentRowNumber29.
    • CommentAuthorUrs
    • CommentTimeJan 7th 2014

    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.

    • CommentRowNumber30.
    • CommentAuthorUrs
    • CommentTimeJan 7th 2014
    • (edited Jan 7th 2014)

    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)

    • CommentRowNumber31.
    • CommentAuthorUrs
    • CommentTimeJan 7th 2014

    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.

    • CommentRowNumber32.
    • CommentAuthorzskoda
    • CommentTimeJan 8th 2014

    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.

    • CommentRowNumber33.
    • CommentAuthorUrs
    • CommentTimeJan 8th 2014
    • (edited Jan 8th 2014)

    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”.

    • CommentRowNumber34.
    • CommentAuthorUrs
    • CommentTimeJan 17th 2014
    • (edited Jan 17th 2014)

    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.

    • CommentRowNumber35.
    • CommentAuthorUrs
    • CommentTimeJan 17th 2014
    • (edited Jan 17th 2014)

    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).

    • CommentRowNumber36.
    • CommentAuthorJames Francese
    • CommentTimeMar 14th 2019

    link to effect algebras

    diff, v36, current

    • CommentRowNumber37.
    • CommentAuthorUrs
    • CommentTimeMay 12th 2021

    added publication data for

    diff, v40, current

    • CommentRowNumber38.
    • CommentAuthorUrs
    • CommentTimeMay 12th 2021

    and added DOI to:

    diff, v40, current

    • CommentRowNumber39.
    • CommentAuthorUrs
    • CommentTimeMay 12th 2021

    added pointer to:

    diff, v40, current

    • CommentRowNumber40.
    • CommentAuthorTodd_Trimble
    • CommentTimeApr 4th 2023

    Changed “linear space” to “linear span”.

    diff, v49, current

    • CommentRowNumber41.
    • CommentAuthorUrs
    • CommentTimeApr 4th 2023
    • (edited Apr 4th 2023)

    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 FinDimVectFinDimVect.

    diff, v51, current

    • CommentRowNumber42.
    • CommentAuthorUrs
    • CommentTimeApr 4th 2023

    added publication data to this item:

    diff, v51, current

    • CommentRowNumber43.
    • CommentAuthorUrs
    • CommentTimeApr 6th 2023

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

    diff, v53, current

    • CommentRowNumber44.
    • CommentAuthorUrs
    • CommentTimeApr 8th 2023
    • (edited Apr 8th 2023)

    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:

    diff, v56, current

    • CommentRowNumber45.
    • CommentAuthorUrs
    • CommentTimeApr 8th 2023

    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

    diff, v56, current

    • CommentRowNumber46.
    • CommentAuthorUrs
    • CommentTimeMay 23rd 2023

    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

    ?

    diff, v60, current

    • CommentRowNumber47.
    • CommentAuthorUrs
    • CommentTimeJun 1st 2023

    added pointer to:

    diff, v61, current

    • CommentRowNumber48.
    • CommentAuthorUrs
    • CommentTimeJul 16th 2023

    added pointer to:

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

    diff, v63, current

    • CommentRowNumber49.
    • CommentAuthorUrs
    • CommentTimeJul 26th 2023

    added pointer to today’s

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

    diff, v64, current

    • CommentRowNumber50.
    • CommentAuthorUrs
    • CommentTimeOct 28th 2023

    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”

    diff, v68, current

1 to 50 of 50

  1.