  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.
