dynamic logic a branch of logic in which, in addition to the usual category of formulas interpretable as propositions, there is a category of expressions interpretable as actions. Dynamic logic (originally called the modal logic of programs) emerged in the late 1970s as one step in a long tradition within theoretical computer science aimed at providing a way to formalize the analysis of programs and their action. A particular concern here was program verification: what can be said of the effect of a program if started at a certain point? To this end operators [a] and ‹a( were introduced with the following intuitive readings: [a]A to mean ‘after every terminating computation according to a it is the case that A’ and ‹a(A to mean ‘after some terminating computation according to a it is the case that A’. The logic of these operators may be seen as a generalization of ordinary modal logic: where modal logic has one box operator A and one diamond operator B, dynamic logic has one box operator [a] and one diamond operator ‹a( for every program expression a in the language. In possible worlds semantics for modal logic a model is a triple (U, R, V) where U is a universe of points, R a binary relation, and V a valuation assigning to each atomic formula a subset of U. In dynamic logic, a model is a triple (U, R, V) where U and V are as before but R is a family of binary relations R(a), one for every program expression a in the language. Writing ‘Xx A’, where x is a point in U, for ‘A is true at x’ (in the model in question), we have the following characteristic truth conditions (truth-functional compounds are evaluated by truth tables, as in modal logic): Xx P if and only if x is a point in V(P), where P is an atomic formula, Xx[a]A if and only if, for all y, if x is R(a)- related to y then Xy A, Xx ‹a( if and only if, for some y, x is R(a)-related to y and Xy A. Traditionally, dynamic logic will contain machinery for rendering the three regular operators on programs: ‘!’ (sum), ‘;’ (composition), and ‘*’ (Kleene’s star operation), as well as the test operator ‘?’, which, operating on a proposition, will yield a program. The action a ! b consists in carrying out a or carrying out b; the action a;b in first carrying out a, then carrying out b; the action a* in carrying out a some finite number of times (not excluding 0); the action ?A in verifying that A. Only standard models reflect these intuitions: R(a ! b) % R(a) 4 R(b), R(a;b) % R(a) _ R(b), R(a*) % (R(a))*, R(?A) % {(x,x) : Xx A} (where ‘*’ is the ancestral star) The smallest propositional dynamic logic (PDL) is the set of formulas true at every point in every standard model. Note that dynamic logic analyzes non-deterministic action – this is evident at the level of atomic programs p where R(p) is a relation, not necessarily a function, and also in the definitions of R(a + b) and R(a*). Dynamic logic has been extended in various ways, e.g., to first- and second-order predicate logic. Furthermore, just as deontic logic, tense logic, etc., are referred to as modal logic in the wide sense, so extensions of dynamic logic in the narrow sense such as process logic are often loosely referred to as dynamic logic in the wide sense. The philosophical interest in dynamic logic rests with the expectation that it will prove a fruitful instrument for analyzing the concept of action in general: a successful analysis would be valuable in itself and would also be relevant to other disciplines such as deontic logic and the logic of imperatives. See also COMPUTER THEORY , DEONTIC LOGIC , MODAL LOGI. K.Seg.