Page 131 - Textos de Matemática Vol. 40

3.4. Universes over Frege structures 119
the following Proposition in a readable way, we need some abbreviations; how- ever, they are chosen in analogy to the definition of IDα in Section 1.5.3. We
will use the usual short hand notation for pairing and projection, i.e., (t,s) for (p t s), (t)0 for (p0 t), and (t)1 for (p1 t). Let tβ s be an abbreviation of t (s, β) and t≺β r of ((t r) ∈˙ univ (r)1) ∧˙ ((r)1 ≺˙ β). To deal with the negative occur- rences of Q, sometimes we use the notation φ(P, Q, ¬Q, x, y) where the second argument stands for the positive occurrences of Q, while the third indicates the negative ones.
Proposition 3.4.13. If φ(P,Q,x,y) is an inductive operator form, then there exists a term tφ of LU such that
FSU + TI(α, T(f ·)) ⊢ ∀β ≺ α.∀x.T(tφβ x) ↔ φ(T(tφβ ·), T(tφ≺β ·), x, β).
Proof. Given an inductive operator form φ(P, Q, x, y), we choose fresh variables u and z not occurring in φ(P, Q, x, y). z is the variable for the fixed point term which will be defined by the Recursion Theorem, and u stands for its argument. Thus, it will often be decomposed into two components, (u)0 for the “real” argument and (u)1 for the level of iteration. Now we do the following replacements in the formula φ(P, Q, ¬Q, x, y):
• the variable x is replaced by (u)0,
• the variable y is replaced by (u)1,
• all occurrences of P (t) are replaced by T(z (t, (u)1)),
• the positive occurrences of Q(s) are replaced by z s ∈ univ (s)1 ∧ (s)1 ≺ (u)1 ,
• the negative occurrences of ¬Q(r) are replaced by (zr ̸∈˙ univ(r)1) ∈ univ (u)1 ∨ ¬((r)1 ≺ (u)1).
The last clause is crucial, since under the reflection of the statement z r ̸∈ univ (r)1 in the universe univ (u)1 the formula will become T-positive.
Thus, the whole formula abbreviated by φ(z, u) reads
φ(T(z (·, (u)1)),
z·∈univ(·)1 ∧(·)1 ≺(u)1,
(z · ̸∈˙ univ (·)1) ∈ univ (u)1 ∨ ¬((·)1 ≺ (u)1), (u)0, (u)1).