 Kolmogorov’s strategy to obtain a (fragment) of formalized intuitionistic logic was to start with a classical system and isolate an intuitionistically acceptable system from it. (Note that, although Kolmogorov refers to Principia Mathematica, he did not take it as his point of departure.) This might (roughly) be described as the method of crossing out, which is also what Heyting would do in 1928 (see below). Given the task Kolmogorov set himself, it is a natural approach. Kolmogorov’s criterion whether to keep an axiom was whether a proposition has an “intuitive foundation” or “possesses intuitive obviousness” (van Heijenoort 1967: 421, 422); on implication he said,