[FOM] Re: The rule of generalization in FOL

[Arnon Avron]

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.

> 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?

LK (or any other Gentzen-type calculus) is just a calculus. It can 
(and should) be *used* to characterize consequence relations. Now
there are two major methods for doing this that can be found 
in the literature:

1) Define that B follows from A_1,..., A_n iff the sequent A_1,..., A_n=>B
is a theorem of G.

  If G is LK than the resulting consequence relation is the "truth"
consequence relation of classical logica (thus A=>\forall x A is in general
not a theorem of G)

2) Define that B follows from A_1,..., A_n iff the singleton sequent =>B
is derivable in G from the n singleton premises =>A_1 ... => A_n (using 
the axioms and rules of G, *including cut*). 

 If G is LK than the resulting consequence relation is the "validity"
consequence relation of classical logica (thus =>\forall x A *is*
derivable from =>A in LK).

  The source of the confusion is that from a "horizontal" point of view,
sequents reflect the truth consequence relation between *formulas*r. 
However,  viewed from a "vertical" point of view, the rules of LK
preserve validity of sequents in Structures, not their truth given 
a structure and an assignment (by truth/validity of a sequent I mean the
truth/validity of its standard translation into a formula of the language).
Hence a *sequent* is provable from other *sequents* iff it follows
from them according to the validity consequence relation. In fact, I
know no Gentzen-type system for classical logic in which all the rules
preserve truth of sequents. 

So the answer to your question is that only this method works (or so
it seems).


Arnon Avron