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

TL;DR

This paper introduces a new logical connective in natural deduction that models quantum phenomena like non-reversibility and non-determinism, bridging logic and quantum computing through a novel propositional logic.

Contribution

It presents a new non-harmonious logical connective and demonstrates its application as the core of a quantum programming language, linking logic with quantum computational concepts.

Findings

The new connective models quantum measurement effects.

The proof language forms the basis of a quantum programming language.

The logic captures non-reversible and non-deterministic aspects of quantum processes.

Abstract

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.