Constructive quantum logics

Following a suggestion of Birkhoff & von Neumann [Ann. Math. 1936;37: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∩I from axiomatizations of Q and I. The translation is centred 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 2023;1: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. We prove that there are infinitely many sub-Ex logics extending Holliday’s fundamental logic.