Truth in applicative theories (Q5951914)

The paper under review is concerned with theories of partial truth over type-free combinatory logic. The notion of self-reflective truth considered has its roots in work by Aczel, Feferman, Fitch, Kripke, Scott and others, see \textit{A. Cantini} [Logical frameworks for truth and abstraction. An axiomatic study, North Holland, Amsterdam (1996; Zbl 0860.03015)] for a comprehensive treatment of truth theories over applicative theories. After introducing the general formal framework and recalling some of the standard results with respect to proof-theoretic strength, the main emphasis in the present paper in on a concise presentation of the author's own recent work in this area of research. The main achievement is the set up of a suitable truth-theoretic notion of \textit{universe} and corresponding generation principles for such universes. The so-obtained truth theories have a strong connection to universes studied in the context of metapredicative explicit mathematics, Martin-Löf type theory, and admissible set theory. Indeed, the author's main proof-theoretic results state that his systems are proof-theoretically equivalent to the corresponding systems in the above mentioned frameworks. Moreover, all these theories are strongly linked to so-called transfinitely iterated fixed point theories as studied by \textit{G. Jäger, R. Kahle, A. Setzer}, and \textit{T. Strahm} [J. Symb. Log. 64, 53-67 (1999; Zbl 0937.03065)]. The final part of the paper elaborates on previous work by Cantini on the notion of \textit{supervaluation} (due to van Fraassen) in an axiomatic setting of truth. In particular, it is shown that the well-known theory for one-inductive definitions \(\text{ID}_1\) is contained in a natural framework based on supervaluation. To sum up, the paper offers an interesting survey on recent developments in the proof theory of axiomatic truth theories.