Verification logic

We introduce verification logics, variants of Artemov's logic of proofs LP with new terms of the form !phi! satisfying the axiom schema phi -> !phi!:phi. The intention is for !phi! to denote a proof of phi in an arithmetical theory - such as Peano arithmetic - whenever such a proof exists. By suitable restrictions of the domain of !.!, we obtain the verification logics VT, VS4, VS5, VL, respectively realizing the axioms of the modal logics T, S4, S5 and the 'trivial' modal logic axiomatized by p square p. Similarly to LP, each of VT, VS4, VS5, VL can be interpreted arithmetically, with some restrictions in the case of VL. Our main result is that each of VT, VS4, VS5, VL is complete for its arithmetical interpretation