Page 127 - Textos de Matemática Vol. 40

3.4. Universes over Frege structures 115
Lemma 37.7.(i)]. In FSU the limit axiom together with the definition of ` is sufficient to establish the corresponding result.
In the definition of the theory we have used a pure axiomatization of the notion of universes. Alternatively, it is possible to introduce this notion as an abbreviation, as we have done it for universes in explicit mathematics, cf. Sec- tion 2.3. As we saw, in this case one has to be careful with the possible ordering principles. So, for instance, linearity of the universes can only be demanded for normal universes, i.e., universes generated (named) by the limit operation. The axiomatization, instead, allows to restrict the totality of universes. The model construction given below will even verify that every universe is normal in the following sense:
(U-Nor) U(u) → ∃f.C(f) ∧ u = l f.
Our theory FSU shares the main features of Cantini’s theory TLR as described in [Can96, Chapter 8]. It is just a matter of routine to check that we can prove the features of TLR analogously in FSU. One has to inspect only the use of directedness which is built into TLR and a part of the soundness axioms of TLR which are not available in FSU. The following applications, which show some of the main results about TLR and FSU, carry over without further requirements.
First, the embedding of explicit mathematics within FON can be extended to “its” concept of universes as we discussed it in the previous Chapter, cf. [Can96, §38]. However, since the universes considered here are not “least”, we can relate them only with the metapredicative versions of universes in explicit mathematics studied by Strahm [Str99]. He gives a proof-theoretic analysis of the theories EMU0, EMU0 + (Σ+−IN), and EMU which match in strength with FSU + (C-IN), FSU + (T-IN), and FSU + (LU -IN), respectively. But, in contrast to the theories of universes in explicit mathematics, FSU allows a syntactical embedding of (transfinitely) iterated fixed point theories IDα, in analogy to the embedding of ID1 within FON + (LFt -IN).
Secondly, there is an embedding of the theory ATR0 within FSU + (C-IN), cf. [Can96, §40]. It has been shown that an important part of mathematics can be formalized in ATR0, cf. [Sim99, Chapter V]. From the embedding it follows that this also holds for FSU + (C-IN).
Finally, truth theories allow a better inspection of set- and truth-theoretical paradoxes, in contrast to the theories of explicit mathematics. For instance, we can formalize the Russell “set” {x|x ̸∈ x}. According to our abbreviations it reads as the term r := λx.x ̸∈˙ x = λx.¬˙ (x x). As for the “liar” used in the proof of Lemma 3.1.1, we get that FON ⊢ ¬P(r r). Now, we consider in addition the Russell set relativized to a universe: Let r be defined as λu, x.¬˙ (u (x x)). Thus, wehaveru={x|(x∈˙ x)̸∈u}. Ifwewriteru forruwegetruru =¬˙(u(ruru)). As for FON we get that ru ru cannot be a class relative to a universe u:
Lemma3.4.6. FSU⊢U(u)→¬(ruru ∈u∨¬˙(ruru)∈u).