EXPLICIT G¨ODEL-L¨OB PROVABILITY LOGIC

Artemov in [1] initiated the study of explicit modal logics (now known as justification logics) by introducing Logic of Proofs, LP, as explicit counterpart of modal logic S4. Relationship between LP and S4 is stated in the Realization Theorem: any theorem of S4 can be converted into a theorem of LP, and vise versa. In this paper, we study the explicit counterpart of G¨odel-L¨ob provability logic GL, that is called JGL. Semantics (Mkrtychev-models) is given, and disjunction property is established. Using Mkrtychev-models we prove that JGL is a conservative extension of J4.