 The novelty is that now we have another domain \(\mathbf{W}^{\prime \prime }\) to include the binary relations defined by programs. Using these structures, one can prove that validity of a dynamic formula is equivalent to the validity of the universal closure of its translation in the class \(\mathcal{E}\) of all many sorted structures obtained in this way. The representation theorem is also available, once we define the theory \(\Delta _{\PDL}\). This theory includes as axioms the many-sorted abstract conditions for the PDL axioms, Extensionality (both for sets and relations) as well as Comprehension axiom for sets and relations defined by translations of formulas and programs.