Concerning the proof theory of IPDL, difficulties appear when we realize that no axiom schema, in the language of PDL with intersection, “corresponds” to the semantics  xR(α∩β)y iff xR(α)y and xR(β)y of the program α∩β. That is, not in the same way for example, that the axiom schemas (A1) and (A2) respectively “correspond” to the semantics of the programs α;β and α∪β.  For this reason, the axiomatization of PDL with intersection was open until the complete proof system developed in Balbiani and Vakarelov [2003].