Page 83 - Textos de Matemática Vol. 40

2.3. Universes in explicit mathematics 71
[Set98]. The proof-theoretic investigation of these theories led to the defini- tion of (iterated) fixed point theories ID1 and IDn by Aczel and Feferman, [Acz77, Fef82].
In the framework of explicit mathematics, universes have first been con- sidered by Feferman [Fef82] in connection with Hancock’s conjecture and by Marzetta [Mar93, Mar94] for designing an explicit analog of Friedman’s theory ATR0 and Ja¨ger’s theory KPl0 of iterated admissible sets without foun- dation (cf. e.g., Ja¨ger [J¨ag84, J¨ag86]).
More about universes in explicit mathematics may be found, for example, in Ja¨ger and Strahm [JS01] and Strahm [Str99], always in connection with theories of predicative or metapredicative strength. Universes are also impor- tant for dealing with Mahloness in explicit mathematics, as shown in the paper Ja¨ger and Studer [JS02b]. In the following Chapter we will also investigate universes for a truth theory over applicative theories, which results in theories of (meta)predicative strength.
In the following we study universes in explicit mathematics leading to the- ories of impredicative strength. This is achieved on the one hand by a leastness condition for universes, on the other hand by adding name induction. In both cases the possibility to prove the principle of inductive generation is crucial. Thus, the theories turn out to be proof-theoretically equivalent to Feferman’s T0 (see Section 2.3.2).
2.3.1 The limit axiom and basic properties of universes
Universes. Now we are going to introduce universes in explicit mathematics. In short, a universe is a type U with: (i) U is closed under elementary compre- hension and join; (ii) all elements of U are names. This second condition (ii) is crucial to avoid universes from being trivial since otherwise, for example, the universal type V = {x : x = x} could act as the topmost universe.
In order to give the definition of universe in greater detail, we introduce some auxiliary notation. First, we use the closure condition C(φ,a) defined in Section 2.2.1 but for the special case that φ(x) is of the form x ∈ S. Therefore, let C(S,a) be the disjunction of the following LEM formulae:
(1) a=nat∨a=id,
(2) ∃x.a=co(x)∧x∈S,
(3) ∃x,y.a=int(x,y)∧x∈S∧y∈S,
(4) ∃x.a=dom(x)∧x∈S,
(5) ∃f,x.a=inv(f,x)∧x∈S,
(6) ∃x,f.a=j(x,f)∧x∈S∧∀y∈˙ x.fy∈S.