Exercise 6.10
Given $S : *$ and $P_1,P_2 : S →*$, we define in λC the expression:
$$R ≡ λx : S. ΠQ : S →*. (Πy : S. (P_1 y →P_2 y →Qy)) →Qx$$
We claim that $R$ codes ‘the intersection of $P_1$ and $P_2$’, i.e. the predicate that holds if and only if both $P_1$ and $P_2$ hold. In order to show this, give inhabitants of the following types, plus (shortened) derivations proving this:
(a) $Πx : S. (P_1 x →P_2 x →Rx)$
(b) $Πx : S. (Rx →P_1 x)$
(c) $Πx : S. (Rx →P_2 x)$
Why do (a), (b) and (c) entail that R is this intersection?
(Hint for (b): see Exercise 5.8(a).)
(a) An inhabitant of the type is
$$ \lambda x:S.\lambda f: P_1 x. \lambda g:P_2 x. \lambda h : \Pi y : S. (P_1 y \to P_2 y \to Qy).hxfg $$
The following is a shortened derivation.
(b) An inhabitant of the type is
$$ \lambda x:S . \lambda f:Rx . ( f P_1 (\lambda y:S.(\lambda a:P_1 y . \lambda b:P_2 y.a)) ) $$
The following is a shortened derivation.
(c) An inhabitant of the type is
$$ \lambda x:S . \lambda f:Rx . ( f P_2 (\lambda y:S.(\lambda a:P_1 y . \lambda b:P_2 y.b)) ) $$
The following is a shortened derivation.
The claim is that, for $x \in S$,
$$ P_1(x) \land P_2(x) \iff R(x) $$
"If and only if" $\iff$ has a particular meaning. $A \iff B$ means both $A \implies B$ and $B \implies A$.
In this case, it means both of the following are true:
- $ P_1(x) \land P_2(x) \implies R(x) $
- $ R(x) \implies P_1(x) \land P_2(x) $ which is equivalent to both $ R(x) \implies P_1(x) $ and $ R(x) \implies P_2(x) $.
The first is shown by (a), and the second is shown by both (b) and (c). So together, (a), (b) and (c), show that $R$ codes the intersection of $P_1$ and $P_2$.
