Friday, February 23, 2007

Different formalisms for different reasoning?

In his "What is logic?" Ian Hacking attributes to William Tait a comment about how natural deduction is more suited towards intuitionistic reasoning while the sequent calculus is more suited to classical reasoning. At first, this comment struck me as odd because the sequent calculus didn't seem suited to anything but proving cut elimination in a nice way and showing a system has the subformula property. Then it occurred to me that Tait might have been talking about the one-sided sequent calculus. This is a neat little thing that one can develop out of the normal two-sided calculus. Since in the classical calculus one can move formulas across the sequent arrow by adding a negation, one can treat all formulas as though they were on the same side of the arrow. I believe this is because since in classical logic everything is equivalent to a formula in negation normal form and you can eliminate double negations, you can always convert a formula to an equivalent one in a nice form. In effect, you get a one-sided sequent ~A_1,...,~A_n,B_1,...,B_n from a two-sided sequent A_1,...,A_n=>B_1,...,B_n by sticking a negation in front of the A_i in the one-sided version. The one-sided version is then read as the disjunction of all the formulas, i.e. at least one of these holds, much like the consequent of the classical two-sided calculus says that at least one of those formulas holds given that all the antecedent formulas hold. Using the one-sided calculus lets you cut down on rules; you only need intro rules for &,v, and \forall and a way of taking care of negations (I will have to review my notes to clarify that). The proofs for the one-sided calculus are much easier and more intuitive than the proofs for the two-sided calculus. This is what makes me think that Tait was right and what makes me think that he was talking about the one-sided calculus.

As for why natural deduction is suited to intuitionistic reasoning, I'm not particularly sure. It certainly feels right, but there isn't a better reason I have off hand. I think I learned about the nuts and bolts of intuitionistic logic in the same setting in which I learned about natural deduction (a proof theory class), so the two are linked in my mind. This is just an accidental feature of my educational history though. I'm not sure what the clearer connection is that Tait sees. Maybe it has something to do with Prawitz's work on the introduction rules of natural deduction defining the intuitionistic connectives.


Aidan said...

Dummett and Tennant argued for intuitionist logic (partly, of course) on the basis that its natural deduction rules are harmonious, while those for classical logic aren't. A standard response for a while was to accuse the anti-realists of overly-privileging natural deduction; the suggestion was that the sequent calculus rules for classical logic were harmonious in just the same way as the natural deduction rules for IL are. I'd guess that it's at least in part these kinds of considerations that prompted Tait's comment.

(My logic teacher, Stephen Read, has subsequently argued at length that the Dummett/Tennant point fails even when we restrict our attention to natural deduction. See his 'Harmony and Autonomy in Classical Logic' in JPL 2000: 123-54).

Aidan said...

PS. That argument for IL can be found in Prawitz as well.

Shawn said...

That sounds like an eminently reasonable interpretation of Tait. I'm not entirely clear on the details of harmony, but the rules for the one-sided sequent calculus are pretty harmonious, in an intuitive sense. Harmony among the rules seems like a good reason to take natural deduction as suited to IL.

I'll try to check out the paper by Read in the nearish future.

Ole Thomassen Hjortland said...

Interesting post Shawn. I interpreted Hacking's remark the same way as Aidan (probably because I've already read Steve's paper on harmony). But I agree that the one-sided calculus is a further reason to think that SQ is particularly suited for classical logic.

Regarding the one-sided systems. I just learned the other day that there are also one-sided systems which use only the left side of sequents. These systems are essentially the same as semantic trees - well known from many introductory books on logic. These systems, of course, test the consistency of the premises (i.e., the antecedent side of the sequents, not the the sequent-premises themselves).

Ole Thomassen Hjortland said...

Oh, and by the way, I'm currently working on a paper on disagreement about logic. One of the major issues is how many arguments allegedly establishing that some logic or the other is the 'correct' logic turn out to be artifacts of the formal system the dispute is framed in. That conservativeness fails for classical negation in natural deduction but not in sequent calculus (and modified natural deduction systems as well - as showed in 'Harmony and Autonomy in Classical Logic') is an excellent example of this problem.