Page 72 - Textos de Matemática Vol. 38

64 PETER KOEPKE
We are now able to canonically interpret the theory ZFC within SO. Theorem 7.2. (SO) = (, ≡, ◭) is a model of ZFC.
Proof. (1) The axiom of extensionality holds in :
∀x∀y(∀z(z ◭ x ↔ z ◭ y) → x ≡ y).
Proof . Consider points x and y such that ∀z(z ◭ x ↔ z ◭ y). Consider u Rx x. Then (u,Rx) ◭ (x,Rx) = x. By assumption, (u,Rx) ◭ (y,Ry). By definition take v Ry y such that (u,Rx) ≡ (v,Ry). Thus
∀uRx x∃vRy y(u,Rx)≡(v,Ry). By exchanging x and y one also gets
∀vRy y∃uRx x(u,Rx)≡(v,Ry).
Hence x ≡ y.
(2) The axiom of pairing holds in :
qed(1)
∀x∀y∃z∀w(w ◭ z ↔ (w ≡ x ∨ w ≡ y)).
Proof. Consider points x = (x,Rx) and y = (y,Ry). By the comprehension
Lemma 7.1 there is a point z = (z,Rz) such that for all points w w ◭ z ↔ (w ≡ x ∨ w ≡ y).
(3) The axiom of unions holds in :
∀x∃y∀z(z ◭ y ↔ ∃w(w ◭ x ∧ z ◭ w)).
qed(2)
Proof. Consider a point x = (x,Rx). Let A = {i ∈ dom(Rx)|∃u ∈ dom(Rx) i Rx u Rx x}. For i ∈ A define the point xi = (i, Rx). By the comprehension lemma 7.1 there is a point y = (y,Ry) such that for all points z
z ◭ y ↔ ∃i ∈ Az ≡ xi.
To show the axiom consider some z ◭ y. Take i ∈ A such that z ≡ xi. Take u ∈ dom(Rx) such that iRxuRxx. Then z≡xi =(i,Rx) ◭ (u,Rx) ◭ (x,Rx) = x, i.e., ∃w(z ◭ w ◭ x).
Conversely assume that ∃w(z ◭ w ◭ x) and take w such that z ◭ w ◭ x. Take uRx x such that w ≡ (u,Rx). Then z ◭ (u,Rx). Take iRx u such that z ≡ (i,Rx) = xi. Then z ◭ y. qed(3)
(4) The replacement schema holds in , i.e., for every first-order formula φ(u, v) in the language of ≡ and ◭ the following is true in :
∀u,v,v′((φ(u,v)∧φ(u,v′)) → v ≡ v′) → ∀x∃y∀z(z ◭ y ↔ ∃u(u ◭ x∧φ(u,z))).