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$ – Rodrigo de Azevedo Jul 5 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 Jul 6 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 Jul 6 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$ – Mauro ALLEGRANZA Jul 7 at 14:04

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.