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?

  • 1
    $\begingroup$ Somewhat related: hsm.stackexchange.com/q/11730/4251 $\endgroup$ Commented Jul 5, 2020 at 16:21
  • 1
    $\begingroup$ 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. $\endgroup$
    – Conifold
    Commented Jul 6, 2020 at 6:49
  • 1
    $\begingroup$ "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. $\endgroup$
    – Conifold
    Commented Jul 6, 2020 at 7:05
  • 1
    $\begingroup$ 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. $\endgroup$ Commented Jul 7, 2020 at 14:04


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.