Abstract: Michael Dummett, in a presentation to the Aristotelian Society 65 years ago (in 1959) inaugurated a long-running debate over semantic realism and anti-realism, and the issue of settling an appropriate logic as a necessary prolegomenon to fruitful discussion metaphysics. Dummett argued that the principles of intuitionistic logic are semantically neutral, but that essentially classical principles carry distinctive metaphysical commitment.
This debate reached its peak in the 1980s and 1990s, but has receded from view in recent years. The situation is curiously reversed in mathematics. Constructive mathematics (in which the underlying logic is intuitionistic) was very much a minority mathematical tradition in the second half of the 20th Century, but has undergone a significant renaissance in recent years, with the advent of proof assistants, such as Agda and Lean. Now, many mathematicians are busy representing informal mathematical proofs in constructive dependent type theory, in which distinctively classical logical principles, if used, are optional extra commitments, and not part of the underlying logic.
In this talk, I will attempt to make sense of this state of affairs, revisiting Dummett’s original concerns in the light of the advent of proof assistants. Along the way, we will encounter issues around logical pluralism, the open texture of concepts, the norms of inference and assertion, and the role of computational devices in our expressive and justificatory practices.
