Exercise 5.11
Let $S$ be a set, with $Q$ and $R$ relations on $S \times S$, and let $f$ and $g$ be functions from $S$ to $S$.
Assume that
(i) $∀_{x,y∈S}(Q(x,f(y)) ⇒ Q(g(x),y))$
(ii) $∀_{x,y∈S}(Q(x,f(y)) ⇒R(x,y))$
(iii) $∀_{x∈S}(Q(x,f(f(x))))$
Prove that $$∀_{x∈S}(R(g(g(x)),g(x)))$$ by giving a context $Γ$ and finding a term $M$ such that:
$$Γ ⊢ M : Πx : S. R (g(gx)) (gx)$$
Give the corresponding (shortened) λP-derivation.
Before we develop a proper proof it is useful to sketch out why $\forall_{x \in S}(R(g(g(x)),g(x)))$ is true.
We first note that since $f:S \to S$ and $g:S \to S$, then $f(x) \in S$ and $g(x) \in S$ for all $x \in S$. In addition the output of any function composition of $f$ and $g$ is also in $S$.
We then note, for all $x \in S$:
- Assumption (ii) tells us $Q(g(g(x)),f(g(x))$ implies $R(g(g(x)),g(x))$.
- Assumption (i) tell us $Q(g(x),f(f(g(x))))$ implies $(Q(g(g(x)),f(g(x)))$.
- Assumption (iii) tells us $Q(g(x),f(f(g(x))))$ is true because $g(x) \in S$.
The following is a λP derivation, with a context and an inhabitant of $Πx : S. R (g(gx)) (gx)$.
So the full judgement is
$$\begin{align} S &:*, \\ Q, R &: S \to S \to *, \\ f,g &: S \to S, \\ u &: \Pi x,y:S .Qx(fy) \to Q(gx)y, \\ v &: \Pi x,y:S .Qx(fy) \to Rxy, \\ w &: \Pi x:S.Qx(f(fx)) \\ \\ & \vdash \lambda x:S. v(g(gx))(gx)(u(gx)(f(gx))(w(gx))) \; : \; \Pi x:S. R(g(gx))(gx) \end{align}$$
