The closed fragment of the interpretability logic of PRA with a constant for IΣ1

In this paper we characterize the closed fragment of the enriched probability logic of PRA and call the logic characterizing it PGL. These logics are enriched in the sense that they contain a constant symbol S which denotes the arithmetical sentence axiomatizing IΣ1. We also determine the closed fragment of the interpretability logic of PRA with a constant IΣ1 which we baptize PIL. We show that IΣ1 proves the consistency of PRA on a cut. By restricting the possible substitutions in Solovay's theorem we obtain a rough upperbound for the full interpretability logic of PRA