On positive fragments of polymodal provability logic

We consider positive fragments of well-known provability logics GLP and GL. The study is motivated by the fact that some important proof-theoretic applications essentially rely on the positive fragment, rather than the full system of GLP. For the fragments, we suggest sequential and equational calculi and develop an arithmetical interpretation.