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.

Advertisements