 Heyting also proposes a provability operator +, where \(+p\) means “\(p\) is provable”. The distinction between \(p\) and \(+p\) is relevant if one believes that (at least some) propositions are true or false independently of our mathematical activity. In that case one can go on and develop a provability logic, as for example Gödel did (see  Section 1 of the supplementary document  The Turn to Heyting’s Formalized Logic and Arithmetic.) That is not the intuitionistic conception, and Heyting remarks that, if the fulfillment of \(p\) requires a construction, then there is no difference between \(p\) and \(+p\). He adds that, on the intuitionistic explanation of negation, there is indeed no difference between \(\neg p\) and \(+\neg p\), as a proof of \(\neg p\) is defined as a construction that reduces \(p\) to a contradiction. But Heyting does not generalize this remark to all of intuitionistic logic. The final section of the paper is a further discussion of the logic of the provability operator, in particular its interaction with negation (e.g., \(\vdash \neg +p\) is the assertion that \(p\) is unprovable). But Heyting ends by saying that, as the intuitionists’ task is the reconstruction of all mathematics, while at the same time no examples of propositions have been found so far for which this provability operator would be necessary to express their status (e.g., to express absolute undecidability), it cannot be asked of intuitionists that they develop this logic (Heyting 1930C: 963 [Mancosu 1998: 309–310])