This project introduces students to logics for reasoning about quantum theory, quantum information, and quantum computation. Work on quantum logic started with Birkoff and von Neumann as a tool for studying relationships among physical observables. The language of this logic is the same as for propositional logic, but the semantics is different. Later developments focused not just on the observables, but also the dynamics of a quantum system: for example what happens to a quantum system when certain actions are made, such as a measurement. Early development of quantum logic avoided the use of probability, though probability has been receiving an increasing amount of attention in quantum logics. We will explore some recently proposed probabilistic extensions of those logics. Quantum systems can be combined. Some states in the composed system can be separated into a composition of states from the subsystems, while others may be entangled. We will study how to reason about these concepts using logic, and explore certain protocols that make use of such compositionality, such as the quantum teleportation protocol or a quantum key distribution protocol.
