Types and truth in weak applicative theories

In this talk we survey recent developments in the study of prooftheoretically weak systems of Feferman's explicit mathematics and theories of truth. We start off from pure first-order applicative theories based on a version of untyped combinatory logic and augment them by the typing and naming discipline of explicit mathematics or, alternatively, by a truth predicate in the sense of Frege structures. We discuss the proof-theoretic strength of the so-obtained formalisms and the general relationship between weak truth theories and explicit mathematics. In particular, we consider two truth theories TPR and TPT of primitive recursive and feasible strength. The latter theory is a novel abstract truth-theoretic setting which is able to interpret expressive feasible subsystems of explicit mathematics, bounded arithmetical systems, and unfoldings of feasible arithmetic.
(Joint work with Sebastian Eberhard.)