Abstract: In this informal talk, I will revisit some longstanding issues in
philosophical logic in the light of some contemporary developments.
The longstanding issues? (1) Michael Dummett’s challenge in The Logical Basis
of Metaphysics to the effect that to get anywhere
in fundamental issues of metaphysics we would do well to attend to the
fundamental commitments of our theory of meaning—and that those concerns lead
to the conclusion that we can find common ground in intuitionistic logic, not
classical logic. (2) The issue of pluralism (or monism) about logical
consequence.
Contemporary work in logic is filled with a range of different (and seemingly
opposed) accounts of what follows from what. Many different kinds of logical
pluralism have arisen to attempt to make sense of the diversity of logical
analyses, and just as many defences of logical monism have been offered.
The contemporary developments? The rise of dependent type theory in computer
science and the consequent rise of proof assistants in the formalisation of
mathematics. Different proof assistants
(Agda,
Idris,
Lean, Isabelle,
Rocq/Coq)
make different choices in the formal representation of mathematical reasoning,
but the predominant choice of these proof assistants is to represent proofs
constructively, in what amounts to intuitionistic logic and not classical
logic. Proof assistants are steadily gaining ground in the mathematical
community—mathematicians use these tools as conversation partners in the
development of mathematical proofs, and many of these conversation partners
have intuitionistic scruples.
I will reexamine Dummett’s appeal to revisit fundamental commitments in our
theory of meaning, and the challenge of logical pluralism, given the example of
the use of proof assistants in mathematical reasoning. We will see that paying
attention to different aspects of our reasoning practices can clarify what is
at stake in debates over the use of this or that logic, or about the propriety
of some semantic principle. In the end, I hope to show that—as Dummett
argued—it is worthwhile to spend some time attending to the concepts we use in
our theorising, just as the astronomer must take care of her telescopes if she
wants to see clearly and see far, and understand the power and limits of her
tools. However, I will also show that taking Dummett’s advice does not mean
that we must accept his restrictive conclusion about the impropriety of
classical reasoning. Classical reasoning can be vindicated, but at some cost.
