Construction of a model of Peano Arithmetic I'm studying the axioms of Zermelo-Frankel Set Theory at the moment. I already know the following six axioms:


*

*The axiom of empty set

*The axiom of extensionality

*The axiom of pairing

*The axiom of infinity

*The axiom schema of separation

*The axiom of power set


In the lecture we wanted to construct a model of peano arithmetic on $\omega$ just using the above axioms. We started as follows (the language of Peano Arithmetic is $\mathcal{L}_{PA}=\{0,s,+,\cdot\}$):
$$0^\mathbb{N}:=\emptyset$$
$$s^\mathbb{N}:=\{\langle n,m \rangle\in \omega\times \omega\mid m=n \cup \{n\}\} $$
$$+^\mathbb{N}:=\bigcup\{a\in\mathcal{P}((\omega\times\omega)\times\omega)\mid\varphi(a)\}, $$
where $$\varphi(a)\equiv \forall x\in \omega (\langle \langle x,\emptyset\rangle,x\rangle\in a) \land \forall x\forall y\forall z\forall z'(\langle \langle x,y\rangle,z\rangle\in a\land \langle \langle x,y\rangle,z'\rangle\in a \rightarrow z=z')$$
Why does the following hold?
$$\forall x\forall y(x+^\mathbb{N}s^\mathbb{N}(y)=s^\mathbb{N}(x+^\mathbb{N}y))$$
Is the definition of $+^\mathbb{N}$ correct? Because even in "simple" cases like $y=\emptyset$ and $x\in\omega$ I don't know what $x+^\mathbb{N}y$ is.
Edit: I thought about my question again and I agree that there's something wrong with the definition of $+^\mathbb{N}$. Here are my thoughts:
Lets define 
$$+^\mathbb{N}:=\bigcap\{a\in\mathcal{P}((\omega\times\omega)\times\omega)\mid\varphi(a)\}, $$
where $$\varphi(a)\equiv \forall x\in \omega (\langle \langle x,\emptyset\rangle,x\rangle\in a) \land \forall x\forall y\forall z\forall z'(\langle \langle x,y\rangle,z\rangle\in a\land \langle \langle x,y\rangle,z'\rangle\in a \rightarrow z=z')\land \forall x\forall y\forall z (\langle\langle x,y\rangle,z\rangle \in a \rightarrow \langle\langle x, s^\mathbb{N}(y)\rangle, z\cup \{z\}\rangle \in a)$$
Now I want to prove that $+^\mathbb{N}$ is functional. Therefore let $x,y\in \omega$. If $y=\emptyset$ then $\langle\langle x,y\rangle,x\rangle\in +^\mathbb{N}.$  So assume now that $y\neq \emptyset.$ But then by definition of $\omega$, $y$ is a successor ordinal. So $y=k\cup \{k\}$. If there is a $z_1\in \omega$ such that $\langle\langle x,k\rangle,z_1\rangle\in a$, then $\langle\langle x,y\rangle,z_1\cup \{z_1\}\rangle\in a.$ But if $k\neq \emptyset$, $k$ is again a successor ordinal, etc... We can do that until we get to the empty set. (I'm really not sure about that. I'm still a little bit confused by the definition of the natural numbers.)  Uniqueness of the sum of two numbers $x,y\in \omega$ is clear by the condition 
$$ \forall x\forall y\forall z\forall z'(\langle \langle x,y\rangle,z\rangle\in a\land \langle \langle x,y\rangle,z'\rangle\in a \rightarrow z=z').$$
 A: The revised $\varphi$ looks good: $\varphi(x)$ now specifies that $x$ satisfies the minimum requirements to be what we want, and intersecting all such sets ought to cut out all of the extraneous elements. However, your argument that $+^{\Bbb N}$ is functional definitely needs work.
Fix $x\in\omega$. Let 
$$B_x=\left\{y\in\omega:\exists u,v\in\omega\left(u\ne v\land\big\langle\langle x,y\rangle,u\big\rangle,\big\langle\langle x,y\rangle,v\big\rangle\in+^{\Bbb N}\right)\right\}\;,$$
and suppose that $B_x\ne\varnothing$. Let $m=\min B_x$, and suppose first that $m=0$. Then there is an $n\in\omega$ such that $\big\langle\langle x,0\rangle,n\big\rangle\in+^{\Bbb N}$ and $n\ne x$. Let 
$$a=\left(+^{\Bbb N}\right)\setminus\left\{\big\langle\langle x,0\rangle,n\big\rangle\right\}\;;$$
then $\varphi(a)$, so $+^{\Bbb N}\subseteq a\subsetneqq+^{\Bbb N}$, which is absurd. Thus, $m>0$, and therefore $m=s^{\Bbb N}(k)$ for some $k\in\omega$. 
A similar argument works for this case. By the choice of $m$ there is a unique $\ell\in\omega$ such that $\big\langle\langle x,k\rangle,\ell\big\rangle\in+^{\Bbb N}$, but there is an $n\in\omega$ such that $\big\langle\langle x,m\rangle,n\big\rangle\in+^{\Bbb N}$ and $n\ne \ell\cup\{\ell\}$. We can again let
$$a=\left(+^{\Bbb N}\right)\setminus\left\{\big\langle\langle x,m\rangle,n\big\rangle\right\}\;,$$
and we get exactly the same contradiction as in the case $m=0$. It follows that $B_x=\varnothing$ and hence that for each $y\in\omega$ there is a unique $u\in\omega$ such that $\big\langle x,y\rangle,u\big\rangle\in+^{\Bbb N}$. Since $x\in\omega$ was arbitrary, we’ve shown that $+^{\Bbb N}$ is a function.
It remains to check that
$$\forall x\forall y\left(x+^\mathbb{N}s^\mathbb{N}(y)=s^\mathbb{N}\left(x+^\mathbb{N}y\right)\right)\;.$$
The idea is basically the same. Fix $x\in\omega$, and let
$$B_x=\left\{y\in\omega:x+^{\Bbb N}s^{\Bbb N}(y)\ne s^{\Bbb N}\left(x+^{\Bbb N}y\right)\right\}\;.$$
Assume that $B_x\ne\varnothing$, let $m=\min B_x$ and use the definition of $+^{\Bbb N}$ to derive a contradiction. This is very much like what I did above to show that $+^{\Bbb N}$ is a function, so I’ll give you a crack at it first; if you get stuck, leave a comment, and I’ll fill it in.
