“Speech Acts & the Quest for a Natural Account of Classical *Proof*,” article in progress.

You are welcome to download and read this document. I *especially* welcome feedback on it. As it is not yet published in final form, if you want to cite the paper, please check with me first. Thanks.

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.

Do you like this, or have a comment? (I especially value feedback on work which is yet to be be published in final form.) If you do, please
*share* or *reply* on Twitter, or
email me.

← Proofs and Models in Naive Property Theory: A Response to Hartry Field's “Properties, Propositions and Conditionals” | Writing Archive | Geometric Models for Relevant Logics →

I’m *Greg Restall*, and this is my personal website. ¶ I am the Shelby Cullom Davis Professor of Philosophy at the University of St Andrews.

- Philosophy Department, The University of St Andrews
- greg@consequently.org
- @consequently@scholar.social on Mastodon.

To receive updates from this site, you can subscribe to the RSS feed of all updates to the site in an RSS feed reader, or follow me on Mastodon at @consequently@scholar.social, where I’ll update you if anything is posted.