Indexed on: 01 Mar '03Published on: 01 Mar '03Published in: International Journal of Theoretical Physics
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.