Page 69 - Textos de Matemática Vol. 38

ORDINALS, COMPUTATIONS, AND MODELS OF SET THEORY 61
6 Assembling sets along wellfounded relations
In standard set theory a set x can be represented as a point in a well- founded relation: consider the ∈-relation on the transitive closure TC({x}) with distinguished element x ∈ TC({x}). By the Mostowski isomorphism theorem x is uniquely determined by the pair (x, TC({x})) up to order isomorphism.
By the previous section, ordered pairs and wellfounded relations can be handled within the theory SO. So assume SO for the following construction. We shall eventually define a model of ZFC within SO.
Definition 6.1. An ordered pair x = (x,Rx) is a point if Rx is a wellfounded relation on ordinals and x ∈ dom(Rx). Let be the class of all points. Unless specified otherwise we use Rx to denote the wellfounded relation of the point x.
Note that according to our previous considerations one can reasonably define the class in SO as well as in ZFC. In ZFC, (x,∈↾ TC({x})) is a point. Conversely, again in ZFC, any point x = (x,Rx) can be interpreted as a standard set I(x): Define recursively
Ix : dom(Rx) → V , by Ix(u) = {Ix(v)|v Rx u}.
Then let I(x) = Ix(x) be the interpretation of x. Note that for points x and y
Ix(u) = Iy(v)
iff {Ix(u′)|u′ Rx u} = {Ix(v′)|v′ Ry v}
iff (∀u′ Rx u∃v′ Ry vIx(u′) = Iy(v′)) ∧ (∀v′ Ry v∃u′ Rx uIx(u′) = Iy(v′)).
This means that the relation Ix(u) = Iy(v) in the variables u and v can be defined recursively without actually forming the interpretations Ix(u) and Iy(v).
Hence this relation can be defined in SO.
Definition 6.2. Define a relation ≡ on points x = (x,Rx),y = (y,Ry) by induc-
tion on the product wellorder Rx × Ry : (x,Rx) ≡ (y,Ry)
iff ∀uRx x∃vRy y(u,Rx)≡(v,Ry)∧∀vRy y∃uRx x(u,Rx)≡(v,Ry).
Lemma 6.3. (SO) ≡ is an equivalence relation on .
Proof. Reflexivity. Consider a point x = (x,Rx). We show by induction on Rx that for all u ∈ dom(Rx) holds (u,Rx) ≡ (u,Rx). Assume that the claim holds for all v Rx u. Consider some v Rx u. By the inductive assumption, (v, Rx) ≡ (v, Rx). This implies
∀vRx u∃wRx u(v,Rx)≡(w,Rx).