Kolmogorov and Brouwer on constructive implication and the Ex Falso rule

摘要

In his dissertation (1907) Brouwer expressed several remarks concerning the subject which was later called "intuitionistic logic." His strict algorithmic point of view led to rejecting the Ex Falso principle and, unfortunately, to many other consequences. The Ex Falso principle was also rejected in Kolmogorov's 1.925 paper on logic. However, in 1932, using the "intended interpretation" (interpretation problem), Kolmogorov concluded that this rule should be accepted. Heyting's proof interpretation led to the same conclusion. Here the role of implication and negation in the Ex Falso principle in the works of Brouwer, Kolmogorov, and Heyting is studied. It is asserted that the 1907 point of view of Brouwer is too strict to create a satisfactory logic, and Brouwer exceeds the bounds of minimal logic in his understanding of implication. The above points of view are compared, and it is concluded that the interpretation problem and the proof interpretation, understood correctly, admit the full intuitionistic logic.