ESSLLI'06 Course on Logics for Quantum Information Flow
By Alexandru Baltag and Sonja Smets
This course is addressed to students interested in the logic of quantum information, and in particular in the use of modal (dynamic and epistemic) logics to reason about information flow in quantum computation. It is an advanced course, based on classical work in quantum logic and quantum computation, as well as on our own work on Quantum Dynamic- Epistemic Logic.
Some prior familiarity with the most basic notions of multi-modal logic (PDL and epistemic logic), and with some basic algebraic notions (in Lattice Theory and Linear Algebra) would be very helpful; nevertheless, we will provide and briefly explain all the basic definitions, so the course is in principle self-contained. The course starts with an introduction to the basic concepts of Quantum Mechanics (in terms of Hilbert spaces, linear maps and tensor products), Quantum Computation (quantum-logic gates, quantum measurements, various quantum algorithms), then continues with a presentation of traditional Quantum Logic and of its algebraic and relational semantics; then we make the connection with dynamic modal logic, introducing Quantum Transition Systems as non-classical relational models for the (classical) language of PDL. We also give an equivalent algebraic semantics, in terms of Quantum Dynamic Algebras, and briefly present a Representation (and completeness) theorem for these structures. In the second part of the course, we introduce epistemic modalities, to express "knowledge" as localised information in a compound quantum system: any localised subsystem is taken as an "agent", whose "knowledge" is given by the information potentially available at that location. We use the resulting Quantum Dynamic- Epistemic Logic to characterise physical-computational properties, such as separation, entanglement, correlations between local measurements, various quantum-logical gates, Bell states etc. We present a proof system for this logic, which can capture important quantum-computational features. Finally, we use this logic to analyze and formally prove the correctness of some quantum programs, such as the famous Teleportation Protocol.