Interpretability suprema in Peano Arithmetic

This paper develops the philosophy and technology needed for adding a supremum operator to the interpretability logic ILM of Peano Arithmetic (PA). It is well-known that any theories extending PA have a supremum in the interpretability ordering. While provable in PA, this fact is not reflected in the theorems of the modal system ILM, due to limited expressive power. Our goal is to enrich the language of ILM by adding to it a new modality for the interpretability supremum. We explore different options for specifying the exact meaning of the new modality. Our final proposal involves a unary operator, the dual of which can be seen as a (nonstandard) provability predicate satisfying the axioms of the provability logic GL.