The proof-explanation of logical constants is logically neutral
Göran Sundholm · Revue internationale de philosophie · 2004
The ultimate justification of intuitionism lies in its conception of truth. The paper presents the effects of this conception on mathematics and logic. Brouwer saw very little value in logic and aimed almost exclusively to produce a good theory of the continuum. To this end, he introduced time into the hitherto static world of mathematics. However it is in logic that intuitionists are more active today. Intuitionistic logic interprets the conditional as a function. The resulting relationship with typed lambda calculus leads to the Formula-as-Type principle, the philosophical consequences of which are as important as its applications in computer science. They concern not only our idea of proof but also the basic notions of logic: formalism has to be given up and some traditional distinctions are vindicated.