[FOM] chow and avron on generalization in the sequent calculus

[Michael Kremer]

Tim Chow and Arnon Avron:

It seems to me the issue that's been worrying you, whether and in what 
sense the rules of the sequent calculus are valid, can be avoided if one 
properly interprets the "->" used in Gentzen's sequents.  Gentzen uses a 
*different* sign for the material implication of his object 
language.  Let's use => for this, and -> for the sequent sign.  Then, for 
example, this is the => introduction rule on the right:

A,X -> Y,B
-----------------
X -> Y, A=>B

Now we should note that => is a connective of the object-language, but -> 
isn't.  In particular, -> can't be iterated, whereas => can.

Then I suggest that the right way to understand -> is as a relational sign 
in the metalanguage.  X -> Y asserts that Y is a logical consequence of X, 
in the sense explained in my previous posting.

Under this interpretation, the rules of the sequent calculus preserve not 
only validity (as Avron claims) but truth.  Thus the rule of forall 
introduction on the right, which we have been discussing, preserves truth, 
in the following sense.  If Y, A(b) is a logical consequence of X (which is 
what X -> Y, A(b) asserts, on this interpretation), and b does not occur 
free in X, Y, or forall x A(x), and b is free for x in A(x), then Y, forall 
x A(x) is a logical consequence of X (which is what X -> Y, forall x A(x) 
asserts, on this interpretation).

I don't claim any originality for any of this.  I think this is one 
standard way to think about what is going on in the sequent calculus.  It's 
certainly how I was taught to think about it (and always have thought about 
it).

I don't mean by any of this to be disputing the useful distinction (made on 
the list first by Avron I think) between two different notions of logical 
consequence in the presence of variables (later called local and global 
validity).  My point is that we can understand the sequent calculus by 
understanding the individual sequents as making *assertions of "local" 
validity* and then we can understand the moves from sequent to sequent as 
themselves valid.

--Michael Kremer