Provability logic with operations over proofs

We present a natural axiomatization for propositional logic with modal operator for formal provability (Solovay, [5]) and labeled modalities for individual proofs with operations over them (Artemov, [2]). For this purpose the language is extended by two new operations. The obtained system $\mathcal{MLP}$ naturally includes both Solovay's provability logic GL and Artemov's operational modal logic $\mathcal{LP}$. All finite extensions of the basic system $\mathcal{MLP}_{0}$ are proved to be decidable and arithmetically complete. It is shown that $\mathcal{LP}$ realizes all operations over proofs admitting description in the modal propositional language.