Can I define the set of natural numbers without the axiom of infinity? The exercise asks if exists a definition of $Nat(x)$ such that $Nat(x) \Rightarrow Nat(S(x))$, and $\exists x $such that $ Nat(x)$ is false without the use of axiom of infinity. Here $Nat(x) \Leftrightarrow x$ is a natural number, and $S(x)$ is the successor of $x$. 
I tried to define $$S(a)=\{a\}.$$ Then I define $$a \in C_a \Leftrightarrow (a\in C_a \Rightarrow S(s) \in C_a).$$
So $$\emptyset\in \cap C_i \forall i. $$
At the end I define $$Nat (a) \Leftrightarrow a\in C_\emptyset.$$ 
Can you ckech my idea or suggest another one?
 A: No, you cannot define the set of natural numbers without infinity; but you can define the property of being a natual number:
Define
\begin{equation}
Or(x)\equiv\forall y\in x(y\subset x) \wedge(\forall u,v\in x)(u\in v \vee v\in u \vee v=u);
\end{equation}
"$x$ is and ordinal". Then define,
\begin{equation}
Lim(x)\equiv Or(x)\wedge\forall y\in x\exists z\in x(y\in z);
\end{equation}
"$x$ is a limit ordinal". Finally we make,
\begin{equation}
Nat(x)\equiv x=\emptyset \vee (Or(x)\wedge \neg Lim(x) \wedge \forall y\in x(\neg Lim(y)\vee y=\emptyset))
\end{equation}
To check $Nat(x)\to Nat(S(x))$ remember that the succesor of any ordinal $x$ is $S(x)=x\cup\{x\}$, not $\{x\}$.
A: I don't understand your attempt.  In particular, you haven't actually defined what "$C_a$" is.  You wrote "$a \in C_a \Leftrightarrow (a\in C_a \Rightarrow S(s) \in C_a)$", but this is circular when taken as a definition (since $C_a$ appears on the right-hand side) and even if it weren't, it would only define when $a\in C_a$, not when $x\in C_a$ for arbitrary $x$.
The other answer describes the standard way to define $Nat(x)$.  Actually, though, for this problem as stated, you can do something much much simpler.  Note that the task of just naming a predicate $Nat(x)$ such that $Nat(x) \Rightarrow Nat(S(x))$ and $\exists x (\neg Nat(x))$ is much easier than actually defining the natural numbers.  For instance, you could define $Nat(x)$ to be $x\neq x$, and then it satisfies these properties.  Slightly less trivially, you could define $Nat(x)$ to be $x\neq \emptyset$, or $x\neq A$ for your favorite set $A$ which is not of the form $S(y)$ for any $y$.
A: Yes, all you need is some kind of type theory with induction principle.
You just define it like this:
N : Type
0 : N
s : N -> N

It works in many proof verifier and maybe some functional programming languages.
