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 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 \, , \. We prove that there are infinitely many sub-Ex logics extending Holliday's fundamental logic.
Aguilera-Servin et al. (Wed,) studied this question.