[FOM] question about Cook and Gentzen
Michael Kremer
kremer at uchicago.edu
Wed Sep 8 16:51:08 EDT 2004
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
More information about the FOM
mailing list