The Decidable Quantum

Quantum logic replaces the distributive law of classical logic with a weaker orthomodular law, reflecting the structure of quantum mechanical propositions. Modal logic adds operators for necessity and possibility. Combining them gives quantum modal logic — a system for reasoning about what is necessarily or possibly true in quantum-mechanical settings. Whether an algorithm can determine theoremhood for any formula in this system was open.

This paper proves quantum modal logic is decidable, using Harrop's lemma — a result from constructive logic about derivability. The proof establishes that there exists an algorithm which, given any formula of quantum modal logic, determines in finite time whether it is a theorem of the system.

Decidability is not guaranteed: many extensions of basic logic are undecidable, and quantum logic's departure from classical distributivity makes it structurally different enough that classical decidability arguments don't transfer. The result says that quantum modal logic, despite its non-classical character, remains algorithmically tractable. You can mechanically check whether a quantum modal statement follows from the axioms. The non-classical weakening that accommodates quantum mechanics doesn't cost decidability.