Duality Theory and Categorical Universal Logic: With Emphasis on Quantum Structures

TL;DR

This paper develops a categorical framework for quantum logics using hyperdoctrines and duality theory, unifying classical, intuitionistic, and quantum logics with sound and complete semantics.

Contribution

It introduces hyperdoctrine-based dual adjunctions for quantum logic, connecting set-theoretical models with categorical quantum mechanics within a unified universal logic framework.

Findings

Hyperdoctrines for quantum logic have universal and existential quantifiers.

Set-theoretical hyperdoctrines provide sound and complete semantics for quantum sequent calculus.

Categorical quantum mechanics can be reconciled with traditional quantum logic through this framework.

Abstract

Categorical Universal Logic is a theory of monad-relativised hyperdoctrines (or fibred universal algebras), which in particular encompasses categorical forms of both first-order and higher-order quantum logics as well as classical, intuitionistic, and diverse substructural logics. Here we show there are those dual adjunctions that have inherent hyperdoctrine structures in their predicate functor parts. We systematically investigate into the categorical logics of dual adjunctions by utilising Johnstone-Dimov-Tholen's duality-theoretic framework. Our set-theoretical duality-based hyperdoctrines for quantum logic have both universal and existential quantifiers (and higher-order structures), giving rise to a universe of Takeuti-Ozawa's quantum sets via the tripos-to-topos construction by Hyland-Johnstone-Pitts. The set-theoretical hyperdoctrinal models of quantum logic, as well as all quantum hyperdoctrines with cartesian base categories, turn out to give sound and complete semantics for Faggian-Sambin's first-order quantum sequent calculus over cartesian type theory; in addition, quantum hyperdoctrines with monoidal base categories are sound and complete for the calculus over linear type theory. We finally consider how to reconcile Birkhoff-von Neumann's quantum logic and Abramsky-Coecke's categorical quantum mechanics (which is modernised quantum logic as an antithesis to the traditional one) via categorical universal logic.