 The distinction between \(p\) and \(+p\) vanishes as soon a construction is intended in \(p\) itself, for the possibility of a construction can be proved only by its actual execution. If we limit ourselves to those propositions which require a construction, the logical function of provability does not arise at all. We can impose this restriction by treating only propositions of the form “\(p\) is provable”, or, to put it another way, by regarding every intention as having the intention of a construction for its fulfillment added to it. It is in this sense that intuitionistic logic, insofar as it has been developed up to now without using the function +, must be understood. (Heyting 1931: 115 [Benacerraf &amp; Putnam 1983: 60; translation modified])