Abstract
This paper is devoted to the completeness issue of PDL_0^∩ – an iteration-free fragment of Propositional Dynamic Logic with intersection of programs. The trouble with PDL_0^∩ is that the operation of intersection is not modally definable. Using new techniques connected with rules for intersection and the notions of large and maximal programs, the paper demonstrates that the presented proof theory for PDL_0^∩ is complete for the standard Kripke semantics of PDL_0^∩.