Tuesday, 23 December 2025

Chapter 9 - Exercise 9

Let $Γ \equiv A : *, B : *, C : *$. Prove, by giving full derivations in $λD_0$:

(a) $\emptyset; \Gamma \; \vdash \; *:\Box$

(b) $\emptyset; \Gamma \; \vdash \; A : *$

(c) $\emptyset; \Gamma \; \vdash \; B : *$

(d) $\emptyset; \Gamma \; \vdash \; C : *$


The following derives all the results (a)-(d) in flag-format.