 It is, conversely, possible to translate any \(\textsf{DPL}\)-formula \(\phi\) to a predicate logical formula \(\phi\)°, such that the domain of \([\phi]\) is the classical interpretation of \(\phi\)°. One of the ways to define this translation is by means of a precondition calculus, with Floyd-Hoare rules (Eijck and de Vries 1992). The following is a variation on this. Take the language of standard predicate logic, with diamond modalities \(\langle \psi \rangle \phi\) added, where \(\psi\) ranges over DPL formulas and \(\alpha \vDash \langle \psi \rangle \phi\) iff there is an assignment \(\beta\) with \(\alpha[\psi]\beta\), and \(\beta \vDash \phi\). Then the following equivalences show that this extension does not increase expressive power.