Page 82 - Textos de Matemática Vol. 40

70 Chapter 2. Explicit Mathematics
implies [C(χ,x)]⋆. So χ⋆(x) follows by our premiss and ψ(⟨0,x⟩) holds by the definition of ψ. If φ(ψ,z) holds and there is no x with z = ⟨0,x⟩, then ψ(z) is trivially fulfilled. Hence we conclude by the leastness condition for Pφ that ∀z.Pφ(z) → ψ(z) holds. Let z be ⟨0, x⟩, then we have Pφ(⟨0, x⟩) → ψ(⟨0, x⟩) which reads as Typ(x) → χ⋆(x). Because R(x) is interpreted as Typ(x) the Theorem is proven. ⊣
This Theorem, together with Theorem 2.2.3 and the well-known proof- theoretic equivalence of IDacc and ID , yields the final result:
11
Theorem 2.2.6. The theory NEM of explicit mathematics with name induction is proof-theoretically equivalent to ID1, and its proof-theoretic ordinal is the Bachmann-Howard ordinal ΨΩ(εΩ+1).
There was a wide variety of theories of explicit mathematics around in the literature, however, NEM is the first one with the proof-theoretic strength of ID1, the theory which may be considered as the most elementary impredicative theory in mathematics.
2.3 Universes in explicit mathematics
In some form or another, universes play an important role in many systems of set theory and higher order arithmetic, in various formalizations of constructive mathematics and in logics for computation. One aspect of universes is that they expand the set or type formation principles in a natural and perspicuous way and provide greater expressive power and proof-theoretic strength.
The general idea behind universes is quite simple: suppose that there is a formal system T given comprising certain set (or type) existence principles which are justified on specific philosophical grounds. Then it may be argued that there should also exist a collection of sets (or types)—a so-called universe— satisfying these closure conditions. This process may be iterated, thus estab- lishing stronger and stronger extensions of T .
In classical set theory this process is related to what is inherent in the usual reflection principles yielding the existence of certain large cardinals (cf. e.g., Drake [Dra74]). In theories for iterated admissible sets, admissibles act as universes and provide for recursive analogs of large cardinals (cf. e.g., Ja¨ger [J¨ag86]). The concept of universes was originally introduced by Martin-Lo¨f in his type theory, [ML84]. They are generated by specific introduction and (sometimes) elimination rules and may be regarded as the constructive ver- sions of certain regular cardinals. For more information about this approach, see Martin-Lo¨f [ML84], Palmgren [Pal98], Rathjen [Rat00] and Setzer
The Section on universes in explicit mathematics is based on [JKS01].