Here's a question that I've long thought to be a puzzle in the history of logic. Perhaps I've been wrong about this, but there doesn't seem to be any reason for Gerhard Gentzen's sequent calculus to make use of sequences of formulae.
Let me try to clarify what I mean here. A sequent, for Gentzen, is a special inference expression connecting a (possibly empty) sequence of antecedent formulae with at least one consequent formula. The system for intuitionistic logic requires just one consequent formula, while the classical system allows a sequence in the consequent. The sequent calculus is then a way of defining classical or intuitionistic logic as a scheme of inferences among sequent expressions rather than the formulae within. Baez and Stay (2009) nicely explain that Gentzen used sequents so he could develop a logical calculus that has the subformula property, which has in turn led to so many useful developments. But that only requires sequent expressions connecting sets of formulae, not sequences of formulae.
I feel there remains the question, why did Gentzen insist that the antecedent and consequent of a sequent be a sequence of formulae? He immediately had to compensate for this by invoking the structural rules, special rules that eliminate the sensitivity of his systems to the sequence structure. He did this, of course, because classical and intuitionistic logic aren't sensitive to the structure of formulae occurring in a sequence. In fact, later authors relying on Gentzen to present classical or intuitionistic logic have frequently just gone ahead and redefined sequents as special expressions connecting sets of formulae, thus doing away with the structural rules. Logicians more recently have played extensively with the logics that result from not using one or more of the structural rules---these are the substructural logics, which are used in type-logical grammar, among other applications. But Gentzen didn't suggest doing away with any structural rules, so far as I know. So then, why did he insist that formulae came in sequences, only to turn around and insert provisions that eliminated this sensitivity? We certainly have to thank him for his odd bit of foresight, given how much fruitful research has been done using substructural logics in recent times.
Subscribe to:
Post Comments (Atom)
Hi Sean! It's good to find your blog.
ReplyDeleteI have always thought that Gentzen's favouring sequences of formulas over sets was due to a kind of Hilbertian foundationalism: sequences can be taken to be concrete objects presented simply by writing them down in a way that a set could be thought to be a little more abstract, and hence, a little more questionable. Finite sequences could be seen to be acceptable for a project of finitist reduction, without causing pause in the manner that sets might.
However, that's always been a suspicion rather than anything stronger.
Wow, Greg,
ReplyDeletewhat a nice surprise to find you here. I remember when I was working to revise my dissertation many years ago, I wished I had your book on substructural logic to refer to while I was writing it the first time through.
Anyway, I appreciate your interesting conjecture concerning Gentzen's sequents. I hadn't thought of it in the proper historical context, as an example of a finitist system.