Foundation for Quantum Computing

In this paper we introduce a minimal formal intuitionistic propositional Gentzen sequent calculus for handling quantum types, quantum storage being introduced syntactically along the lines of Girard's of course operator !. The intuitionistic fragment of orthologic is found to be translatable into this calculus by means of a quantum version of the Heyting paradigm. When realized in the category of finite dimensional Hilbert spaces, the familiar qubit arises spontaneously as the irreducible storage capable quantum computational unit, and the necessary involvement of quantum entanglement in the quantum duplication process is plainly and explicitly visible. Quantum computation is modelled by a single extra axiom, and reproduces the standard notion when interpreted in a larger category.