Page 133 - Textos de Matemática Vol. 40

3.4. Universes over Frege structures 121 where t(φN) is given as in Proposition 3.4.13. Using this Proposition, the
β
verification of the fixed point axiom of IDα in FSU + TI(α, T(f ·)) is obvi- ous. The induction principle of IDα can be verified by (LU-IN). Moreover, in FSU + TI(α + 1, T(f ·)) we can use (C-IN ) for this verification, since the (trans- lations of) formulae containing (possibly negative) occurrences of fixed points up to level α can be rewritten as classes by use of the universe univ (α + 1). So we have:
Proposition 3.4.14. For each ordinal α less than ε0, it holds that: 1. IDα ⊢φ ⇒ FSU+TI(α,T(f·))+(LU-IN)⊢φN,
2. IDα ⊢φ ⇒ FSU+TI(α+1,T(f·))+(C-IN)⊢φN.
Therefore we get, together with Proposition 3.4.12, the following embed- dings for the limit cases:
Proposition 3.4.15. There exists a translation ·N from the language Lfix into the language LU such that
1. ID<ω ⊢φ ⇒ FSU+(C-IN)⊢φN, 2. ID<ωω ⊢φ ⇒ FSU+(T-IN)⊢φN, 3. ID<ε0 ⊢φ ⇒ FSU+(LU-IN)⊢φN.
All three embeddings preserve arithmetical sentences.
3.4.6 The upper bounds
The proof of the upper bounds follows a well-known procedure. First we de- fine a Tait calculus for FSU which allows us to prove partial cut elimination up to T+/T− formulae, which we define below. Then, we introduce partial models of FSU by use of an appropriate inductive operator form which can be formalized in IDα. As for FON we have to extend these theories slightly to deal with consistency. The partial models can be used to give an asym- metric interpretation of our theories. This procedure is well-known from the literature, cf. e.g., [Sch77, J¨ag80, J¨ag84, Can85, Can86] and especially Can- tini [Can89, Can96] for truth theories or Glaß, Marzetta and Strahm [Gla93, Gla95, GS96, Mar93, Mar94, MS98, Str99] for explicit mathematics.
A Tait calculus for FSU. For the proof-theoretic treatment, we replace our Hilbert-style calculus by a Tait-style calculus, [Tai68]. We dispense of logic with negation and start only from the connectives ∧, ∨ and quantifiers ∀ and ∃. Additionally, we extend the language LU with new relation symbols
• N,=,T and U