= Solution
Write $Q=(A\to B)\to A$ and $P=Q\to A$. The displayed formula is $(P\to B)\to B$. A proof of <logical implication> may use its temporary assumption more than once; this is ordinary <natural deduction>, not a linear proof system.
Assume $h:P\to B$, then $f:Q$, then $a:A$, then $g:Q$. The <identity weakening rule> derives $a:A$ from the hypotheses $a:A$ and $g:Q$. Discharging $g$ by the <implication introduction rule> gives $\lambda g^Q.a:P$. Applying $h$ by the <implication elimination rule> gives $h(\lambda g^Q.a):B$. Discharge $a$ to obtain $\lambda a^A.h(\lambda g^Q.a):A\to B$. Applying $f$ gives an $A$; discharge $f$ to obtain a $P$; apply $h$ once more to obtain $B$, and finally discharge $h$.
Here is the complete decorated <natural deduction> derivation, split at its intermediate $A\to B$ conclusion to keep the tree readable. Superscript labels mark which assumption occurrences are discharged; both occurrences labelled $1$ are discharged together.
$$
\frac{
\frac{
[h:P\to B]^1\qquad
\frac{\frac{[a:A]^3\quad[g:Q]^4}{a:A}\;\mathrm{Id}}
{\lambda g^Q.a:P}\;\to I_4
}{h(\lambda g^Q.a):B}\;\to E
}{\lambda a^A.h(\lambda g^Q.a):A\to B}\;\to I_3
$$
To avoid an excessively wide final tree, continue the same derivation as follows, using the right-hand derived premise above:
$$
\frac{
\frac{
[f:Q]^2\qquad \lambda a^A.h(\lambda g^Q.a):A\to B
}{f(\lambda a^A.h(\lambda g^Q.a)):A}\;\to E
}{\lambda f^Q.f(\lambda a^A.h(\lambda g^Q.a)):P}\;\to I_2
$$
followed by
$$
\frac{
\frac{[h:P\to B]^1\quad\lambda f^Q.f(\lambda a^A.h(\lambda g^Q.a)):P}
{h(\lambda f^Q.f(\lambda a^A.h(\lambda g^Q.a))):B}\;\to E
}{\lambda h^{P\to B}.h(\lambda f^Q.f(\lambda a^A.h(\lambda g^Q.a))):(P\to B)\to B}\;\to I_1.
$$
Thus the concise <lambda term>, with bound-variable types determined by the displayed tree, is
$$
\boxed{\lambda h.\;h\bigl(\lambda f.\;f(\lambda a.\;h(\lambda g.\;a))\bigr).}
$$
Under the <Curry-Howard correspondence>, <implication introduction rules> correspond to <lambda abstractions>, <implication elimination rules> to applications, and the <identity weakening rule> retains the first term while allowing an unused second hypothesis. No other inference rule or classical axiom is required.
Back to article page
