The axiom of foundation, combined with extensionality, pair set and sum set,
tells us there is a definable operation of sets, $s\left(x\right)=x\cup \left\{x\right\}$,
called the *successor* operation which is 1-1 and does not contain
$0$ (i.e. $\varnothing $) in its range.

Definition.

A set $x$ is *inductive* if
$0\in x$ and $\forall y\in x\u200as\left(y\right)\in x$.

An inductive set is therefore infinite.

**Axiom of infinity:** there is an inductive set,
$\exists x\u200a(0\in x\wedge \forall y\in x\u200as\left(y\right)\in x)$.

The axiom says there is one such inductive set, but in fact we can find a very special one, the least such.

Proposition.

If $x,y$ are inductive then so is $x\cap y=\{u\in x:u\in y\}$.

**Proof.**

Easy exercise.

Definition.

If $x$ is a non-empty set, $\bigcap x$ denotes $\{u:\forall y\in x\u200a(u\in y)\}$. This is easily seen to be a set by separation as for any $z\in x$ we have $\bigcap x=\{u\in z:\forall y\in x\u200a(u\in y)\}$.

Definition.

Let $x$ be inductive. The set $\omega $ is the set $\bigcap \{u\subseteq x:u\text{is inductive}\}$. This is a set by power set and separation, and is independent of the choice of $x$ by the previous proposition. We also see that $\omega $ is definable by a formula of ${L}_{\in}$, $u=\omega $ holds if and only if $\forall x\u200a(x\text{is inductive}\to u\subseteq x)$.

Proposition.

$\omega $ is inductive.

**Proof.**

Easy exercise.

The simplicity of the results her bely their power. What we have done is to define a set $\omega =\left\{0,s\left(0\right),s\left(1\right),\dots \right\}$ and prove it is the least inductive set. (Be careful, as the $\dots $ is not precise and sets cannot be defined in this way except through special means such as those above.) What this is is in fact an induction principle, and $\omega $ is a copy of the natural numbers. To ephasise this we shall write $1$ for $s\left(0\right)$, $2$ for $s\left(1\right)$, $3$ for $s\left(2\right)$, and so on.

**Principle of induction on $\omega $:** If $\varphi \left(x\right)$
is a first order ${L}_{\in}$ formula, possibly with parameters,
and suppose $\varphi \left(0\right)$ holds and also $\forall x\u200a\left(\varphi \right(x)\to \varphi (s\left(x\right)\left)\right)$.
Then $\forall x\in \omega \u200a\varphi \left(x\right)$.

**Proof.**

The set $\{x\in \omega :\varphi \left(x\right)\}$ exists by separation and is inductive by hypothesis. Hence it equals $\omega $.

Proposition.

Every nonempty set $x\in \omega $ contains $0$.

**Proof.**

Induction on $x$.

Definition.

A set $t$ is transitive if for all sets $x,y$ we have $x\in y\in t$ implies $x\in t$.

Proposition.

Every set $x\in \omega $ is transitive.

**Proof.**

Induction on $x$.

Going hand-in-hand with induction is recursion, also sometimes
called inductive definitions

. We need to explain and justify these.

Set theory has many notions of function. One is function as a definable
first order formula. A formula $\varphi (\stackrel{\_}{x},y)$ behaves like a function
if $\forall \stackrel{\_}{x}\u200a\exists y\u200a\left(\varphi \right(\stackrel{\_}{x},y)\wedge \forall z\u200a\left(\varphi \right(\stackrel{\_}{x},z)\to y=z))$.
(This is usually abbreviated to $\forall \stackrel{\_}{x}\u200a\exists !y\u200a\varphi (\stackrel{\_}{x},y)$.)
Sometimes this is true when restricted to $\stackrel{\_}{x}$ from a particular set
or satisfying a partucular formula. Functions defined by formulas
are called *class functions*.

The other kind of function is a function as a set.

Definition.

$\u27e8x,y\u27e9$ is the set $\left\{\left\{x\right\},\left\{x,y\right\}\right\}$.

This exists by the pair set axiom.

Proposition.

If $\u27e8x,y\u27e9=\u27e8x\prime ,y\prime \u27e9$ then $x=x\prime $ and $y=y\prime $.

**Proof.**

Easy case-by-case argument.

Definition.

A *set function* is a set $f$ such that every element of
$f$ is $\u27e8x,y\u27e9$ for some sets $x,y$
and $\forall x,y,z\u200a(\u27e8x,y\u27e9\in f\wedge \u27e8x,z\u27e9\in f\to x=z)$.
For such an $f$ we write $\text{dom}\left(f\right)$
for
$\{u:\exists v\u200a\u27e8u,v\u27e9\in f\}$ and
$f\left(u\right)$ for the unique $v$ such that
$\u27e8u,v\u27e9\in f$ when $u\in \text{dom}\left(f\right)$.

Theorem.

Suppose $\varphi (x,\stackrel{\_}{a})$ and $\psi (x,y,z,\stackrel{\_}{a})$ are first order formulas such that $\exists !x\u200a\varphi (x,\stackrel{\_}{a})$ and $\forall x\u200a\forall y\u200a\exists !z\u200a\psi (x,y,z,\stackrel{\_}{a})$. Then there is a formula $\theta (x,y,\stackrel{\_}{a})$ such that $\forall x\in \omega \u200a\exists !y\u200a\theta (x,y,\stackrel{\_}{a})$ and

- $\theta (0,y,\stackrel{\_}{a})\leftrightarrow \varphi (y,\stackrel{\_}{a})$
- $\theta (x,y,\stackrel{\_}{a})\wedge \psi (x,y,z,\stackrel{\_}{a})\to \theta \left(s\right(x),z,\stackrel{\_}{a})$

This shows that we can define a function $f(x,\stackrel{\_}{a})$ by $f(0,\stackrel{\_}{a})=g\left(\stackrel{\_}{a}\right)$ and $f(x+1,\stackrel{\_}{a})=h(x,f(x,\stackrel{\_}{a}),\stackrel{\_}{a})$. In the statement of this theorem we have used class functions, but set functions take part in the proof.

**Proof.**

We say a set-function $f$ is an *attempt* if
$\text{dom}\left(f\right)$ is $x\cup \left\{x\right\}$ for some $x\in \omega $
such that

- $\varphi (y,\stackrel{\_}{a})\to f\left(0\right)=y$
- $\forall u\in \text{dom}\left(f\right)\u200a\forall y\u200a\forall z\u200a(u\ne x\wedge f(u)=y\wedge \psi (u,y,z,\stackrel{\_}{a})\to f(s\left(x\right))=z)$

Our formula $\theta (x,y,\stackrel{\_}{a})$ is the formula stating there is an attempt $f$ with $x\in \text{dom}\left(f\right)$ and $y=f\left(x\right)$.

The rest is an exercise. You need to prove by induction on $\omega $ that for all $x\in \omega $ attempts exist with $x\in \text{dom}\left(f\right)$ and that any two attempts $f,g$ agree on the values they give for $f\left(x\right),g\left(x\right)$.