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

翻译：我们研究了具有非和谐演绎规则的逻辑联结词（如Prior的tonk）与量子计算之间未曾预料到的联系。我们认为这些联结词对信息擦除、不可逆性以及非确定性进行了建模，而这些特性在量子测量等领域中均有所体现。我们引入了一种直觉主义命题逻辑，其中包含一个非和谐的联结词sup和两条居间规则，并证明该逻辑的证明语言构成了量子编程语言的核心。