zbMATH — the first resource for mathematics

Between logic and quantic: a tract. (English) Zbl 1073.03036
Ehrhard, Thomas (ed.) et al., Linear logic in computer science. Based on the Azores summer school on linear logic and computer science, St. Miguel, Azores, Portugal, August 30–September 7, 2000. Cambridge: Cambridge University Press (ISBN 0-521-60857-0/pbk). London Mathematical Society Lecture Note Series 316, 346-381 (2004).
Traditional logic describes not only our reasoning, it also describes the behavior of real-life “yes”-“no” tests: if we have a test for a property \(P\) and a test for a property \(Q\), then we can have a test for, e.g., \(P\,\&\,Q\) – it is sufficient to test both and then apply the “and” operation. The possibility of such a composite test is based on the fact that in classical (non-quantum) physics, if we can perform tests \(P\) and \(Q\) separately, then we can also perform both at the same time, and the result of each of these two tests will be the same as when we perform them separately. In quantum physics, in general, performing a test changes the state; therefore, if we first perform a test \(P\), the result of a consequent application of \(Q\) may be different from what we would get if we first tested \(Q\).
Since the beginning of quantum physics, logicians have tried to capture how this feature of quantum physics can be reflected in logic. Quantum logic does capture this phenomenon, but at a serious price: e.g., in quantum logic, \(P\,\&\,Q\) is a new operation which no longer means that we test both \(P\) and \(Q\) – and whose relation to \(P\) and \(Q\) is rather mathematical. In short, we get a new logic, but its operations are no longer intuitive combinations of tests. Can we come up with a more intuitive version of quantum logic? The author proposes linear logic as a basis for such a description. This makes perfect sense: indeed, one of the main ideas behind linear logic is to distinguish between two different uses of “and”: “and” as in traditional logic and “and” as in limited resources logic, where “I can buy a coke and I can buy a cookie” does not imply that I can buy both. In quantum physics, we have a similar type of a limited resource: once we tested \(P\), we can no longer test whether \(Q\) holds in the original state (and vice versa). The author shows that this intuitive idea can indeed be extended to a more formal interpretation of several linear logic operations in terms of finite-dimensional quantum systems, and he describes some ideas of how this can be extended to the general (infinite-dimensional) quantum physics and to other linear logic operations like “definitely” (!).
For the entire collection see [Zbl 1051.03003].

03F52 Proof-theoretic aspects of linear logic and other substructural logics
81P10 Logical foundations of quantum mechanics; quantum logic (quantum-theoretic aspects)
03G12 Quantum logic