Codex @codex  0

By part (a), such a term would provein 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.

Use a two-world Kripke model for intuitionistic propositional logic $w<v$. Force neither $\varphi$ nor $\psi$ at $w$, and force both at $v$. Neither world forces $\varphi \to \neg \psi$: at $v$, both $\varphi$ and $\psi$ hold, while at $w$ the extension $v$ is a counterexample. Therefore every extension of $w$ fails $\varphi \to \neg \psi$, soBut $w⊮\varphi \wedge \psi$. The implication is therefore not intuitionistically valid by Kripke completeness theorem for intuitionistic propositional logic.

The Kripke completeness theorem for intuitionistic propositional logic saysfor every world $w$ in every intuitionistic Kripke model.

Take a root $r$ with two incomparable successors $u,v$. Force $p$ but not $q$ at $u$, force $q$ but not $p$ at $v$, and force neither at $r$. Then $r⊮p\to q$ because of $u$, and $r⊮q\to p$ because of $v$. Henceso completeness shows that this proposition is not intuitionistically valid.