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.
More information: https://link.springer.com/chapter/10.1007%2F978-3-030-85315-0_11