Birkhoff-von Neumann quantum logic enriched with entanglement quantifiers: coincidence theorem and semantic consequence

In this paper, we investigate a slightly simplified version of Birkhoff–von Neumann quantum logic enriched with entanglement quantifiers which is proposed in Ying (Birkhoff–von Neumann quantum logic as an assertion language for quantum programs, 2022. arXiv:2205.01959). The main result is a coincidence theorem, which says that every formula is interpreted by a closed subspace in the Hilbert space corresponding to the free variables of the formula. We also prove that many instances of semantic consequence, which are used in the proof of the prenex normal form theorem in first-order logic, also hold in this logic. The technical work is about the interplay among the three operations on density operators, namely, tensor product, support and partial trace.