 Given the axioms for \(\text S\) we can lay out the rest of Prior’s system Q. For its non-modal foundations, Q takes every propositional tautology (not just its closures, as in KQML) to be an axiom and follows SQML in adopting standard classical axioms for quantification and identity. However, the non-modal fragment of the system itself is not quite classical. For reasons we will discuss below, it includes a modified version of modus ponens that renders some classical first-order validities unprovable.