Interpretability over Peano arithmetic

Abstract

We investigate the modal logic of interpretability over Peano arithmetic (PA). Our main result is an extension of the arithmetical completeness theorem for the interpretability logic ILMω. This extension concerns recursively enumerable sets of formulas of interpretability logic (rather than single formulas). As corollaries we obtain a uniform arithmetical completeness theorem for the interpretability logic ILM and a theorem answering a question of Orey from 1961. All these results also hold for Zermelo-Fraenkel set theory (ZF).