Principles of Constructive Provability Logic (CMU-CS-10-151)

We present a novel formulation of the modal logic CPL, a constructive logic of provability that is closely connected to the Godel-L ¨ ob logic of provability. Our logical formulation allows modal ¨ operators to talk about both provability and non-provability of propositions at reachable worlds. We are interested in the applications of CPL to logic programming; however, this report focuses on the presentation of a minimal fragment (in the sense of minimal logic) of CPL and on the formalization of minimal CPL and its metatheory in the Agda programming language. We present both a natural deduction system and a sequent calculus for minimal CPL and show that the presentations are equivalent.