# Reasoning about Quantum Information: An Overview of Quantum Dynamic Logic
## 2 The Logic of Quantum Actions  
[PERSON] presented his first ideas on quantum logic in [18] and later developed a setting for quantum logic together with [PERSON] in 1936 [19]. The main logical setting in [19] was presented in an algebraic-axiomatic form, but [PERSON] and [PERSON] provided a motivation for it that was based on specific semantic ingredients that come directly from the Hilbert-space formalism. At that time, in the early 1930s, the currently known methods of providing a formal semantics had not yet been used in the area of research on quantum logic. Indeed, it still took a while before [PERSON]'s work on the concept of truth in formalized languages (dating from 1930-1931 in Polish and from 1935 in German translation [20]) reached the main logic community. It was [PERSON], a logician and philosopher of science in Amsterdam, who proposed to apply [PERSON]'s semantic approach to the formal analysis of physical theories in 1948 and 1949 (see [21; 22; 23]). [PERSON] proposed to connect [PERSON]'s semantic method to the logical analysis of classical and quantum mechanics, referring for the latter, among others, to [PERSON] and [PERSON]'s work. The importance of the semantic method was picked up again later by philosophers of science at the end of the 1960s and early 1970s and was at that time brought to the attention of the wider quantum logic community by [PERSON] [24; 25; 26]. The semantic analysis of scientific theories certainly helped clarify the ways in which quantum logic can be viewed as a logic in its own right. We stress the importance of this development here for our paper, as it is crucial to understand this background of work when we highlight the important difference between syntax and semantics for our logic. This is the background that also provides insights on the importance of being able to evaluate the truth value of a given sentence in a model. So, here, we work with sentences in a given formal language that express information about the properties of a physical system. The models we work with consist of states at which we evaluate these sentences. Such states refer to the actual realizations of a physical system and belong to the main ingredients coming from physics. The way in which such a logic can be constructed will be made clear further in this section, which starts by introducing first the syntax of the main formalism of Quantum Dynamic Logic \(QDL\) and then its quantum semantics.  
The design of the logical language below will provide us with enough expressive power to talk about the states and properties of physical systems and comes equipped with operators to model the effect of the main quantum-physical actions (or programs) on these systems, i.e., quantum measurements and unitary evolutions. Zooming in on these quantum actions, we will restrict our attention to a specific type of quantum measurements called \"binary measurements\". Binary measurements consist of a pair of two so-called \"physical tests\": one test (or experimental procedure) will come with a specification to check if a given physical property holds, the other one is the test for its negation. Such a test of a physical property (or of its negation) is called successful if, as a result of actually performing the test, the state of the system afterwards will exhibit the tested property. In our logical language, we take such successful tests of physical properties as one of the basic building blocks. Another main building block is given by the unitary evolutions, capturing the specific \"quantum logical gates\" in quantum information theory such as for instance the Hadamard gate and the controlled NOT gate. Together, these building blocks for quantum actions form the layer of quantum programs in the language below, where such programs are used to express the possible transitions that a quantum system can undergo when it moves from one state to another.