Quantum Modal Logic

Origin. Various approaches combining modal logic and quantum mechanics (2000s-present). Baltag, Smets, Dishkant, Goldblatt. Modal interpretation of quantum observables. Reasoning about quantum measurements and information. Foundation for quantum epistemics.

Models. Modal logic for quantum states. Classical modal: Kripke frames with accessibility. Quantum modal: Hilbert spaces with subspace structure. □φ: necessarily φ (eigenstate of observable). Dynamic: measurement updates knowledge.

Formalism.

Static quantum modal logic: Propositions = closed subspaces of Hilbert space H. a ⊨ P iff state a ∈ P (subspace).

Modal operator via observable A: □_A φ: "measuring A would definitely give result compatible with φ" State in eigenspace of A corresponding to values in ⟦φ⟧.

Dynamic quantum modal logic: [M]φ: after measurement M, φ holds. Measurement updates state (projection).

Semantics: ⟦p⟧ = closed subspace (quantum proposition) ⟦□φ⟧ = {ψ : ψ in eigenspace implies ψ ∈ ⟦φ⟧} ⟦[M]φ⟧ = {ψ : Proj_M(ψ) ∈ ⟦φ⟧}

Quantum epistemic logic: Agent's knowledge = compatible states. Kφ: agent knows φ (all compatible states satisfy φ). Measurement reveals information.

Orthomodular modal logic: □ is a right adjoint, so □(φ ∧ ψ) = □φ ∧ □ψ still holds — meets are preserved. What fails is in the propositional base, not the modality: φ ∧ (ψ ∨ χ) ≠ (φ ∧ ψ) ∨ (φ ∧ χ), since ∨ is closed span, not union. Reflects quantum superposition: a superposition lies in the span of two subspaces without lying in either.

Symbols.

Symbol	Unicode	Name	Meaning
□	U+25A1	Necessity	Observable certainty
◇	U+25C7	Possibility	Compatible
[M]	—	Measurement	After measuring M
⟦φ⟧	—	Interpretation	Subspace
K	—	Knows	Epistemic
⊥	U+22A5	Up tack / Orthogonal	Perpendicular; orthocomplement of a subspace
Proj	—	Projection	Measurement
∧	U+2227	Logical and / Meet	Intersection of subspaces
∨	U+2228	Logical or / Join	Closed span of subspaces
⊨	U+22A8	Double turnstile / Satisfaction	a ⊨ P when the state lies in the subspace
∈	U+2208	Element of	Membership in a subspace
≠	U+2260	Not equal	Failure of distribution
φ, ψ, χ	U+03C6, U+03C8, U+03C7	Phi, psi, chi	Formula variables
H	—	Hilbert space	Carrier of the propositional lattice
a?	—	Quantum test	Dynamic action whose modality is the Sasaki hook
→_S	—	Sasaki hook	a⊥ ∨ (a ∧ b); equals [a?]b
φ_a	—	Sasaki projection	State update after a yes-outcome on a
∘	U+2218	Ring operator / Composition	Composing tests, which does not collapse
KTB	—	System B	Reflexive symmetric normal modal logic; host of Goldblatt's translation

Metatheory. Goldblatt (1974) proved that orthologic is faithfully embeddable in the modal system KTB: an orthoframe is a set with an irreflexive symmetric orthogonality relation, whose complement is reflexive and symmetric, which is exactly the frame condition for B, and quantum propositions are the □◇-stable sets. Baltag and Smets (2005) axiomatized the dynamic side and identified the key correspondence: the modality of the quantum test a?, giving the state after a successful yes-outcome measurement of a, is the Sasaki projection, so the dynamic formula [a?]b is precisely the Sasaki hook a →_S b. Because [a?] is a right adjoint it preserves meets, so the modality is normal in that respect even though the underlying lattice of propositions is not distributive. Their completeness results are relative to quantum transition systems, and their representation work characterizes Piron-style lattices by dynamic conditions rather than by the covering law. Orthologic itself is decidable, having cut elimination and the finite model property.

Applies to. Quantum information theory. Quantum protocols. Quantum computing foundations. Philosophy of quantum mechanics. Quantum game theory. Epistemic quantum states.

Limitations. Quantum tests do not compose: the Sasaki projections satisfy φ_a ∘ φ_b ≠ φ_{a ∧ b}, so [a?][b?]φ is not [(a ∧ b)?]φ and sequences of measurements cannot be collapsed, which is the modal form of import-export's failure. The propositional base is non-distributive, so proof by cases is unavailable and standard normal-modal machinery — canonical models, filtration, Sahlqvist correspondence — cannot be transplanted without first fixing a non-Boolean propositional algebra. There is no single necessity: □_A is indexed by an observable A, and nothing in the model selects one, so "necessarily φ" is always relative to a chosen measurement context. The epistemic reading inherits logical omniscience from any normal modality, and must decide whether measurement-induced state change is knowledge update or physical change — a commitment the formalism forces rather than derives. Goldblatt's translation covers orthologic, not orthomodular logic, so the orthomodular law is not captured by the modal embedding.