 From your remarks it has become clear to me that the simple explanation of \(a \rightarrow b\) by “When I think \(a\), I must think \(b\)” is untenable; this idea is in any case too indeterminate to be able to serve as the foundation for a logic. But also your formulation: “When \(a\) has been proved, so has \(b\)”, is not wholly satisfactory to me; when I ask myself what you may mean by that, I believe that also \(a \rightarrow b\), like the negation, should refer to a proof procedure: “I possess a construction that derives from every proof of \(a\) a proof of \(b\)”. In the following, I will keep to this interpretation. There is therefore no difference between \(a \rightarrow b\) and \(+a \rightarrow +b\). (Troelstra 1983: 206–207; translation mine)