Exercise 4.6
(a) Prove that there are no $Γ$ and $N$ in λω such that $Γ ⊢ \Box : N$ is derivable.
(b) Prove that there are no $Γ$, $M$ and $N $in λω such that $Γ ⊢M→ \Box : N$ is derivable.
(a) We will prove this by structural induction.
Figure 4.1 in the textbook summarises the derivation rules for λω, and the conclusion $Γ ⊢ \Box : N$ must be a result of one of the seven rules.
In fact it can only be a result of (weak) or (conv). Let's consider each in turn.
Note that (var) is not applicable as the rule creates a variable, not a more general term. That is, $x$ in the rule is a metavariable which can represent a variable like $y$, but not any term, like $yx$ or $\Box$.
The induction hypothesis is that a judgement of the form $Γ ⊢ \Box : N$ is not derivable holds for the premises.
(weak) A conclusion $Γ ⊢ \Box : N$ would require $Γ' ⊢ \Box : N$ as one of the two premises. The induction hypothesis, true for the premises, is that $Γ' ⊢ \Box : N$ is not derivable. So the conclusion of this rule is not derivable.
(conv) A conclusion $Γ ⊢ \Box : N$ would require $Γ ⊢ \Box : M'$ as one of the two premises, where $M =_\beta M'$. By induction, $Γ ⊢ \Box : M'$ is not derivable, and so the conclusion of this rule is not derivable.
So by structural induction $Γ ⊢ \Box : N$ is not derivable in λω.
(b) We will also prove this by structural induction.
A conclusion $Γ ⊢M→ \Box : N$ can only be a result of the (weak), (form) and (conv) rules. Let's consider each in turn.
The induction hypothesis is that a judgement of the form $Γ ⊢M→ \Box : N$ is not derivable holds for the premises.
(weak) A conclusion $Γ ⊢M→ \Box : N$ would require $Γ' ⊢M→ \Box : N$ as one of the two premises. The induction hypothesis tell us that $Γ' ⊢M→ \Box : N$ is not derivable, So the conclusion of this rule is not derivable.
(form) A conclusion $Γ ⊢M→ \Box : N$ would require two premises $Γ ⊢M: N$ and $Γ ⊢\Box : N$. However, we've shown above that $Γ ⊢ \Box : N$ is not derivable, so the conclusion of this rule is not derivable.
(conv) A conclusion $Γ ⊢M→ \Box : N$ would require $Γ ⊢M→ \Box : M$ as one of the two premises, where $M =_\beta N$. The induction hypothesis tells us that a judgement of the form $Γ ⊢M→ \Box : M$ is not derivable, and so the conclusion of this rule is not derivable.
So by structural induction $Γ ⊢M→ \Box : N$ is not derivable in λω.
