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

Overview & Synopsis

We investigate an unsuspected connection between logical connectives with non-harmonious deduction rules, such as Prior's tonk, and quantum computing. We argue these 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 logical connective sup that has non-harmonious deduction rules and also with two interstitial rules, and show that the proof language of this logic forms the core of a quantum programming language.