Of course, PDL is an extension of classical propositional logic. We first expect that all propositional tautologies hold, and all propositional reasoning is allowed. In particular, modus ponens is a valid rule: from A and A → B infer B. For any program α, restricting an LTS to the relation R(α) we obtain a Kripke model in which the logic of the modality [α] is the weakest propositional normal modal logic, namely, the logic K. Thus, PDL contains every instance of the familiar distribution axiom schema: