Page 71 - Textos de Matemática Vol. 38

ORDINALS, COMPUTATIONS, AND MODELS OF SET THEORY 63
Similarly
and thus (u,Rx) ≡ (w,Rz). In particular for x = (x,Rx), y = (y,Ry) and
z = (z,Rz)
∀w′ Rz w∃u′ Rx u(u′,Rx) ≡ (w′,Rz) x ≡ y ∧ y ≡ z → x ≡ z.
We now define a membership relation for points.
Definition 6.4. Let x = (x,Rx) and y = (y,Ry) be points. Then set
x ◭ y iff ∃v Ry yx ≡ (v,Ry).
Lemma 6.5. (SO) The equivalence relation ≡ is a congruence relation with
respect to ◭, i.e.,
x ◭ y ∧ x ≡ x′ ∧ y ≡ y′ → x′ ◭ y′.
Proof. Letx◭y∧x≡x′∧y≡y′ →x′ ◭y′.TakevRyysuchthatx≡(v,Ry). By y ≡ y′ take v′Ry′ y′ such that (v, Ry) ≡ (v′, Ry′ ). Since ≡ is an equivalence relation, the equivalences x ≡ x′, x ≡ (v,Ry) and (v,Ry) ≡ (v′,Ry′) imply x′ ≡(v′,Ry′).Hencex′ ◭y′. ✷
7 The class of points satisfies ZFC
We show that the class of points with the relations ≡ and ◭ satisfies the axioms ZFC of Zermelo-Fraenkel set theory with the axiom of choice. For the existence axioms of ZFC we prove a comprehension lemma about combining points into a single point.
Lemma 7.1. (SO) Let (xi|i ∈ A) be a set-sized sequence of points. Then there is a point y = (y,Ry) such that for all points x holds
x◭y iff ∃i∈Ax≡xi.
Proof. Obviously we may substitute the xi’s by ≡-equivalent points x′i. We may thus assume that the domains of the wellfounded relations Rxi are pairwise disjoint. Take some y ̸∈ i∈A dom(Rxi ) and define the point y = (y, Ry ) by
Ry=Rxi ∪{(xi,y)|i∈A}. i∈A
Consider i ∈ A. If x ∈ dom(Rxi ) then the iterated Rxi -predecessors of x are equal to the iterated Ry -predecessors of x. Hence (x, Rxi ) ≡ (x, Ry ).
Assume now that x ◭ y. Take v Ry y such that x ≡ (v,Ry). Take i ∈ A such that v = xi. By the previous remark
x ≡ (v,Ry) = (xi,Ry) ≡ (xi,Rxi) = xi.
Conversely consider i ∈ A and x ≡ xi. Then x ≡ xi = (xi,Rxi) ≡ (xi,Ry) and xi Ry y. This implies x ◭ y. ✷