This article is intended as an introduction to the subject of quantum logic, and as a brief survey of the relevant literature. Also discussed here are logics for specification and analysis of quantum information systems, in particular, recent work by P. Mateus and A. Sernadas, and also by R. van der Meyden and M. Patra. Overall, our objective is to provide a high-level presentation of the logical aspects of quantum theory. Mateus’ and Sernadas’ EQPL logic is illustrated with a small example, namely the state of an entangled pair of qubits. The "KT" logic of van der Meyden and Patra is demonstrated briey in the context of the B92 protocol for quantum key distribution.
This article is intended as an introduction to the subject of quantum logic, and as a brief survey of the relevant literature. Also discussed here are logics for specification and analysis of quantum information systems, in particular, recent work by P. Mateus and A. Sernadas, and also by R. van der Meyden and M. Patra. Overall, our objective is to provide a high-level presentation of the logical aspects of quantum theory. Mateus’ and Sernadas’ EQPL logic is illustrated with a small example, namely the state of an entangled pair of qubits. The "KT" logic of van der Meyden and Patra is demonstrated briey in the context of the B92 protocol for quantum key distribution.
This article is intended as an introduction to the subject of quantum logic, and as a brief survey of the relevant literature. Also discussed here are logics for specification and analysis of quantum information systems, in particular, recent work by P. Mateus and A. Sernadas, and also by R. van der Meyden and M. Patra. Overall, our objective is to provide a high-level presentation of the logical aspects of quantum theory. Mateus' and Sernadas' EQPL logic is illustrated with a small example, namely the state of an entangled pair of qubits. The "KT" logic of van der Meyden and Patra is demonstrated briefly in the context of the B92 protocol for quantum key distribution.
This paper provides an overview of quantum dynamic logics, showing how they have been designed and illustrating how these logics can be applied to verify the correctness of quantum protocols. Similar to the advantages of using dynamic logics to reason about the flow of classical information, the quantum analogues of these logics are tailored to the task of reasoning about the flow of quantum information. We present our logical systems in a modular way, starting with the qualitative logic of quantum measurements and unitary evolutions in single quantum systems, which can already express non-classical effects, e.g., the state-changing interference induced by quantum tests, their non-commutativity, etc. We then move on to logics for compound quantum systems that can capture the non-local features of quantum information: separability, entanglement, correlated measurements, Bell states, etc. We then briefly summarize the logic of quantum probabilities and sketch some applications to quantum protocols.
The non-classical nature of quantum theory has led to a number of efforts to formalize the logic of statements whose universe of discourse is the subatomic (see, for example, [3], [6], [8], and [10]).It might be hoped that ideally the fruit of such efforts would be a formalism not totally divorced from the classical logic, but incorporating or incorporated in it in such a manner as to unify the logic of the micro-and the macro-worlds.Indeed, this has been the general direction taken by these efforts, including that which we principally examine and expand upon here.*Josef Jauch, [6], pp.67-89, developed a "propositional calculus of quantum mechanics".He objected to calling a system like his a "logic of quantum mechanics"; however, our use of 'logic' here is not, I think, the use to which Jauch objected.A logic, for our present purposes, is a mathematical formalism having a reasonable interpretation as a theory of deduction; its actual application as normative of argumentation in reality is a matter of empirical judgment.This seems close to the way Jauch wished to use "propositional calculus" but more general, allowing for extension to a quantification theory of quantum mechanics, for example.Although Jauch's presentation of a propositional calculus of quantum mechanics is mathematically interesting and suggestive, there are a number of problems connected with it.It is our purpose to engage some of these problems and to present a rigorously defined formalism intended to come close to doing the job intended by Jauch for his logic.The success or lack of success of this effort as related to actual application of this formalism in the foundations of quantum theory is, I think, a matter for the physicists to decide; the empirical judgment involved in this application is not in the scope of this paper.If a formalism is to have a reasonable interpretation as a theory of deduction, it seems clear that it must include a relation which, when it holds between two elements of the formalism, may be reasonably interpreted as expressing that one of the elements 'follows from' the other, in •The author wishes to thank Robert Piziak for advice and comments in the course of research for this paper.
This paper applies to quantum systems a modelling for the logic of knowledge, originally developed for reasoning about distributed systems, but since then applied to game theory, computer security and artificial intelligence. A formal model of quantum message passing systems is developed and the question of how one might define the semantics of a modal operator for knowledge in this model is considered. It is argued that there are at least two plausible semantics, depending on whether the agents are permitted to make use of their quantum state in determining what they know, and on whether one is dealing with single instances of quantum systems, or ensembles. The framework is illustrated using a number of examples from the quantum computing literature, including protocols for quantum key distribution and teleportation. 1
Quantum information is an emerging field which has attracted a lot of attention in the last fifteen years or so. It is a broad subject which covers from the most applied questions (e.g., how to build quantum computers or secure cryptographic systems), to the most theoretical problems concerning the formalism of quantum mechanics, its complexity, and its potential to go beyond classical physics. I have written these notes as an introduction to the formalism of quantum information, trying to show how it is a natural progression from an undergraduate course on quantum mechanics (just as I felt it was for me). Hence, these are mainly notes about the language of quantum information and the meaning of its terms, not about its applications. They do not intend to be an exhaustive review about the field, but just a logical sequence of ideas, concepts and definitions, building up towards the continuous variables formalism, which actually takes over most of the notes. In this way, most of the results are stated without proof, and I haven't been careful with references; this is a work in progress, and I intend to add such things in the future. In any case, most of the topics that I introduce have been thoroughly covered in previous books and reviews, and with this notes I only intend to give my point of view, as well as to introduce the different topics and objects in exactly the way I work with and think about them, hoping it will be useful, especially for the people who are starting in the field. These notes originated in 2010 as a way of studying for my close collaboration with Raúl García-Patrón and Nicolas J. Cerf, to whom I am deeply grateful for guidance and incredibly clarifying discussions. They benefited greatly as well from the weeks I spent in Doha with Hyunchul Nha and his group in 2012, especially from discussions with him and Ho-Joon Kim.