Three Fixed-Dimension Satisfiability Semantics for Quantum Logic: Implications and an Explicit Separator

TL;DR

This paper compares three different semantics for propositional quantum logic over fixed finite-dimensional Hilbert spaces, revealing their relationships and differences through explicit examples and formal proofs.

Contribution

It introduces and compares three satisfiability notions for quantum propositional formulas, providing formal implications and an explicit formula distinguishing their satisfiability.

Findings

Standard semantics is the most permissive.

Explicit formula satisfiable in standard but not in other semantics.

Satisfiability classes form strict inclusions for dimensions ≥ 2.

Abstract

We compare three satisfiability notions for propositional formulas in the language {not, and, or} over a fixed finite-dimensional Hilbert space H=F^d with F in {R, C}. The first is the standard Hilbert-lattice semantics on the subspace lattice L(H), where meet and join are total operations. The second is a global commuting-projector semantics, where all atoms occurring in the formula are interpreted by a single pairwise-commuting projector family. The third is a local partial-Boolean semantics, where binary connectives are defined only on commeasurable pairs and definedness is checked nodewise along the parse tree. We prove, for every fixed d >= 1, Sat_COM^d(phi) implies Sat_PBA^d(phi) implies Sat_STD^d(phi) for every formula phi. We then exhibit the explicit formula SEP-1 := (p and (q or r)) and not((p and q) or (p and r)) which is satisfiable in the standard semantics for every d >= 2, but unsatisfiable under both the global commuting and the partial-Boolean semantics. Consequently, for every d >= 2, the satisfiability classes satisfy SAT_COM^d subseteq SAT_PBA^d subset SAT_STD^d and SAT_COM^d subset SAT_STD^d, while the exact relation between SAT_COM^d and SAT_PBA^d remains open. The point of the paper is semantic comparison, not a new feasibility reduction or a generic translation theorem.