Exercise 5.12
In λP, consider the context
$Γ ≡ S : *$,
$R : S →S →*$,
$u : Πx,y : S. Rxy →Ryx$,
$v : Πx,y,z : S. Rxy →Rxz →Ryz$
(a) Show that $R$ is ‘reflexive on its domain’, by constructing an inhabitant of the type $Πx,y : S. Rxy →R xx$ in context $Γ$; give a corresponding (shortened) derivation.
(b) Show that $R$ is transitive by constructing an inhabitant of the type $Πx,y,z : S. Rxy →Ryz →Rxz$ in context $Γ$; give a corresponding (shortened) derivation.
(a) Before we develop a proper derivation, let's sketch out why $Πx,y : S. Rxy →R xx$ is true.
- (i) $\forall_{x,y \in S}(Rxy \implies Ryx)$
- (ii) $\forall_{x,y \in S}(Rxy \implies Rxz \implies Ryz)$
- We start with the assumption that $Rxy$ is true. By (i) this means $Ryx$ is true.
- Renaming variables in $(ii)$ gives $(Ryx \implies Ryx \implies Rxx)$. We swapped $x$ for $y$, and set $z$ to $x$.
- From $Ryx$, we have $Ryx \implies Rxx$. Since we have $Ryx$, we conclude $Rxx$.
- The assumption $Rxy$ gave us $Rxx$, that is $Rxy \implies Rxx$.
The following is a shortened λP derivation.
(b) Again, before we develop a proper derivation, let's sketch out why $Πx,y,z : S. Rxy →Ryz →Rxz$ is true.
- (i) $\forall_{x,y \in S}(Rxy \implies Ryx)$
- (ii) $\forall_{x,y \in S}(Rxy \implies Rxz \implies Ryz)$
- We start with the assumption that $Rxy$ is true. By (i) this means $Ryx$ is true.
- Renaming variables in (ii) gives us $(Ryx \implies Ryz \implies Rxz)$. He we swapped $x$ for $y$ and left $z$ as is.
- From $Ryx$, we have $(Ryz \implies Rxz)$.
- The first assumption $Rxy$ gave us $Ryz \implies Rxz$, that is $ Rxy \implies Ryz \implies Rxz$.
The following is a shortened λP derivation.
