[FOM] question about Cook and Gentzen

[Michael Kremer]

I haven't read Cook's notes, but...

The rule should be subject to the following restrictions:  b does not occur 
free in X, Y, or for all x:A(x) (also, b must be "free for x in A(x)" in 
the sense that there is no free occurrence of x in A(x) within the scope of 
a quantifier binding b).  As thus stated the rule does preserve logical 
consequence, as defined by you later.  (More precisely:  the definition of 
logical consequence for finite sequences X, Y should be:  Y is a 
consequence of X iff for all structures M and assignments to free variables 
sigma, if M |= psi[sigma] for all psi in X then M |= phi[sigma] for some 
phi in Y -- this is the proper definition to use when working with 
Gentzen's sequent calculus).

--Michael Kremer

Tim Chow wrote:
>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
>_______________________________________________
>FOM mailing list
>FOM at cs.nyu.edu
>http://www.cs.nyu.edu/mailman/listinfo/fom