Exercise 4.2
Give complete λω-derivations, first in tree format and then in flag format (not shortened), of the following judgements:
(a) $∅ ⊢ (∗→∗) →∗ : \Box$
(b) $α : ∗, β : ∗ ⊢ (α →β) →α : ∗$
(a) The tree format derivation is as follows.
$$ (1) \; \emptyset \vdash * : \Box \quad (sort)$$
$$ \frac{(1) \; \emptyset \vdash * : \Box \qquad (1) \; \emptyset \vdash * : \Box \quad} {(2) \; \emptyset \vdash * \to * : \Box} \;(form) $$
$$ \frac{(2) \; \emptyset \vdash * \to * : \Box \qquad 1) \; \emptyset \vdash * : \Box} {(3) \; \emptyset \vdash (* \to *) \to * : \Box} \;(form) $$
The flag format derivation is as follows.
(b) The tree format derivation is as follows.
$$ (1) \; \emptyset \vdash * : \Box \quad (sort)$$
$$ \frac{(1) \; \emptyset \vdash * : \Box}{(2) \; \alpha:* \vdash \alpha:*} \; (var) $$
$$ \frac{(1) \; \emptyset \vdash * : \Box \qquad (1) \; \emptyset \vdash * : \Box}{(3) \; \alpha:* \vdash *:\Box} \; (weak) $$
$$ \frac{(2) \; \alpha:* \vdash \alpha:* \qquad (3) \; \alpha:* \vdash *:\Box}{(4) \; \alpha:*, \beta:* \vdash \alpha:*} \; (weak) $$
$$ \frac{(3) \; \alpha:* \vdash *:\Box}{(5) \; \alpha:*, \beta:* \vdash \beta:*} \; (var) $$
$$ \frac{(4) \; \alpha:*, \beta:* \vdash \alpha:* \qquad (5) \; \alpha:*, \beta:* \vdash \beta:*}{(6) \; \alpha:*, \beta:* \vdash \alpha \to \beta:*} \; (form) $$
$$ \frac{(6) \; \alpha:*, \beta:* \vdash \alpha \to \beta:* \qquad (4) \; \alpha:*, \beta:* \vdash \alpha:*}{(7) \; \alpha:*, \beta:* \vdash (\alpha \to \beta) \to \alpha:*} \; (form) $$
The flag format derivation is as follows.
