The complete axiomatization of PDL is a recursive definition of the set of valid PDL formulas, or in other words, of the set of formulas whose negation is not satisfiable. Hence, concerning the problem (PDL-SAT), we have a sub-procedure that would answer “no” if the PDL formula A were not satisfiable. The sub-procedure (SP1) consists in enumerating all the formulas ⊢-deducible, starting from the axioms and inferring other theorems with the help of the inference rules. Given enough time, if a formula is ⊢-deducible, the sub-procedure would find it eventually. Thus, if A is not satisfiable, (SP1) must eventually find ¬A, and answer “no” when it does.