# Reasoning about Quantum Information: An Overview of Quantum Dynamic Logic
## 2 The Logic of Quantum Actions
### Semantics of \(Lqa\)  
The language of \(Lqa\) can be interpreted in terms of quantum frames or also called 'quantum transition systems'. We illustrate how this works for the concrete case starting from a given physical system and its given Hilbert space \(\mathcal{H}\). As standard, a Hilbert space \(\mathcal{H}\) is taken to be a complex vector space with an inner product \(<-|->\), which is complete in the induced metric. **Quantum Transition Systems. ** Any given Hilbert space \(\mathcal{H}\) of a physical system can be canonically structured as a _quantum transition system_ (also called 'quantum frame') \(\Sigma\) with the following signature:  
\[\Sigma=(\Sigma,\{\frac{P_{\Sigma}^{\mathfrak{T}}}{\}_{P\in\mathcal{L}},\{ \frac{U}{\mathfrak{U}}\}_{U\in\mathcal{U}}})\]  
This structure consists of a set \(\Sigma\) of states and two families of binary relations \(\{\overrightarrow{P}\}_{P\in\mathcal{L}}\subseteq\Sigma\times\Sigma\) and \(\{\frac{U}{\mathfrak{U}}\}_{U\in\mathcal{U}}\subseteq\Sigma\times\Sigma\) as explained below. In the remainder of this paragraph, we explain how a Hilbert space \(\mathcal{H}\) can be structured into a quantum frame \(\Sigma\). **State space. ** Given any set of vectors \(X\subseteq\mathcal{H}\) in a Hilbert space \(\mathcal{H}\), we denote by \(\overline{X}\) the closed linear subspace of \(\mathcal{H}\) generated by \(X\). In particular, for a singleton \(\{x\}\) consisting of only non-zero one-vector \(x\in\mathcal{H}\setminus\{0\}\), we can write \(\overline{x}\) for \(\overline{\{x\}}\), denoting the 'ray' (one-dimensional subspace) generated by \(x\). Our state space \(\Sigma:=\{\overline{x}:x\in\mathcal{H}\}\) is the set of all such rays (one-dimensional subspaces). **Orthogonality and Bi-orthogonal Closure. ** Two states in \(\Sigma\) are said to be _orthogonal_, written as \(s\perp t\), if every two vectors \(x\in s\), \(y\in t\) are orthogonal, that is, if their inner product \(<x|y>\) equals to \(0\). For a given set of states \(P\subseteq\Sigma\), we write \(P^{\perp}:=\{t\in\Sigma\,|\,t\perp s\text{ for all }s\in P\}\) for the set of its orthogonal states and we denote by \(P^{\perp\perp}:=(P^{\perp})^{\perp}\) the _bi-orthogonal closure_ of \(P\). **Testable Property. ** Any arbitrary set of states \(P\subseteq\Sigma\) is called a _logical property_, or 'proposition'. Moreover, a set of states \(P\subseteq\Sigma\) is called a _(quantum) testable property_ if and only if it is bi-orthogonally closed, i.e., if \(P=P^{\perp\perp}\). We use the notation \(\mathcal{L}\subseteq\mathcal{P}(\Sigma)\) to denote the family of all quantum-testable properties. Note that there is a natural bijective correspondence between the family \(\mathcal{L}\) of all testable properties and the family \(\mathcal{W}\) of all closed linear subspaces \(W\) of \(\mathcal{H}\), given by the bijection \(P\to W_{P}=:\bigcup P\). The image under this map of the bi-orthogonal closure \(P^{\perp\perp}\) of a set \(P\subseteq\Sigma\) coincides with the closed linear subspace generated by the union of its states: \(\bigcup P^{\perp\perp}=\overline{\bigcup P}\). It is this construction that will be crucial for us later in this section when providing an interpretation to the elements of our syntax of \(Lqa\), which makes essential use of these properties. **Quantum Tests. ** Recall that for any closed linear subspace \(W\subseteq\mathcal{H}\), the _projector_\(Proj_{W}:\mathcal{H}\to\mathcal{H}\) onto \(W\) is a linear operator given by: \(Proj_{W}(x+y)=x\), for all \(x\in W\), \(y\in W^{\perp}\) (where \(W^{\perp}=\{y\in\mathcal{H}:<x,y>=0\text{ for all }x\in W\}\) is the orthogonal space. Projector operators are idempotent (\(Proj_{W}\circ Proj_{W}=P\)) and self-adjoint (\(Proj_{W}^{\mathcal{H}}=Proj_{W}\)). Now, to every testable property \(P\in\mathcal{L}\subseteq P(\Sigma)\), we assign a partial map \(P\)? on \(\Sigma\), that we call the _quantum test_ of \(P\).