Quantifiers for quantum logic

Understand

We consider categorical logic on the category of Hilbert spaces.

• More generally, in fact, any pre-Hilbert category suffices.
• We characterise closed subobjects, and prove that they form orthomodular lattices.
• This shows that quantum logic is just an incarnation of categorical logic, enabling us to establish an existential quantifier for quantum logic, and conclude that there cannot be a universal quantifier.