Reflecting on Truth and Types

The goal of this research is to deepen our understanding of varying forms of reflection principle and their interrelation. We focus primarily on two distinct forms critical in characterising the concepts and understanding inherent in general mathematics: reflections of formal truth in logical languages and the universal reflection and induction principles at the cornerstone of type theory. The analysis will involve core methods from proof theory, model theory and constructive mathematics.