Table of Contents
Fetching ...

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.

Constructive Quantum Logics

TL;DR

Problem: identify the jointly valid principles of quantum logic (orthologic) and constructivism (intuitionistic logic). Approach: introduce the axiom within fundamental logic, prove the Ex-Embedding Theorem, and establish the isomorphism 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 and a Heyting lattice via a fundamental embedding into ; (iii) a lattice isomorphism 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 and each superintuitionistic logic yields an axiomatization of from axiomatizations of and . 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.

Paper Structure

This paper contains 14 sections, 28 theorems, 57 equations, 2 figures.

Key Result

Theorem 1.1

The validities of Ex-logic are precisely the joint validities of orthologic and intuitionistic logic (in the signature $\{\vee,\wedge,\lnot\}$).

Figures (2)

  • Figure 1: Orthologic, intuitionistic logic, and their common principles.
  • Figure 2: The structure of constructive quantum logics.

Theorems & Definitions (52)

  • Theorem 1.1
  • Theorem 1.2
  • Corollary 1.3
  • Corollary 1.4
  • Definition 2.1
  • Definition 2.2
  • Proposition 2.3: Holliday Ho23
  • Definition 2.4
  • Definition 2.5
  • Remark 2.6
  • ...and 42 more