Model theory and proof theory of the global reflection principle

The current paper studies the formal properties of the Global Reflection Principle, to wit the assertion "All theorems of Th are true," where Th is a theory in the language of arithmetic and the truth predicate satisfies the usual Tarskian inductive conditions for formulae in the language of arithmetic. We fix the gap in Kotlarski's proof from [15], showing that the Global Reflection Principle for Peano Arithmetic is provable in the theory of compositional truth with bounded induction only (CT0). Furthermore, we extend the above result showing that sigma(1)-uniform reflection over a theory of uniform Tarski biconditionals (UTB-) is provable in CT0, thus answering the question of Beklemishev and Pakhomov [2]. Finally, we introduce the notion of a prolongable satisfaction class and use it to study the structure of models of CT0. In particular, we provide a new model-theoretical characterization of theories of finite iterations of uniform reflection and present a new proof characterizing the arithmetical consequences of CT0.