Page 137 - Textos de Matemática Vol. 40

3.4. Universes over Frege structures
3. For a limit ordinal β, Zβ is the least fixed point of Φ(X,
Iterating this sequence up to the first recursively inaccessible ordinal ι we get a model Iι of FSU + (LU -IN). (For the notion of recursively inaccessible or- dinal, and admissible ordinal used below, we refer to the standard literature, e.g., [Bar75, Hin78].) The construction and proof are analogous to the corre- sponding model Cι of TLR by Cantini, cf. [Can96, Theorem 39.16]. T(t) can be interpreted in Iι by ∃γ < ι.t ∈ Zγ, and U(t) by ∃β < ι.∃b.t = lb∧∀x.bx ∈ Zβ ∨ ¬˙ (b x) ∈ Zβ . In the verification that Iι is a model, consistency follows directly from the leastness of the fixed points. The only complicated case is for the limit axioms, whereby we obtain the premiss
Iι |=∀x.∃γ.fx∈Zγ ∨¬˙ (fx)∈Zγ.
As in the proof of Theorem 39.16 of [Can96] one can check that this formula can be rewritten as a Σ1 formula. Σ1-reflection, available in Lι, the constructible hierarchy up to ι, allows to conclude
Iι |= ∃δ∀x.f x ∈ Zδ ∨ ¬˙ (f x) ∈ Zδ.
One can easily check that lf will be a universe in Zδ+1 “reflecting” f. To find δ, ι has to be at least admissible and because this can be iterated, ι has to be a limit of admissibles, i.e., recursively inaccessible.
¿From the definition of Φ it is already clear, that Iι will also satisfy the axiom of linearity of universes (U-Lin), and therefore also (U-Dir), as well as (U-Nor). In fact, we could even demand that the hierarchy of universes is well- founded. However, while the former axioms will not change the proof-theoretic strength, this is not obvious for an axiom stating the well-foundedness of the universes.
To determine the proof-theoretic upper bounds of FSU we have to work with much shorter sequences. But, we have to integrate consistency into the fixed points. A set X is called a consistent fixed point of Φ, if it is a fixed point ofΦandforallelementsa,¬(a∈X∧¬˙a∈X)holds. Wecallasequenceof sets (Xβ ), for β ≤ α, a Φ+ sequence if the following conditions hold:
1. X0 is a consistent fixed point of Φ(X, ∅, x, 0),
2. Xβ+1 is a consistent fixed point of Φ(X, Xβ , x, β + 1),
3. For a limit ordinal β, Xβ is a consistent fixed point of Φ(X,
We define partial models M(α) of FSU by use of a Φ+ sequence (Xβ)β≤α. Given the interpretation of TON extended by the new constants, we need to interpret the predicates T and U. We translate the truth predicate T(t) by
t ∈ Xα
γ<β
125 Xγ , x, β).
γ<β
Xγ , x, β).