Inferring inductive invariants is one of the main challenges of formal verification. One of the latest breakthroughs in invariant inference is property-directed reachability (IC3/PDR). In this talk we investigate some of the unique properties of propositional PDR from the theoretical perspective. First, we show that the SAT queries performed by PDR, which enable an incremental construction of the invariant, are more powerful than simple inductiveness checks. In particular, we show that IC3 cannot be implemented in the ICE framework. Second, we utilize the rich theory of abstract interpretation to shed light on the overapproximation of the reachable states performed by PDR’s frames. Namely, we define an eager version of PDR, called Lambda-PDR, in which all generalizations of counterexamples are used to strengthen a frame, and show that its frames can be formulated as an abstract interpretation algorithm in a logical domain based on Bshouty’s monotone theory. Since the frames of Lambda-PDR are tighter than the frames of PDR, the same overapproximation, and more, is present in PDR’s frames. We demonstrate that this overapproximation can result in an exponential gap compared to exact forward reachability.