Exercise 6.4
Let $Γ ≡S : *, Q : S →S →*$ and let $M$ be the following expression:
$$M ≡ (Πx,y : S. (Qxy → Qyx → ⊥)) → Πz : S. (Qzz → ⊥)$$
(a) Give a shortened derivation of $Γ ⊢M : *$ and determine the smallest subsystem to which this judgement belongs.
(b) Prove in λC that $M$ is inhabited in context $Γ$. You may use a shortened derivation.
(c) We may consider $Q$ to be a relation on set $S$. Moreover, it is reasonable to see $A →⊥$ as the negation $¬A$ of proposition $A$. (We shall explain this in Section 7.1.) How can $M$ then be interpreted, if we also take Figure 5.2 into account? And what is a plausible interpretation of the inhabiting term you found in (b)?
(a) The following is a shortened derivation of $Γ ⊢M : *$.
The following are the arrow sub-terms and their corresponding (form) types:
- Context $S \to *$ corresponding to $(*,\Box)$.
- Context $S \to S \to *$ corresponding to $(*, \Box)$.
- Subterm $Qyx \to \bot$ corresponding to $(*,*)$.
- Subterm $\bot$ corresponding to $(\Box, *)$.
- Subterm $Qxy \to Qyx \to \bot$ corresponding to $(*,*)$.
- Subterm $\Pi x,y:S.(Qxy \to Qyx \to \bot)$ corresponding to $(*,*)$
- Subterm $Qzz \to \bot$ corresponding to $(*,*)$.
- Subterm $Qxy \to Qyx \to \bot$ corresponding to $(*,*)$.
- Subterm $\Pi z:S.(Qzz \to \bot)$ corresponding to $(*,*)$
- Term $(\Pi x,y:S.(Qxy \to Qyx \to \bot)) \to \Pi z:S.(Qzz \to \bot)$ corresponds to $(*,*)$.
This means the smallest subsystem the judgement can belong to is λP2.
(b) By inspection the inhabitant should be
$$\lambda f:(\Pi x,y:S.(Qxy \to Qyx \to \bot)) . (\lambda z:S.(\lambda q:Qzz.fzzq))$$
The following is a derivation of this inhabitant, continuing from the derivation of the type above.
(c) The interpretation of $M$ is as follows.
$$\forall_{x,y \in S}(\; Q(x,y) \implies \neg Q(y,x)\; ) \implies \forall_{z \in S}(\; \neg Q(z,z) \; )$$
In words, if $Q$ is asymmetric, then $Q$ is not reflexive.
The interpretation of the inhabitant is "there exists a function (here, $f$) that maps an asymmetric function to an irreflexive function", which proves the above logical statement.
