[FOM] Re: The rule of generalization in FOL

[Timothy Y. Chow]

On Thu, 9 Sep 2004, Arnon Avron wrote:
> Tim Chow wrote:
> 
> > Let A(b) denote a formula with free 
> > variable b.  Then we have the rule
> > 
> >       X  ->  Y, A(b)
> >  ------------------------
> >  X  ->  Y, forall x: A(x)
> > 
> > provided that b does not occur free in Y.  
> 
> b should not occur free in X either (otherwise you can prove 
> invalid sequents), and this is the standard =>\forall rule, as originally
> formulated by Gentzen.

Yes, sorry, I misread Cook's notes.  He does say that b should not occur 
free in either X or Y.  (Since a formula can move freely between X and Y
just by adding a "not" sign in front, it's obvious that the condition has
to hold for both X and Y.)

However, I'm still confused about the question of logical consequence.
Rereading my last article, I see that I wasn't sufficiently clear about
my question.  As I said before, Cook's notes define "phi is a logical 
consequence of psi" to hold iff for all structures M and all 
interpretations sigma, if M |= psi[sigma] then M |= phi[sigma].
Under this definition, the bottom *sequent* in the above rule is not
a logical consequence of the top *sequent*.  (Stephen Cook just confirmed
this himself in his last FOM message.  Michael Kremer was probably misled
by my failure to clarify that it was the "vertical" sequent-to-sequent
direction that I was referring to, not the "horizontal" direction.)

What I'm wondering is, if Gentzen's calculus is being used, wouldn't it 
make more sense to redefine logical consequence so that the bottom sequent 
*is* a logical consequence of the top sequent?  That is, if I understand
your terminology correctly, to use the "validity" consequence relation?
Stephen Cook almost seems to suggest this when pointing out that the 
universal closure of the bottom sequent is a logical consequence of the 
universal closure of the top sequent.

Tim