 The formula \(a \rightarrow b\) generally means: “If \(a\) is correct, then \(b\) is correct too”. This proposition is meaningful if \(a\) and \(b\) are constant propositions about whose correctness nothing need be known … The case if conceivable that after the statement \(a \rightarrow b\) has been proved in the sense specified, it turns out that \(b\) is always correct. Once accepted, the formula \(a \rightarrow b\) then has to remain correct; that is, we must attribute a meaning to the sign \(\rightarrow\) such that \(a \rightarrow b\) still holds. The same can be remarked in the case where it later turns out that \(a\) is always false. For these reasons, the formulas [\ref{HeytingAxiom5}] and [\ref{HeytingAxiom10}] are accepted. (Heyting 1930: 44 [Mancosu 1998: 313])