The modal logic of pure provability

Abstract

We introduce a propositional modal logic PP of “pure” provability in arbitrary theories (propositional or first-order) where the □ 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 □O subtheory is characterized. © 1990 by the University of Notre Dame. All rights reserved.