Event Detail

It is tempting to take the logical connectives, such as conjunction, disjunction, negation and the material conditional to be defined by the basic inference rules in which they feature. Systems of ‘natural deduction’ provide the basic framework for studying these inference rules. In natural deduction proof systems, well-behaved rules for the connectives give rise to intuitionistic logic, rather than to classical logic. Some, like Michael Dummett, take this to show that intuitionistic logic is on a sounder theoretical footing than classical logic. Defenders of classical logic have argued that other proof-theoretical frameworks, such as Gentzen’s sequent calculus, or a bilateralist system of natural deduction, can provide a proof-theoretic justification of classical logic. Such bilateralist defences of classical logic have significant shortcomings, in that the systems of proof offered are much less natural than existing systems of natural deduction. Neither sequent derivations nor bilateralist natural deduction proofs are good matches for representing the inferential structure of everyday proofs.

In this talk I clarify the shortcomings of existing bilateralist defences of classical proof, and, making use of recent results in the proof theory for classical logic from theoretical computer science (specifically, the λμ calculus of Michel Parigot), I show that the bilateralist can give an account of natural deduction proof that models our everyday practice of proof as well as intuitionist natural deduction, if not better.

https://berkeley.zoom.us/j/99271828753 Registration with Zoom is required for access. Password hint: Gödel’s first name (lowercase)