Page 139 - Textos de Matemática Vol. 40

3.4. Universes over Frege structures 127 These bounds remain unchanged even if we strengthen FSU by (U-Lin) or (U-Nor).
Proof. In all three cases, the proof is by induction on the length of the derivation in the Tait calculus. For the verification of (C-IN )T and (T-IN )T , we follow closely the procedure of Cantini in [Can89], cf. also [Can96]. In the following for brevity we drop the indices ⃗x and ⃗n.
1. FSUT + (C-IN )T . Induction base. If k = 0, then one element of Γ is an axiom. Of course, the logical axioms and the axioms from TON are satisfied. From the axioms of FSU we will check the basic ones, the closure for universal quantification, the order axiom and the limit axioms.
(1) Γ, U(s), T(s t) ∨ T(¬˙ (s t)).
Let l < m be minimal such that Ul+1(s) holds. Now by case distinction on Tl(t)∨¬Tl(t) we get from clauses 11 and 12 Tl+1(st)∨Tl+1(st). Finally, persistence yields Tm+1(s t) ∨ Tm+1(s t).
(2) Γ, U(s), T(s t), T(t).
Let l < m be minimal such that Ul+1(s) and Tl+1(s t) hold. By clause 11
we get Tl(t) and persistence yields Tm+1(t).
(10a) Γ, U(s), (∃x.T(s (t x))), T(s (∀˙ t)).
Let l < m be minimal such that Ul+1(s) and Tl+1(s(tc)) hold for all c. Clause 11 yields Tl(tc) for each c. By clause 9 we have Tl(∀˙ t) and, again by 11, Tn(s(∀˙ t)). Persistence finally yields Tm+1(s(∀˙ t)).
Note that for the adaptation of this step into the transfinite, it is important that we form universes on successor levels only. Otherwise, we could not find one fixed level on which T(tc) holds for all c.
(10b) Γ, U(s), T(s (∀˙ t)), ∀x.T(s (t x)).
Let l < m be minimal such that Ul+1(s) and Tl+1(s(∀˙ t)). By clause 11 we have Tl(∀˙ t) and by 9 Tl(t c) for all c. Thus, by clause 11 we have Tl+1(s (t c)) for each c and together with persistence ∀x.Tm+1(s (t x)).
(12) Γ, U(r), U(s), T(s (r t)), T(s t).
Let l < m be minimal such that Ul+1(s) and Tl+1(s (r t)). By clause 11 we get Tl(r t) and let k ≤ l be minimal such that Tk(r t). On the other hand, there is a minimal n < m such that Un+1(r), i.e., ∃b.r = lb∧Cn(b). Therefore, according to clause 11 Tk (r t) can become true only if k = n+1. Thus, we have Un+1(r) and Tn+1(r t) for n + 1 < l and clause 11 yields Tn(t). By persistence we have Tl(t) and, since Ul+1(s) holds, we get Tl+1(st). Finally, persistence yields Tm+1(st).
(13) Γ, U(s), T(s t), T(s (¬˙ t)).