# Reasoning about Quantum Information: An Overview of Quantum Dynamic Logic
## 2 The Logic of Quantum Actions
### Semantics of \(Lqa\)
_Information is Monotonic with respect to groups_[4]: if \(I\subseteq J\) then \(\sim_{I}\subseteq\sim_{I}\);
3. _Observability Principle_: if \(s\sim_{N}s^{\prime}\) then \(s=s^{\prime}\). 4. _Vacuous Information_: \(s\sim_{\varnothing}s^{\prime}\) for all \(s,s^{\prime}\in\Sigma\). The given properties (1-4) of \(\sim_{I}\) seem natural when thinking of the relations \(\sim_{I}\) in terms of observational equivalence. The first property captures that we see these states as equivalent from the perspective of one subsystem. The second property captures the fact that the states that are observationally equivalent for a system/group \(I\) are also observationally equivalent for any subgroup \(J\subseteq I\). The third property states that if two states are indistinguishable with respect to the global system \(N\), then they are the same. The last property captures the fact that the empty group cannot distinguish between any two states. **Semantics. ** The semantic structure of the quantum epistemic fragment of our logic will extend \(\Sigma\) with the family of binary relations \(\{\sim_{I}\}_{I\subseteq N}\subseteq\Sigma\times\Sigma\), one for every subsystem \(I\subseteq N\). As explained above, the relation \(\sim_{I}\) is used to capture a notion of \"observational equivalence\" between possible states of the system. Below, this relation of observational equivalence is employed to give an interpretation to the \(K_{I}\)-operator. **Interpretation of the Epistemic Operator. ** The epistemic modality \(K_{I}\varphi\) in our language is used to express the fact that the subsystem \(I\) carries the information that \(\varphi\) holds (as a property of the global system). As already mentioned, the quantum information carried by a subsystem \(I\) (when the global system is in state \(s\)) is given by its local state \(s_{I}=tr_{N\setminus I}(\rho_{s})\). So, we say that \(I\) 'knows' \(\varphi\) whenever \(\varphi\) is entailed by \(I\)'s local state; i.e., we set:  
\[s\in\;\|K_{I}\varphi\|\;\;\text{iff }\;s_{I}\subseteq\|\varphi\|\]This amounts to defining  
\[\|K_{I}\varphi\|\,:=\,\{s\in\Sigma:t\in\|\varphi\|\text{ for every }t\sim_{I}s\},\]  
which matches the usual definition of knowledge \(K_{I}\) in epistemic logic as the Kripke modality for the corresponding indistinguishability relation \(\sim_{I}\):  
\[s\in\|K_{I}\varphi\|\ \text{ iff }\ t\in\|\varphi\|\text{ for all }t\sim_{I}s.\]  
**Properties of Quantum 'Knowledge'** Using standard results on correspondence theory in Modal Logic, we can see that the above-mentioned four properties of observational equivalence correspond to the following properties of our epistemic operators:  
1. \(K_{I}\) satisfies the _axions of the standard modal-epistemic system \(S5\)_: \(K_{I}\varphi\Rightarrow\varphi\) (Factivity of Knowledge); \(K_{I}\varphi\Rightarrow K_{I}K_{I}\varphi\) (Positive Introspection); \(\
eg K_{I}\varphi\Rightarrow K_{I}\
eg K_{I}\varphi\) (Negative Introspection);
2. _Monotonicity of Knowledge_: if \(I\subseteq J\), then \(K_{I}\varphi\Rightarrow K_{I}\varphi\) (every system knows everything 'known' by its subsystems);
3. _Observability_: \(\varphi\Rightarrow K_{N}\varphi\) (the global system 'knows' everything):
4. _Vacuity_: \(K_{\emptyset}\) is the global modality, quantifying universally over all states (so, in particular, we have \(K_{\emptyset}\varphi\Rightarrow[\pi]\varphi\)). In the remainder of this section, we illustrate how our formalism can be used to model entangled quantum systems that contain non-local information. **Epistemic Characterization of Entanglement and Separability. ** As explained in [5], we can provide an epistemic-informational characterization of entanglement and separability. To formalize this, we need to be given a formula \(\varphi_{0}\) that denotes the state \(s_{0}=|00\cdots 0\rangle=|0\rangle\otimes\cdots\otimes|0\rangle\) (consisting of \(n\) separated bits).