[FOM] Re: The rule of generalization in FOL

[Timothy Y. Chow]

Arnon Avron wrote:
>there is no single "First Order Logic", but there are TWO different ones.

This reminds me of something that's been bothering me lately.  I've been 
reading Stephen Cook's excellent course notes for CSC 2429H: "Proof 
complexity and bounded arithmetic."  He gives a version of Gentzen's
systems PK and LK.  What surprises me is that one (or two, depending
on whether you think forall is an abbreviation for ~exists~ or not) of
the LK sequent calculus rules does *not* preserve logical consequence,
as defined a few pages earlier.

The rule in question is this.  Let X and Y denote arbitrary finite 
sequences of first-order formulas.  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.  On the other hand, "phi is a 
logical consequence of psi" is defined to hold iff for all structures M
and all interpretations sigma, if M |= psi[sigma] then M |= phi[sigma].

Working with this system makes my head spin because I have to keep reining 
in my natural urge to interchange derivability and logical consequence.
My question is, what is the compensating advantage of this system that 
makes this apparent mismatch worthwhile?

Tim