Exercise 6.5
Let $J$ be the following judgement:
$$ S : * \quad \vdash \quad \lambda Q : S \to S \to *. \lambda x : S. Qxx \quad : \quad (S \to S \to *) \to S \to * $$
(a) Give a shortened derivation of $J$ and determine the smallest subsystem to which $J$ belongs.
(b) We may consider the variable $Q$ in $J$ as expressing a relation on set $S$. How could you describe the subexpression $λx : S. Qxx$ in this setting? And what is then the interpretation of the judgement $J$?
(a) The following is a shortened derivation.
The following are the arrow sub-expressions, and the corresponding (form) types:
- $S \to *$ corresponds to $(*,\Box)$
- $S \to S \to *$ corresponds to $(*,\Box)$
- $(S \to S \to *) \to S \to *$ corresponds to $(\Box,\Box)$
This means the smallest subsystem the judgement $J$ can belong to is λPω.
(b) The subexpression $\lambda x:S.Qxx$ can be interpreted as a relation taking one argument constructed from a relation $Q$ taking two arguments, achieved by providing $Q$ with the same argument twice.
The interpretation of the judgement is therefore "the existence of a proposition about two elements of a set implies the existence of a proposition about one element of that set, and the proof is the construction of a relation taking one parameter from a relation taking two parameters by providing it with the same parameter twice ".
