# Reasoning about Quantum Information: An Overview of Quantum Dynamic Logic
## 2 The Logic of Quantum Actions
### Semantics of \(Lqa\)
\[s_{I}:=tr_{N\setminus I}(\rho_{s})\]  
We call \(s_{I}\) the \(I\)-local state of a system that captures the state of information about the global system viewed from the perspective of (sub)system \(I\subseteq N\). We denote by \(\Sigma_{I}\) the set of all local states \(s_{I}\). **I-Local Actions. ** In addition to the notion of an \(I\)-local state, we introduce the notion of an \(I\)-local action such as an \(I\)-local test or \(I\)-remote unitary evolution. On a given system \(N\), an action can be described as a map \(T:\Sigma\rightarrow\Sigma\) that transforms one state into another state. For a subsystem \(I\subseteq N\), \(I\)-_local actions_ are maps from \(I\)-local states to \(I\)-local states, i.e., maps \(T_{I}:\Sigma_{I}\rightarrow\Sigma_{I}\). In the quantum case, these maps are required to be linear. There are two types of \(I\)-local actions that are important for us: tests and unitary evolutions. What we call quantum \(I\)-local-tests are actions denoted by \(S_{I}\)? that test an \(I\)-local property. In the Hilbert space formalism, these \(I\)-local tests correspond to the projectors onto a subspace generated by \(S_{I}\) of \(\mathcal{H}_{I}=\bigotimes_{I}\mathcal{H}_{i}\). The \(I\)-local evolutions are actions \(U_{I}\) induced on \(\Sigma_{I}\) by unitary evolutions \(U:\mathcal{H}_{I}\rightarrow\mathcal{H}_{I}\). We denote global actions as the \(N\)-actions \(T:\Sigma\rightarrow\Sigma\) on the global state space. Given a (global) \(N\)-action \(T:\Sigma\rightarrow\Sigma\), we call this action \(I\)-_local_ if there exists some \(I\)-local action \(T_{I}:\Sigma_{I}\rightarrow\Sigma_{I}\) such that the global action \(T\) can be written as follows:  
\[T(s_{I}\otimes s_{N\setminus I})=T_{I}(s_{I})\otimes s_{N\setminus I}\ \ \text{ for all}\ s_{I}\in\Sigma_{I},s_{N\setminus I}\in\Sigma_{N\setminus I}.\]Here, we use \(\otimes\) as the notation for product states as usual in quantum mechanics. **Observational Equivalence. ** The above abstract description of \(I\)-local states in terms of the mixed states of a quantum system serves us well to extract a relation of 'observational equivalence' \(\sim_{I}\subseteq\Sigma\times\Sigma\) on global states as follows:  
\[s\sim_{I}s^{\prime}\text{ iff }tr_{N\setminus I}(\rho_{s})=tr_{N\setminus I}( \rho_{s}^{\prime})\]  
This relation of observational equivalence \(s\sim_{I}s^{\prime}\) expresses that for any two possible states \(s\) and \(s^{\prime}\), if the implicit information carried by a system \(I\) is the same in these two states, then they are \"observationally equivalent\", or \"indistinguishable\" from the perspective of system \(I\). More specifically, this means that the observations that can be made from the perspective of \(I\) in states \(s\) and \(s^{\prime}\) are exactly the same. Concretely, an \(I\)-local state satisfies the following:  
\[s_{I}:=\{s^{\prime}\in\Sigma:s\;\sim_{I}\;s^{\prime}\}\]  
In other words, we can express the _local state_\(s_{I}\) of a system (which is in a global state \(s\in\Sigma\)) as an \(\sim_{I}\)-equivalence class consisting of a set of global states that are informationally consistent with the \(I\)th-subsystem. Note that in [5], we made use of \(I\)-local actions in order to show two other equivalent possible characterizations of 'observational equivalence' as a relation on \(\Sigma\). More specifically, for \(I\subseteq N\), and \(s,s^{\prime}\in\Sigma\), the following statements are equivalent:  
**(1). **: \(tr_{N\setminus I}(\rho_{s})=tr_{N\setminus I}(\rho_{s^{\prime}})\);
**(2). **: For every \(I\)-local test, the probability of obtaining any given result is the same in state \(s\) as in state \(s^{\prime}\);
**(3). **: \(s^{\prime}=U(s)\) for some \(I\)-remote unitary map \(U\). **Properties of Observational Equivalence. ** One can observe that these equivalent expressions of observational equivalence will all satisfy the following properties:  
1. All \(\sim_{I}\) are equivalence relations (i.e., they are reflexive, transitive, and symmetric relations), labeled by sets \(I\subseteq N\);
2.