Page 74 - Textos de Matemática Vol. 38

66 PETER KOEPKE
We claim that ((δ,ξ),Ry) ≡ c and thus c ◭ y.
Consider β Ry (δ,ξ). By the definition of Rywe have (β,ξ) ∈ P and so
β ∈ z. By the definition of z choose vRcc such that (v,Rc) ≡ (β,Rx) ≡ (β,Ry). Conversely, consider vRcc. Then (v, Rc) ◭ (c, Rc) = c. The subset property implies (v,Rc) ◭ (x,Rx) = x. Take βRxx such that (v,Rc) ≡ (β,Rx) ≡ (β,Ry). By definition, β ∈ z, (β,ξ) ∈ P and β Ry (δ,x). qed(5)
(6) The axiom of choice holds in :
∀x((∀y, z((y ◭ x ∧ z ◭ x) → (∃uu ◭ y ∧ (¬y ≡ z → ¬∃u(u ◭ y ∧ u ◭ z))))) →
∃w∀y(y ◭ x → ∃u((u ◭ w ∧ u ◭ y) ∧ ∀v((v ◭ w ∧ v ◭ y) → u ≡ v)))). Proof . Let x = (x, Rx) ∈ be a point such that
∀y, z((y ◭ x ∧ z ◭ x) → (∃uu ◭ y ∧ (¬y ≡ z → ¬∃u(u ◭ y ∧ u ◭ z)))). Choose an ordinal α ∈ dom(Rx) and define the point w = (α,Rw) by letting its
“elements” be least ordinals in the “elements” of x:
Rw =Rx∪{(ξ,α)|∃ζ(ξRxζRxx∧(∀ξ′ <ξ∀ζ′((ζ,Rx)≡(ζ′,Rx)→¬(ξRxξ′Rxζ))))}.
To show that w witnesses the axiom of choice for x consider a point y with y ◭ x. We may assume that y is of the form y = (ζ,Rx) where ζ Rx x. By the assumption on x there exists u ◭ y. Take some ξ such that (ξ,Rx) ≡ u. We may assume that ζ and ξ with these properties are chosen so that ξ is minimal in the ordinals. Then
ξRx ζRx x∧(∀ξ′ <ξ∀ζ′((ζ,Rx)≡(ζ′,Rx)→¬(ξRx ξ′ Rx ζ))) (7.3)
and so ξRw α. Thus u ◭ w. To show the uniqueness of this u with u ◭ w∧u ◭ y consider some v with v ◭ w∧v ◭ y. We may assume that v is of the form v = (ξ′,Rw) with ξ′ Rw α. By the definition of Rw we choose some ζ′ such that
ξ′ Rx ζ′ Rx x ∧ (∀ξ′′ < ξ′∀ζ′′((ζ′, Rx) ≡ (ζ′′, Rx) → ¬(ξ′ Rx ξ′′ Rx ζ′))). (7.4) Now
v ◭ y ◭ x and v = (ξ′,Rw) ◭ (ζ′,Rw) ◭ (x,Rx) = x.
Since the “elements” of x are “pairwise disjoint”, we have y ≡ (ζ′,Rw). Since y ≡ (ζ,Rx) the conditions (2) and (3) become equivalent and define the same ordinal ξ = ξ′. Hence
u ≡ (ξ,Rx) ≡ (ξ′,Rw) ≡ v.
(7) The foundation schema holds in , i.e., for every first-order formula
φ(u) in the language of ≡ and ◭ the following is true in : ∃uφ(u) → ∃y(φ(y) ∧ ∀z(z ◭ y → ¬φ(z)).
qed(6)