Constructive Quantum Logics
Juan P. Aguilera, Guillaume Massas
TL;DR
Problem: identify the jointly valid principles of quantum logic (orthologic) and constructivism (intuitionistic logic). Approach: introduce the axiom $Ex$ within fundamental logic, prove the Ex-Embedding Theorem, and establish the isomorphism $SE \cong SO \times SI$ between super-Ex logics and the product of quantum and superintuitionistic logics. Contributions: (i) Ex-logic exactly captures the intersection of orthologic and the implication-free fragment of intuitionistic logic; (ii) the Ex-Embedding Theorem provides a structural decomposition of any Ex-lattice into an ortholattice $O_L$ and a Heyting lattice $A_L$ via a fundamental embedding into $O_L \times A_L$; (iii) a lattice isomorphism $SE \cong SO \times SI$ characterizes all super-Ex logics; (iv) infinite families of sub-Ex and Sub-Ex logics and corollaries for orthomodular and De Morgan logics illuminate the landscape. Significance: this work clarifies the architecture of constructive quantum reasoning, offering a unified, algebraic framework with potential implications for quantum computation and the design of logics that merge quantum and constructive principles.
Abstract
Following a suggestion of Birkhoff and Von Neumann [Ann. Math. 37 (1936), 23-32], we pursue a joint study of quantum logic and intuitionistic logic. We exhibit a linear-time translation which for each quantum logic $Q$ and each superintuitionistic logic $I$ yields an axiomatization of $Q\cap I$ from axiomatizations of $Q$ and $I$. The translation is centered around a certain axiom (Ex) which (together with introduction and elimination rules for connectives) is shown to axiomatize the intersection of orthologic and intuitionistic logic, solving a problem of Holliday [Logics 1 (2023), pp. 36-79]. We prove that the lattice of all super-Ex logics is isomorphic to the product of the lattices of quantum logics and superintuitionistic logics in the signature $\{\land,\lor,\neg\}$. We prove that there are infinitely many sub-Ex logics extending Holliday's fundamental logic.
