The formal language of Propositional Dynamic Logic (PDL) is built up from two sets of primitive symbols, a countable set of atomic formulae and a countable set of atomic programs. The set of formulae is the least set containing and is closed under the rules: if and are formulae then and are formulae; if is a formula and is a program then is a formula. The set of programs is the least set containing all atomic programs and closed under the rule: if and are programs then , and are programs; if is a formula then is a program.
The dual operator to is defined as follows:
The intuitive reading of the program connectives and the formulae are as follows:
A PDL-model is a structure , where is a non-empty set, is a function which assigns to every program a binary relation on , and is a valuation function which assigns to every atomic formula a subset of .
The satisfaction relation `` is true at point in model '', denoted , is defined inductively on the formation of as follows:
To preserve the intuitive reading of the program connectives, the following formal requirements must be met:
Well-known results say that PDL is decidable and finitely axiomatizable (cf. [Har84], [Gol87], [KT90]). A complete axiomatization consists of the following axioms and inference rules:
It can be shown that the axiom (A5) is still valid if , i.e., if the program construct is interpreted by the transitive closure of the relation corresponding to , and not by the reflexive, transitive one. This fact explains how the minimal temporal logic of transitive time K4 (with only the future operators) can be embedded into dynamic logic: the temporal operator ``always in the future'' is interpreted by the operator , where is any (atomic) program.