Page 122 - Textos de Matemática Vol. 40

110 Chapter 3. Truth Theories Using the translation above, in the applicative framework we get the term
fibgen satisfying the following recursion equation: fibgenxy ≃ px(λz.fibgeny(x+y)).
The stream fibs then is defined by:
fibs := fibgen 0 1.
In a suitable applicative theory now we can prove fibs ↓ and ∀x.N(x) → (nth x fibs) ↓. This would not be provable if we would replace the “pointer” (λz.fibgen y (x + y)) in the recursion equation of fibgen by the simple term fibgeny(x+y).
3.4 Universes over Frege structures
Using Aczel’s original idea by defining an element relation in terms of the truth predicate, the closure conditions of the truth levels may be read as set theoretical closure conditions for universes. In analogy to the well-know hierarchy of truth predicates, Cantini studied in [Can96] iterated truth predicates in the given context (cf. also [Can95]), which will correspond to our universes.
The definition of universes over Frege structures merges, in some sense, the ideas of universes in explicit mathematics with the concept of iterated truth predicates. In fact, our theory is closely related to Cantini’s theory of TLR of reflective truth with levels [Can96, Chapter 8]. In this theory, truth is iterated by use of levels which are represented by a special sort of index terms. In contrast, our approach uses a relation which is defined within the applicative language to iterate the concept of truth. For this reason, we stay completely within the applicative framework.
By use of a uniform limit axiom, analogous to the one for universes in explicit mathematics, we will be able to form transfinite hierarchies of uni- verses. But in contrast to our theories for explicit mathematics, we study in the following metapredicative theories, i.e., we have no leastness condition or induction principle for universes. Therefore, they are more closely related to the metapredicative theories of explicit mathematics with universes studied by Strahm, [Str99, Str01].
For our theories we get a very smooth syntactical treatment of the metapred- icative, transfinitely iterated fixed point theories IDα. In fact, the theories pre- sented here were one of the first metapredicative theories, and they have been the reason for the proof-theoretic analysis of IDα in [JKSS99].
There is one conceptional difference between the account to universes we gave in explicit mathematics and the one we will give in the context of truth
The Section on universes over Frege structures is based on [Kah03].