Page 132 - Textos de Matemática Vol. 40

120
Chapter 3.
Truth Theories
˙
Now we define tφ := rec (λz, u.φ(z, u)). So we have:
tφ (x,β)
˙
= φ(T(tφ (·, β)),
tφ · ∈ univ (·)1 ∧ (·)1 ≺ β,
(tφ·̸∈˙ univ(·)1)∈univβ∨¬((·)1 ≺β),
x,β)
φφφ˙
= φ(T(tβ ·), T(t≺β ·), (t · ̸∈˙ univ (·)1) ∈ univ β ∨ ¬((·)1 ≺ β), x, β).
¿From the assumption β ≺ α, we get with Lemma 3.4.11 that U(univ β) holds. Now, ∀x.T(tφβ x) ↔ φ(T(tφβ ·), T(tφ≺β ·), x, β) follows by straightforward induc- tion on the construction of φ. The only cases to check are the negative oc- currences of T(tφ≺β ·). So we have to show the equivalence of ¬T(tφ≺β r) with
˙ T((tφ r ̸∈˙ univ (r)1) ∈ univ β ∨ ¬((r)1 ≺ β)):
˙ T((tφ r ̸∈˙ univ (r)1) ∈ univ β ∨ ¬((r)1 ≺ β))
↔ (tφr̸∈˙ univ(r)1)∈univβ∨¬((r)1 ≺β)
↔ ((r)1 ≺ β) → (tφ r ̸∈˙ univ(r)1) ∈ univβ
↔ ((r)1 ≺β)→tφr̸∈univ(r)1
↔ ¬(tφr∈univ(r)1)∨¬((r)1 ≺β)
˙
↔ ¬(T(tφ r ∈˙ univ (r)1)) ∧ T((r)1 ≺ β))
˙
↔ ¬T((tφ r ∈ univ (r)1) ∧ ((r)1 ≺ β))
↔ ¬ T ( t φ≺ β r ) . ⊣
3.4.5 Embeddings of IDα
To determine the proof theoretic lower bounds of the theories of universes over Frege structures, we will interpret iterated fixed point theories IDα in FSU plus
the different induction principles. As for FON, we have to stress the fact that we not only have a proof-theoretic reduction, but a syntactical interpretation which shows the expressive power of our theories.
To embed the IDα theories within FSU, we extend the standard interpre- tation ·N of PA in TON by setting
(Pφ(s))N := T(t(φN ) (sN )) ββ