A New Connective in Natural Deduction, and its Application to Quantum Computing

We investigate an unsuspected connection between non-harmonious logical connectives, such as Prior's tonk, and quantum computing. We argue that non-harmonious connectives model the information erasure, the non-reversibility, and the non-determinism that occur, among other places, in quantum measurement. We introduce a propositional logic with a non-harmonious connective sup and show that its proof language forms the core of a quantum programming language.