= Solution
By part (a), such a term would prove
$$
((\sigma\to\tau)\to\sigma)\to\sigma
$$
in intuitionistic propositional logic. Consider the two-world <Kripke model for intuitionistic propositional logic> $r<s$. Let $\sigma$ hold only at $s$ and let $\tau$ hold nowhere. At both worlds $\sigma\to\tau$ fails, so $(\sigma\to\tau)\to\sigma$ holds at $r$ vacuously, while $\sigma$ does not hold at $r$. The displayed formula therefore fails at $r$. By the <Kripke completeness theorem for intuitionistic propositional logic>, it is not derivable, so no simply typed lambda term inhabits that type.
Back to article page
