[FOM] Re: The rule of generalization in FOL

[Stephen Cook]

I saw my name mentioned, so I will make a brief reply to
Timothy Chow:

Although it is true that for two of the LK rules the bottom
may not be a logical consequence of the top, nevertheless
for all rules the universal closure of the bottom is always
a logical consequence of the universal closure(s) of the top.

So to extract meaning from a line in an LK proof, think of the
free variables as being universally quantified.

Stephen Cook


	 This reminds me of something that's been bothering me lately.  I've be
	en 
	 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 fre
	e 
	 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 rei
	ning 
	 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