The following proposition in (1) is taken as an axiom in intuitionistic propositional logic.
$$(A\rightarrow(B\rightarrow C))\rightarrow((A\rightarrow B)\rightarrow(A\rightarrow C))\quad\quad(1)$$
What about its converse in (2)?
$$((A\rightarrow B)\rightarrow(A\rightarrow C))\rightarrow(A\rightarrow(B\rightarrow C))\quad\quad (2)$$
It's clear that (2) is also valid in intuitionistic propositional logic. But why it's less mentioned in the literature compared to (1)?
Best Answer
Formula (2) is indeed valid intuitionistically. The likely reason for its not being an axiom is that it follows easily from other intuitionistically valid formulas. The details of that would depend on the particular deductive system, but the idea is that $(B\to(A\to C))\to(A\to (B\to C))$ and $B\to(A\to B)$ together imply (2).