Modal Deduction Systems for Quantum State Transformations

We introduce two modal natural deduction systems, MSQS and MSpQS, which are suitable to represent and reason about transformations of quantum states in an abstract, qualitative, way. Our systems provide a modal framework for reasoning about operations on quantum states (unitary transformations and measurements) in terms of possible worlds (as abstractions of quantum states) and accessibility relations between these worlds. We give a Kripke–style semantics that formally describes quantum state transformations, and prove the soundness and completeness of our systems with respect to this semantics.We also prove a normalization result for MSQS and MSpQS, showing that all derivations can be reduced to a normal form that satisfies a subformula property and yields a syntactic proof of the consistency of our deduction systems.