Nonstandard provability for Peano Arithmetic: A modal perspective

This thesis is a study of nonstandard provability predicates for Peano Arithmetic (PA). By a nonstandard provability predicate, we mean the provability predicate of a theory that coincides with PA from the external point of view, however not verifiably in PA. Our perspective is shaped by modal logic: the goal is to determine which modal principles govern the behaviour of our nonstandard provability predicates in PA.
Chapter 3 deals with the bimodal provability logic GLT. We show that GLT - while lacking the finite model property - is decidable, and complete with respect to several natural classes of Kripke frames. We provide a characterisation of the closed fragment of GLT, and establish its arithmetical completeness with respect to a wide class of provability predicates.
Chapter 4 is concerned with theories obtained from PA by speeding up or slowing down ordinary provability. We show that GLT is arithmetically complete with respect to a wide class of provability predicates, including ordinary and fast, as well as slow and ordinary provability.
Chapter 5 studies the so-called supremum adapters. These provability predicates are useful for obtaining interpretability suprema of finite extensions of PA. We first discuss methodological issues arising from the enterprise of adding supremum operators to the interpretability logic ILM of PA. The supremum adapters provide a convenient solution. We establish some modal principles for these operators, and study the behaviour of their transfinite iterations.
In Chapter 6 it is shown that the provability logic of a certain supremum adapter is the Gödel-Löb provability logic GL.
Finally, in Chapter 7 we establish some connections between the supremum adapters and the slow provability predicates.