Page 68 - Textos de Matemática Vol. 38

60 PETER KOEPKE
Definition 5.3. For sets or classes R, X, Y, f define the following notions in SO:
∅ := dom(R) := ran(R) := fun(f) := f:X→Y := α=f(β) := αRβ := X×Y := X↾Y :=
ι0
{α|∃β((α, β) ∈ R)}
{β|∃α((α, β) ∈ R)} ∀α,β1,β2((α,β1)∈f∧(α,β2)∈f→β1 =β2) fun(f)∧dom(f)=X∧ran(f)⊂Y
(α,β)∈f
(α,β)∈R
{γ|G1(γ)∈X∧G2(γ)∈Y} {(α,β)∈X|α∈Y}
The axioms of SO imply that these notions have their usual basic proper- ties. We can now prove transfinite induction and recursion in SO.
Theorem 5.4. (SO) Let φ(α,X1,...,Xn) be an LSO-formula. Then for all X1,...,Xn,
implies
∀α((∀β < αφ(β,X1,...,Xn)) → φ(α,X1,...,Xn)) ∀αφ(α,X1,...,Xn)
Proof. Otherwise, by (WO), there would be a minimal counterexample α, contradicting the assumption. ✷
Theorem 5.5. (SO) Let R : On × SOn → On be a function defined by some for- mula φ(α, f, β, X1, . . . , Xn). Then there exists a unique function F : On → On defined by a formula ψ(α,β,X1,...,Xn) such that
∀α(F (α) = R(α, F ↾ ια)) (5.2)
Proof. This is proved similar to the recursion theorem in ZF: We define the notion of approximation functions which are set-functions defined on proper initial segments of Ord, satisfying (5.2) on their domain. Then we obtain F as the union of all of these approximation functions. ✷
As in ZF this result can be generalized from the relation < to arbitrary set-like well-founded relations.
Using Go¨del-pairing one can also formalize ordered pairs of an ordinal α and a set z by
(α, z) = {G(α, β)|β ∈ z}.
One could now develop further mathematical notions - numbers, spaces, first- order syntax and semantics — in SO much the way as one does in standard set theory.