Friday, September 28, 2007

That seemingly magical fact

[Edit: I'm trying out using the html for the math symbols and Greek letters since Blogger won't do LaTeX markup. Let me know if they are not rendering correctly in your browser.]
Sometimes you read that that natural deduction systems are more appropriate for intuitionistic logic while sequent calculi are more appropriate for classical logic, e.g. in Hacking's article "What Is Logic?", whence the title. While reading a defense by Peregrin of why intuitionistic logic best characterizes the logic of inference, I came across a line that caught my eye. Peregrin comes to the conclusion that intuitionistic logic is the logic of inference as long as we restrict ourselves to single conclusion inferences. He goes on to say that he has written elsewhere about why we should restrict ourselves in that way. The interesting bit is the restriction to single conclusion inference.

One of the first lessons learned when studying the sequent calculus is that you get classical logic from the intuitionistic rules by allowing multiple conclusions. Going back over my notes from proof theory last year, it seems that you can also get classical logic if you keep the single conclusion by add a reductio rule, Γ, ∼φ ⇒ ⊥, so Γ => φ. This requires giving up the subformula property, so the multiple conclusion formulation is usually opted for.

Natural deduction systems only allow for one conclusion for each inference. This doesn't mean we don't have natural deduction systems for classical logic. We do, but they involve a reductio rule, from ∼∼φ to φ. How would this square with being more appropriate to intuitionistic logic? There seems to be a sense in which the reductio rule is really a multiple conclusion rule. In a standard multiple conclusion sequent calculus formulation, proving the reductio rule requires using multiple conclusions. Alternatively, we can prove that a formula is provable in a classical natural deduction system with reductio iff it is provable in the multiple conclusion sequent calculus. Given that this is "iff", why should the sequent calculus version be privileged? The sequent calculus version has the subformula property and cut elimination. This puts really strong restrictions on the structure of proofs. In particular, the subformula property requires that only the things in the bottom line of the proof appear in the preceding steps of the proof. This restriction is strong enough to simulate, in a way, semantic effects (See Jeremy Avigad's work for more on this). Put in a more philosophical way, it requires us to make explicit everything that goes directly in to the proof.

This explicitness requirement does the work. The sequent calculus version shows us that the reductio rule is really a multiple conclusion wolf masquerading in single conclusion sheep's clothing. It is apparent that none of the other rules require multiple conclusions. These correspond to the intuitionistic sequent calculus rules and they go over directly to natural deduction systems. Classical logic with its reductio rule can go over too, but along the way the reductio rule assumes the appearance of a single conclusion rule. Natural deduction is natural for single conclusion inference and the sequent calculus is natural for multiple conclusion inference (I haven't really defended the latter claim here). There is a sense, then, in which natural deduction is more natural for intuitionistic logic.

No comments: