
cases, the proof of the Lindenbaum Lemma requires additional effort, since the logics in question are not compact. This additional effort can be summarized by the slogan saturated sets are maximal consistent, and this is done explicitly in Goldblatt (1993) and Segerberg (1994) . In PDL, formulas and programs are defined with mutual recursion, since test programs A? for arbitrary formulas A are allowed. This is unlike the logics treated in the completeness proofs in Goldblatt (1982 Goldblatt ( , 1987 Goldblatt ( , 1993 and Segerberg (1994) , where the recursion is nested: first the modalities/programs are defined, and then the formulas using the modalities or programs. The structure of the Truth Lemma reflects this. First, some property is proved for modalities/programs. This property is then used in the proof of the following formula property: a formula holds in a maximal consistent set in the canonical model iff it is an element of that set. For PDL ω , the property for programs and the formula property have to be proved via simultaneous induction. This requires some adaptation of the proofs mentioned above, but the adaptation is rather straightforward, as Professor Goldblatt has kindly shown us (in private correspondence). Thus, contrary to our remark on p. 70 that the proof in Goldblatt (1982) "does not transfer to PDL", there is an extension of Goldblatt's methods to PDL. In particular, Theorem 13.12 on first-order dynamic logic in Goldblatt (1987) straightforwardly leads to the Lindenbaum Lemma for PDL ω . Therefore, we no longer claim any priority regarding the proof of strong completeness of PDL ω . Indeed, the proof of Theorem 1 in Renardel de Lavalette et al. (2008) turns out to be a rather short argument that can be obtained by stripping down other, more general proofs to the bare essentials for PDL. 3. Finally, the notion of derivable sequent used in Lemma 1 of Renardel de Lavalette et al. (2008) does not correspond to Definition 4. This can be remedied by the following adaptation of Definition 4. A sequent ϕ is derivable iff it is the root of some derivation tree; a derivation tree is a well-founded tree (i.e. with all branches finite), with leaves labeled with axioms, and non-leaves labeled with sequents that are the conclusion of a rule with the labels of the children as premises. This yields an equivalent notion of derivability, corresponding to the definition in Mirkowska (1981) .

{'paper_id': '6035339', 'title': 'Strong Completeness and Limited Canonicity for PDL', 's2_url': 'https://api.semanticscholar.org/CorpusID:6035339', 'source': 'S2ORC'}