Characterizing the NP-PSPACE Gap in the Satisfiability Problem for Modal Logic

There has been a great deal of work on characterizing the complexityof the satisfiability and validity problem for modal logics.In particular, Ladner showed that the satisfiability problemfor all logics between K and S4 is PSPACE-hard, while for S5it is NP-complete. We show that it is negative introspection,the axiom ¬K_p K¬K_p, that causes the gap: if we addthis axiom to any modal logic between K and S4, then the satisfiabilityproblem becomes NP-complete. Indeed, the satisfiability problemis NP-complete for any modal logic that includes the negativeintrospection axiom.