Interpretability suprema in Peano Arithmetic
Paula Henk, Albert Visser · Archive for Mathematical Logic · 2017
This paper develops the philosophy and technology needed for adding a supremum operator to the interpretability logic $$\mathsf {ILM}$$ of Peano Arithmetic ( $$\mathsf {PA}$$ ). It is well-known that any theories extending $$\mathsf {PA}$$ have a supremum in the interpretability ordering. While provable in $$\mathsf {PA}$$ , this fact is not reflected in the theorems of the modal system $$\mathsf {ILM}$$ , due to limited expressive power. Our goal is to enrich the language of $$\mathsf {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 $$\mathsf {GL}$$ .