  According to Brouwer, truth in constructive (intuitionistic)  mathematics means the existence of a proof, cf. (Troelstra and van  Dalen 1988). In 1931–34, Heyting and Kolmogorov gave an  informal description of the intended proof-based semantics for  intuitionistic logic (Kolmogorov 1932, Heyting 1934), which is now  referred to as the Brouwer-Heyting-Kolmogorov (BHK)  semantics. According to the BHK conditions, a formula is  ‘true’ if it has a proof. Furthermore, a proof of a  compound statement is connected to proofs of its components in the  following way: