 The argument is, however, incomplete. It is uncontroversial that, once \(a \rightarrow b\) has been proved, it should remain so when afterward \(\neg a\) is proved. But why should \(a \rightarrow b\), if it has not yet been proved, become provable just by establishing \(\neg a\)? (Johansson asked this in a letter to Heyting in  1935;[28]  see Section 1 of the supplementary document  Objections to the Proof Interpretation). Clearly, then, further work needed to be done on the explanation of intuitionistic logic.