Preservation Proof (Pierce exercise 2.2.8) In Benjamin C. Pierce's Types and Programming Languages, there's an exercise 2.2.8 that is as follows:
Suppose that $R$ is a binary relation on a set $S$, and $P$ is a predicate on $S$ that is preserved $R$. Show that $P$ is also preserved by $R^{*}$.
Is this attempt any good?:
Let $R, R^*, P$ as defined.
Suppose $(x,y)$ are in $R^*$. We want to show $P(x) = P(y)$.
If $(x,y)$ are in R, we're done since $P$ is preserved by $R$.
If $x=y$ (so that $(x,y) = (y,z)$), it follows that $P(x) = P(x) = P(y)$, as required.
Suppose that we have $(x,y)$ in $R$ and $(y,z)$ in $R$. So then $(x,z)$ will be in $R^*$ (by transitive closure). Note that since $P$ respects $R$, we have $P(x) = P(y) = P(z)$. So we have $P(x) = P(z)$ and P is also preserved by $R^*$.
 A: Let $R$ be a relation on $S$ and let $P \subseteq S$ such that $P$ is preserved by $R$:
$$\forall x \forall y \Bigl(x \in P \wedge \langle x, y \rangle \in R \rightarrow y \in P \Bigr)$$
Let $R^*$ denote the reflexive transitive closure of $R$. Then $R^*$ meets the following conditions:

*

*$R \subseteq R^*$ ($R^*$ contains $R$)

*$\forall x \in S\colon\langle x, x \rangle \in R^*$ ($R^*$ is reflexive)

*$\forall x \forall y \forall z \Bigl(\langle x, y \rangle \in R^* \wedge \langle y, z \rangle \in R^* \rightarrow \langle x, z \rangle \in R^*\Bigr)$ ($R^*$ is transitive)

*$\forall T \Bigl(T \text{ fulfills conditions 1-3} \rightarrow R^* \subseteq T\Bigr)$ ($R^*$ is the smallest such relation)

We wish to prove that $P$ is preserved by $R^*$.
Notice that we are basically trying to prove that $x \in P \rightarrow y \in P$ holds for all $\langle x, y \rangle \in R^*$. So we are interested in proving a statement for all ordered pairs in $R^*$. This is reminiscent of proving "for all"-statements involving the natural numbers. In the natural number case our main tool is induction.
But our inductive definition of the reflexive transitive closure gives rise to it's very own principle of (structural) induction (you might want to compare this to the content of Section 3.3 in Pierce's TAPL).
To uncover this induction principle and prove our initial goal we'll first define a set of ordered pairs that satisfy our condition:
$$\mathcal{I} = \Bigl\{\langle x, y \rangle \in R^* : x \in P \rightarrow y \in P\Bigr\} $$
If we manage to prove that $\mathcal{I}$ is reflexive, transitive and contains $R$, then we could conclude that $R^* \subseteq \mathcal{I}$ (by letting $T=\mathcal{I}$ in the minimality condition of $R^*$).

*

*Reflexivity of $\mathcal{I}$: Let $x \in S$. By reflexivity of $R^*$ we have $\langle x, x \rangle \in R^*$. Combined with the tautology $x \in P \rightarrow x \in P$ we can say that $\langle x, x \rangle \in \mathcal{I}$.

*Transitivity of $\mathcal{I}$: Let $\langle x, y \rangle, \langle y, z \rangle \in \mathcal{I}$. Then $\langle x, y \rangle, \langle y, z \rangle \in R^*$, $x \in P \rightarrow y \in P$ and $y \in P \rightarrow z \in P$. By transitivity of $R^*$ we have $\langle x, z \rangle \in R^*$ and by Hypothetical syllogism we have $x \in P \rightarrow z \in P$. Thus $\langle x, z \rangle \in \mathcal{I}$.

*$\mathcal{I}$ contains $R$: Let $\langle x, y \rangle \in R$. Since $R \subseteq R^*$ we have $\langle x, y \rangle \in R^*$. Now suppose that $x \in P$. Since $\langle x, y \rangle \in R \wedge x \in P$ and $P$ is preserved by $R$, we have $y \in P$. Hence $x \in P \rightarrow y \in P$ and combined with $\langle x, y \rangle \in R^*$ we have $\langle x, y \rangle \in \mathcal{I}$.

Hence $R^* \subseteq \mathcal{I}$ (we can in fact say that $R^* = \mathcal{I}$ as the other inclusion $\mathcal{I} \subseteq R^*$ follows directly from the construction of $\mathcal{I}$). Equipped with this information we can conclude that $P$ is also preserved by $R^*$ almost immediately.
Let $x \in P$ and $\langle x, y \rangle \in R^*$. But then $\langle x, y \rangle \in \mathcal{I}$ because $R^* \subseteq \mathcal{I}$. In particular we then know that $x \in P \rightarrow y \in P$. One application of Modus ponens tells us that $y \in P$. Hence $x \in P \wedge \langle x, y \rangle \in R^* \rightarrow y \in P$ for all $x,y$ as required.
