# Reasoning about Quantum Information: An Overview of Quantum Dynamic Logic
## 2 The Logic of Quantum Actions
### Syntax of Quantum Dynamic Logic  
Given a list (ordered set) \(\Omega\) of atomic sentences \(p,q,\ldots\), and a list \(\mathcal{U}\) of actions symbols (meant to denote unitary evolutions), the full language of quantum dynamic logic consists of two layers: a layer of well-formed formulas \(\varphi\) and a layer of programs \(\pi\) defined by mutual induction as follows in BNF form:  
\[ \begin{array}{lclclclclcl}\varphi&::=&p&\mid\
eg\varphi&\mid\varphi\wedge \varphi&\mid[\pi]\varphi&\mid K_{I}\varphi\mid P^{\geq r}\varphi\\ \pi&::=&U&\mid\varphi?&\mid\pi\cup\pi&\mid\pi;\pi\end{array} \]  
where \(p\in\Omega\) and \(U\in\mathcal{U}\). We will explain the language of this logic in different stages by focussing on specific fragments. We start first with the dynamic fragment of this logic, which is called the _logic of quantum actions_\(LQA\), and it is obtained by leaving out the epistemic operators \(K_{I}\) and the probabilistic statements \(P^{\geq r}\varphi\) (which will be explained in the next section). **The Language of \(LQA\). ** More concretely, the fragment \(LQA\) consists of the following two layers, which are defined by mutual induction2:  
Footnote 2: The notation \(\varphi\) is used for arbitrary formulas, i.e., well-formed statements about the properties and states of physical systems. The formulas are built from atomic sentences \(p,q,\ldots\)coming from a given set \(\Omega\), using logical connectives. The state in which a system can be realized is itself a physical property and can similarly be expressed via an atomic sentence. **Propositional Constructs: negation, conjunction and dynamic modalities. ** Among our logical connectives, we have a classical _negation_: intuitively, \(\
eg\varphi\) expresses the fact that property \(\varphi\) does _not_ hold in the current state of the system. We also have a classical _conjunction_\(\varphi\wedge\psi\), intuitively expressing the fact that _both_ properties \(\varphi\) and \(\psi\) hold in the current state. Finally, the dynamic modality \([\pi]\varphi\) uses ingredients from both the layer of well-formed formulas and the layer of programs. Intuitively, the dynamic modality \([\pi]\varphi\) is the _weakest precondition_ that ensures that a property \(\varphi\) will hold after the execution of the action/program \(\pi\). In other words, \([\pi]\varphi\) expresses the fact that if action \(\pi\) is successfully performed in the current state of the statement, then property \(\varphi\) will definitely hold after that (in any of the possible output states that this action may yield). **Program constructs of _LQA. ** The basic building-blocks of our quantum program constructs \(\pi\) in the language of _LQA_ are _quantum tests_\(\varphi\)? of a property \(\varphi\) (where \(\varphi\) comes from the layer of well-formed formulas), as well as _unitary evolutions_\(U\) of the physical system. The first intuitively denotes the successful measurement of a property \(\varphi\) (whose formal semantics will be later given in terms of projectors), while the second corresponds to the so-called \"quantum logical gates\" used in Quantum Computing. More complex programs are built using _concatenation_ (sequential composition) of programs \(\pi;\pi^{\prime}\), and the _non-deterministic choice_ (union) of programs \(\pi\cup\pi^{\prime}\). Concatenation makes it possible to express, e.g., the performance of a test after we let the system evolve via a logical gate. The arbitrary choice of programs makes it possible to express binary measurements as non-deterministic choices between two successful tests (and more generally, arbitrary measurements in a finite basis as choices between finitely many tests). **Abbreviations: classical disjunction and implication, tautology and contradiction. ** Classical _disjunction_ can be introduced as an abbreviation, namely as the De Morgan dual of conjunction: \(\varphi\vee\psi:=\
eg(\
eg\varphi\wedge\
eg\psi)\). Classical material _implication_ is also defined in the standard way as \(\varphi\Rightarrow\psi:=\
eg\varphi\vee\psi\).