 In order to describe the logic used by the intuitionist mathematician, it was necessary first to analyse the mathematical processes of the mind, from which analysis the logic could be extracted. In 1930, Brouwer’s most famous pupil, Arend Heyting, published a set of formal axioms which so clearly characterise the logic used by the intuitionist that they have become universally known as the axioms for  intuitionistic logic  (Heyting [1930]). These axioms captured the informal BHK-interpretation of the connectives and quantifiers that we gave earlier.