Inductively and Co-Inductively defined sets "Even" set can be represented as Inductively Defined sets with two rules:
"$0 \in E$" and "$X \in E \implies X+2 \in E$"
now my question is, how the Co-Inductively defined sets are defined? why do we need them?
and what are the differences?
 A: Essentially, an inductive datatype is one that is characterised by introduction rules, whereas a coinductive datatype is characterised by elimination rules. Here is one of the simplest pair of examples. Let $X$ be a fixed set.


*

*Finite lists of elements of $X$ constitute an inductive datatype. There are two introduction rules:


*

*The empty list $\mathsf{nil}$ is a finite list.

*If $x$ is an element of $X$ and $t$ is a finite list, then $\mathsf{cons}(x, t)$, i.e. the list obtained by prefixing $x$ to $t$, is also a finite list.


*Streams of elements of $X$ constitute a coinductive datatype. There are two elimination rues:


*

*If $s$ is a stream, then $\mathsf{head}(s)$ is an element of $X$.

*If $s$ is a stream, then $\mathsf{tail}(s)$ is another stream.



Now, how do we capture this formally? We need to transform the introduction/elimination rules into recursion/corecursion principles. For the above example, we get the following:


*

*If $A$ is any set equipped with a chosen constant $a$ and a map $c : X \times A \to A$, then there is a unique map $f : \mathsf{List}(X) \to A$ such that $f (\mathsf{nil}) = a$ and $f (\mathsf{cons}(x, t)) = c(x, f(t))$.

*If $C$ is any set equipped with maps $h : C \to X$ and $t : C \to C$, then there is a unique map $g : C \to \mathsf{Stream}(X)$ such that $\mathsf{head}(g(c)) = h(c)$ and $\mathsf{tail}(g(c)) = g(t(c))$.
Now, for various reasons it is easy to convert a recursion principle on a set into an induction principle. In the case of $\mathsf{List}(X)$ it amounts to saying that any subset $Y$ of $\mathsf{List}(X)$ containing $\mathsf{nil}$ and closed under $\mathsf{cons}(x, -)$ for all $x$ in $X$ must be the whole of $\mathsf{List}(X)$. (In the case $X = \{ 0 \}$ this is ordinary mathematical induction!)
However, coinduction is a rather more unfamiliar concept. The coinduction principle associated with $\mathsf{Stream}(X)$ says this: for any equivalence relation $\sim$ on $\mathsf{Stream}(X)$, if $\mathsf{head}(s) = \mathsf{head}(s')$ and $\mathsf{tail}(s) \sim \mathsf{tail}(s')$ whenever $s \sim s'$, then in fact $\sim$ is the equality relation on $\mathsf{Stream}(X)$.
To get a really concrete description of $\mathsf{List}(X)$ and $\mathsf{Stream}(X)$ as sets we must solve what are basically fixed point equations:
$$\mathsf{List}(X) \cong 1 + X \times \mathsf{List}(X)$$
$$\mathsf{Stream}(X) \cong X \times \mathsf{Stream}(X)$$
It is not hard to see that
$$\mathsf{List}(X) = 1 + X + X^2 + X^3 + \cdots = \sum_{n \in \mathbb{N}} X^n$$
$$\mathsf{Stream}(X) = X \times X \times X \times \cdots = X^\mathbb{N}$$
are solutions, but we must still check that these satisfy the appropriate recursion/corecursion principle: fortunately, this is straightforward.
