ZF Natural Even Numbers

Question

Regarding $\Bbb N$ as constructed using ZF ($0=\emptyset, n+1=n^+=n\cup\{n\}$), how is the property "divisible by 2" expressed (using sets and logic)?

Answer 1

We can define addition and multiplication on the natural numbers as defined. $m+n$ is defined to be the unique $k$ such that there is a bijection between $k$ and $m\times\{0\}\cup n\times\{1\}$. Similarly $m\cdot n=k$ when $k$ is the unique natural number such that $m\times n$ has a bijection with $k$.

Now we can say that $\exists k(k+k=n)$.

Answer 2

Well, one way to go about it is to define arithmetic on $\Bbb N,$ explicitly or by recursion. Then we define evenness in the usual way.

Alternatively (and a bit more cumbersomely), define $f:\Bbb N\to\Bbb N$ by $f(n)=(n^+)^+.$ Now, given any $n\in\Bbb N,$ define $f^0(n)=n,$ and define $f^{m+1}(n)=f\bigl(f^m(n)\bigr).$ By recursion, we have that $f^m:\Bbb N\to\Bbb N$ for all $m\in\Bbb N.$ We can then say that $n$ is even if and only if $n=f^m(0)$ for some $m\in\Bbb N.$