Theories of Frege structure equivalent to Feferman's system T0

Feferman [9] defines an impredicative system T 0 of explicit mathematics, which is proof-theoretically equivalent to the subsystem Delta 1 2- CA + BI of second-order arithmetic. In this paper, we propose several systems of Frege structure with the same proof-theoretic strength as T 0 . To be precise, we first consider the Kripke- Feferman theory, which is one of the most famous truth theories, and we extend it by two kinds of induction principles inspired by [22]. In addition, we give similar results for the system based on Aczel's original Frege structure [1]. Finally, we equip Cantini's supervaluation-style theory with the notion of universes, the strength of which was an open problem in [24]. (c) 2024 Elsevier B.V. All rights are reserved, including those for text and data mining, AI training, and similar technologies.