# How did Kolmogorov came up with his formalization of intuitionistic logic?

According to this article Kolmogorov published a paper in 1925 in which he attempted to formalize Brouwer’s intuitionistic mathematics. In that paper there are the following logical formulas:

\begin{align} \tag{1} A & \rightarrow(B \rightarrow A)\\ \tag{2} (A > \rightarrow(A \rightarrow B)) & \rightarrow (A \rightarrow B)\\ > \tag{3} (A \rightarrow(B \rightarrow C)) & \rightarrow (B > \rightarrow(A \rightarrow C))\\ \tag{4} (B \rightarrow C) & > \rightarrow((A \rightarrow B) \rightarrow(A \rightarrow C))\\ \tag{5} > (A \rightarrow B) & \rightarrow((A \rightarrow \neg B) \rightarrow > \neg A)\\ \end{align}

Were there any preceding concepts that he used to come up with the above?

Is it possible to reconstruct a plausible thought process and preceding conceptual resources that he used to come up with these formulas?

• Somewhat related: hsm.stackexchange.com/q/11730/4251 Jul 5 '20 at 16:21
• SEP article you linked mentions the background:"As van Dalen has suggested, Kolmogorov probably had come into contact with intuitionism through Alexandrov or Urysohn, who were close friends of Brouwer’s. Kolmogorov was in any case remarkably well-informed, citing even papers that had only appeared in the Dutch-language". There were no prior formalizations of intuitionism, and Brouwer himself was opposed to them in principle as antithetical to his idea of intuitionism (as was clear from his reaction to Heyting's later). You may want to look at Hesseling's book they cite for educated guesses. Jul 6 '20 at 6:49
• "Kolmogorov's paper stands head and shoulders above other contributions to the debate at the time", he says (p. 241). On formal side Kolmogorov was familiar with Hilbert's 1922 lecture. Another useful source is van Dalen, Kolmogorov and Brouwer on constructive implication and the Ex Falso rule (freely available), who lists Brouwer's works Kolmogorov knew and speculates on word of mouth transmission through Alexandrov and Urysohn in 1923-4. Jul 6 '20 at 7:05
• It is "simply" derived from that of David Hilbert, Die logischen Grundlagen der Mathematik (1922) separating the intuitionistic treatment of negation from the classical one. Jul 7 '20 at 14:04