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.
natural deduction quantum computing modal logics labelled deduction proof theory