Abstract: 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 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 some other proof-theoretical framework, such as Gentzen’s sequent calculus, or a bilateralist system of signed natural deduction, can provide a proof-theoretic justification of classical logic. Such 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 signed natural deduction proofs are good matches for representing the inferential structure of everyday proofs.
In this paper 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, 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.
