The modal logic of pure provability.
Samuel R. Buss · Notre Dame Journal of Formal Logic · 1990
We introduce a propositional modal logic PP of "pure" provability in arbitrary theories (propositional or first-order) where the D operator means "provable in all extensions".This modal logic has been considered in another guise by Kripke.An axiomatization and a decision procedure are given and the DO subtheory is characterized.