# Reasoning about Quantum Information: An Overview of Quantum Dynamic Logic
## 2 The Logic of Quantum Actions
### Semantics of \(Lqa\)
For programs, the relations \(\stackrel{{ U}}{{\rightarrow}}\) are already given as part of the structure of our quantum transition system, while for tests \(\varphi?\), we put  
\[s\stackrel{{\varphi?}}{{\rightarrow}}t\text{ iff }\overline{\bigcup\| \varphi\|}?(s)=\|\varphi\|^{\perp\perp}?(s)=t.\]  
In addition, we have the following recursive clauses for programs:  
\[s\stackrel{{\pi_{1}\cup\pi_{2}}}{{\longrightarrow}}t\text{ iff }s \stackrel{{\pi_{1}}}{{\rightarrow}}u\stackrel{{\pi_{2}}}{{ \rightarrow}}t\text{ for some }u\in\Sigma\]  
\[P\overline{x}:=\overline{Proj_{W}(x)}\in\Sigma,\text{ if }\overline{x}\
ot\in P ^{\perp}(\text{i.e., if }Proj_{W}(x)\
eq 0)\]0  
These clauses use the fact that the set \(P(\Sigma)\) of all the logical properties of a physical system is closed under the standard set-theoretic operations. However, note that the quantum testable properties in \(\mathcal{L}\) are only a _subset_ of the set \(P(\Sigma)\) of all logical properties, corresponding to  
components. In case we impose specific restrictions on one or another component, then we will make this explicit in the text. For now, it is important to note that epistemic logic is ideal to reason about the spatial features of such systems that are composed of different components. The added value of epistemic logic is that it comes equipped with epistemic operators that can capture the actual and potentially available information, which is viewed from the perspective of one component (or location) \(i\in N\) or from the perspective of a group of components (or a complex subsystem) \(I\subseteq N\). The largest group of components is the entire system \(N\), while the smallest groups are singletons \(\{i\}\) consisting of an individual component. **Syntax of the Quantum Epistemic Fragment. ** To reason about compound physical systems, we extend the dynamic fragment \(LQA\) of our language with an epistemic operator:  
\[ \begin{array}{ccccc|c}\varphi&::=&p&|\
eg\varphi&|\varphi\wedge\varphi&|[ \pi]\varphi&|K_{I}\varphi\\ \pi&::=&U&\varphi^{2}&|\pi\cup\pi&|\pi;\pi\end{array} \]  
The syntax of our epistemic extension includes an \"information\" (or \"implicit knowledge\") operator \(K_{I}\) for each subsystem \(I\) of a given physical system. As stressed in [5], the term knowledge is used here only in the _implicit, external_ sense as \"information that is in principle available\" via local observations at a given location. Informally, proposition \(K_{I}\varphi\) refers to the fact that the subsystem \(I\) (potentially) carries the information that \(\varphi\) is the case. In the case of one component or individual agent, we write \(K_{\{i\}}\) or simply \(K_{i}\). **Key Semantic Notions. ** Before we can provide an interpretation to the main epistemic ingredient in our language, we need to introduce a number of key semantic concepts. As the system can be composed of different subsystems, this requires a new concept to refer to the state of a specific subsystem. Similarly, we need to introduce new notions to refer to the actions on a system that affect only a subsystem. **I-Local States. ** Let us consider a concrete quantum system composed of \(N\) subsystems \(1,\ldots,n\) as described in the Hilbert space formalism of quantum theory so that its state space \(\Sigma=\Sigma_{1}\otimes\cdots\otimes\Sigma_{n}\) is generated from the _tensor product_\(\mathcal{H}_{1}\otimes\cdots\otimes\mathcal{H}_{n}\) of \(n\) Hilbert spaces. In quantum theory, the \"state\" of subsystem \(I\) can be obtained by taking the partial trace \(tr_{N\setminus I}\) (with respect to the subsystem's environment \(N\setminus I\)) of the density operator 3 associated to the global state \(s\in\Sigma\). So, if a global system is in state \(s\), having an associated density operator \(\rho_{s}\), then the state \(s_{I}\) of any of its subsystems \(I\) (possibly entangled with its environment \(N\setminus I\) in the state \(s\)) is given by :  
Footnote 3: The \(I\)-local states are \(tr_{N\setminus I}(\rho_{s})\) and \(tr_{N\setminus I}(\rho_{s})\).