In constructive type theory and explicit mathematics, the idea of universes has been used to strengthen the expressive power or the proof-theoretic strength of a given system. Similarly, Cantini (1996) and Kahle (2003) introduced universes for axiomatic truth theories over TON (total applicative theory). Set-theoretic universes are usually large sets that are closed under several operations like complements, whereas truth-theoretic universes can be seen as quasi-truth predicates which satisfy some axioms for the truth predicate. Cantini and Kahle then showed that by adding the axiom assuring the existence of universes, several truth theories become proof-theoretically stronger.

In this talk, I will formulate the theory VFU, an extension of Cantini’s supervaluational truth theory VF (cf. Kahle, 2002) with the universe-generating axiom, and then prove that VFU has the same proof-theoretic strength as KPi (Kripke-Platek set theory with the recursively inaccessible universe) and T0 (Feferman’s explicit mathematics with the inductive generation axiom). To determine the lower bound, I show that T0 is relatively interpretable in VFU. As for the upper bound, I give a truth-as-provability interpretation for VFU, where the truth predicate is understood as the provability in a certain infinite derivation system. As this is formalisable in KPi, a relative interpretation of VFU in KPi is obtained. Therefore, all the three systems are proof-theoretically equivalent. Finally, I would like to mention the possibility of constructing natural numbers in VFU.