 A similar method can be applied in Propositional Dynamic Logic (PDL). PDL is a modal logic initially designed to talk about states and computer programs, it has a complete calculus whose axioms include the usual ones in modal logic K as well as other axioms describing the composition of programs (see the entry on  propositional dynamic logic).  Among them, it is worth highlighting Axiom 5. This axiom is also known as “induction axiom” and it is the responsible for one of the characteristic of PDL, its uncompactness. For this reason, the calculus of PDL is sound and complete but only in the weak sense.