Transitive closure proof (Pierce, ex. 2.2.7) Simple exercise taken from the book Types and Programming Languages by Benjamin C. Pierce.
This is a definition of the transitive closure of a relation R.
First, we define the sequence of sets of pairs:
$$R_0    = R$$
$$R_{i+1}  = R_i \cup \{ (s, u) | \exists t, (s, t) \in R_i, (t, u) \in R_i \}$$
Finally, define the relation $R^+$ as the union of all the $R_i$:
$$R^+=\bigcup_i R_i$$
Show that $R^+$ is really the transitive closure of R.
Questions:


*

*I would like to see the proof (I don't have enough mathematical background to make it myself).

*Isn't the final union superfluous? Won't $R_n$ be the union of all previous sequences?

 A: First of all, if this is how you define the transitive closure, then the proof is over. But you may still want to see that it is a transitive relation, and that it is contained in any other transitive relation extending $R$.
To the second question, the answer is simple, no the last union is not superfluous because it is infinite. Every step contains a bit more, but not necessarily all the needed information.
So let us see that $R^+$ is really transitive, contains $R$ and is contained in any other transitive relation extending $R$.


*

*Clearly $R\subseteq R^+$ because $R=R_0$.

*If $x,y,z$ are such that $x\mathrel{R^+} y$ and $y\mathrel{R^+}z$ then there is some $n$ such that $x\mathrel{R_n}y$ and $y\mathrel{R_n}z$, therefore in $R_{n+1}$ we add the pair $(x,z)$ and so $x\mathrel{R_{n+1}}z$ and therefore $x\mathrel{R^+}z$ as wanted.

*If $T$ is a transitive relation containing $R$, then one can show it contains $R_n$ for all $n$, and therefore their union $R^+$. To see that $R_n\subseteq T$ note that $R_0$ is such; and if $R_n\subseteq T$ and $(x,z)\in R_{n+1}$ then there is some $y$ such that $(x,y)\in R_n$ and $(y,z)\in R_n$. Since $R_n\subseteq T$ these pairs are in $T$, and since $T$ is transitive $(x,z)\in T$ as well.

A: We need to show that $R^+$ contains $R$, is transitive, and is minmal among all such relations.
$R\subseteq R^+$ is clear from $R=R_0\subseteq \bigcup R_i=R^+$.
Transitivity:
By induction on $j$, show that $R_i\subseteq R_j$ if $i\le j$.
Assume $(a,b), (b,c)\in R^+$. Then $(a,b)\in R_i$ for some $i$ and $(b,c)\in R_j$ for some $j$. This implies $(a,b),(b,c)\in R_{\max(i,j)}$ and hence $(a,c)\in R_{\max(i,j)+1}\subseteq R^+$. 
Now for minimality, let $R'$ be transitive and containing $R$.
By induction show that $R_i\subseteq R'$ for all $i$, hence $R^+\subseteq R'$, as was to be shown.
As for your specific question #2:
Yes, $R_n$ contains all previous $R_k$ (a fact, the proof above uses as intermediate result). But neither is $R_n$ merely the union of all previous $R_k$, nor does there necessarily exist a single $n$ that already equals $R^+$.
For example, on $\mathbb N$ take the realtaion $aRb\iff a=b+1$. Then $aR^+b\iff a>b$, but $aR_nb$ implies that additionally $a\le b+2^n$.
