This paper deals with universes in explicit mathematics. After introducing some basic definitions, the limit axiom and possible ordering principles for universes are discussed. Later, we turn to least universes, strictness and name induction. Special emphasis is put on theories for explicit mathematics with universes which are proof-theoretically equivalent to Feferman's.

This paper is concerned with the interaction between formal semantics and the foundations of mathematics. We introduce a formal theory of truth, TLR, which extends the classical first order theory of pure combinators with a primitive truth predicate and a family of truth approximations, indexed by a directed partial ordering. TLR naturally works as a theory of partial classifications, in which type-free comprehension coexists with functional abstraction. TLR provides an inner model for a well known subsystem of second order arithmetic; (...) indeed, TLR is proof-theoretically equivalent to Predicative Analysis. (shrink)

In this article we show how to use the result in Jäger and Probst [7] to adapt the technique of pseudo-hierarchies and its use in Avigad [1] to subsystems of set theory without foundation. We prove that the theory KPi0 of admissible sets without foundation, extended by the principle (Σ-FP), asserting the existence of fixed points of monotone Σ operators, has the same proof-theoretic ordinal as KPi0 extended by the principle (Σ-TR), that allows to iterate Σ operations along ordinals. By (...) Jäger and Probst [6] we conclude that the metapredicative Mahlo ordinal φ ω00 is also the ordinal of KPi0+(Σ-FP). Hence the relationship between fixed points and iteration persists in the framework of set theory without foundation. (shrink)

We give a broad discussion of reflection principles in explicit mathematics, thereby addressing various kinds of universe existence principles. The proof-theoretic strength of the relevant systems of explicit mathematics is couched in terms of suitable extensions of Kripke–Platek set theory.

In this paper we introduce theories of universes in analysis. We discuss a non-uniform, a uniform and a minimal variant. An analysis of the proof-theoretic bounds of these systems is given, using only methods of predicative proof-theory. It turns out that all introduced theories are of proof-theoretic strength between Γ0 and ϕ1ɛ00.

In this paper, we study a concept of universe for a truth predicate over applicative theories. A proof-theoretic analysis is given by use of transfinitely iterated fixed point theories . The lower bound is obtained by a syntactical interpretation of these theories. Thus, universes over Frege structures represent a syntactically expressive framework of metapredicative theories in the context of applicative theories.