The Decidable Quantum

Quantum logic replaces the Boolean lattice of classical propositions with the orthomodular lattice of subspaces of a Hilbert space. Modal logic adds operators for necessity and possibility. Quantum modal logic combines both — modalities over quantum propositions. Whether this system is decidable — whether an algorithm exists to determine if any given formula is a theorem — was open.

Tokuo proves it is, using Harrop’s lemma.

Harrop’s lemma is a result about intuitionistic logic: if a formula is not provable, there exists a finite Kripke model that refutes it. The key is finiteness — the countermodel has bounded size, so a systematic search through all models up to that size decides theoremhood. Tokuo adapts this strategy to quantum modal logic, showing that non-theorems have finite countermodels in the appropriate semantic framework.

The decidability means the logic is tame in a precise sense. Despite combining the non-distributive structure of quantum propositions with the intensional structure of modality, the resulting system doesn’t escape algorithmic reach. The finite model property holds: anything that fails to be a theorem fails finitely.

This is not obvious. Quantum logic alone is decidable (the orthomodular lattice has a finite model property). Modal logic alone is decidable (Kripke semantics provides finite countermodels). But combining decidable systems doesn’t guarantee a decidable product — the interaction between modality and quantum structure could have created undecidability. It didn’t. Harrop’s lemma reaches across the boundary.