Although intersection of programs plays an important role in various applications of PDL to artificial intelligence and computer science, the proof theory and the complexity theory of PDL with intersection remained unexplored for several years. Concerning the complexity theory of IPDL, difficulties appear when one considers the finite model property.  In fact the construct sloop(α) can be expressed in IPDL. In propositional dynamic logic with intersection it is equivalent to &lt;α∩1?&gt;1. We can thus adapt the formula of   IPDL of section 4.3, and we have that