[FOM] Re: [FOThe meaning and use of Gentzen-type rules

[Arnon Avron]

On Fri, September 10, Michael Kremer wrote:

> I suggest that the right way to understand -> is as a relational sign 
> in the metalanguage.  X -> Y asserts that Y is a logical consequence of X, 
> in the sense explained in my previous posting.

To be precise:  X -> Y (in your notation. I am used to use -> as 
the object-language connective, and => for separating the two sides 
of a sequent)  can be interpreted as asserting that Y is a 
logical consequence of X according to the *"truth"* consequence relation
(maybe this name is not very good, because the word "truth" is overloaded,
but I am used to it). There is no single notion of "logical consequence".

> Under this interpretation, the rules of the sequent calculus preserve not 
> only validity (as Avron claims) but truth.  

I am afraid that there is a confusion here, caused perhaps by an
unfortunate choice of names on my part. In what I wrote I used
the word "truth" in a very specific, technical meaning: I meant
"A is true for a pair <M,v>, where v is a valuation in M" as synonymous 
with "A is satisfied by the pair <M,v>". I then just noteD the following 
fact: if one translates a sequent G to to a formula A(G) (e.g.:
if G is A_1,...,A_n -> B_1,...,B_k then A(G) might be taken to be
-A_1\/...\/-A_n\/B_1\/...\/B_k) then:

1) It is not always the case that if G is derivable from G_1, ..., G_n
in LK than A_(G) is true for every pair <M,v> for which 
A(G_1), ..., A(G_n) are all true.

2) It is the case  that if G is derivable from G_1, ..., G_n
in LK than A_(G) is valid in every structure M  in which 
A(G_1), ..., A(G_n) are all valid.

Moreover, I know no Gentzen-type system for classical logic
that preserve truth *in the specific technical sense of 1)*.

>  My point is that we can understand the sequent calculus by 
> understanding the individual sequents as making *assertions of "local" 
> validity* and then we can understand the moves from sequent to sequent as 
> themselves valid.

The moves are indeed valid according to this interpretation, as well
as according to the interpretation given in 2) above. However, I think
that understanding the individual sequents as making *assertions of "local"
validity is inferior to the understanding provided by 2) (as preserving
validity of sequents in structures, not just logical validity of sequents).
The reason is that unlike the latter, the former provides meaning only 
to *pure* proofs in Gentzen-tpe calculi, not to proofs from premisses 
(by this I mean proofs in which 
a sequent can be derived from a set of other, not necessarily valid, sequents).
However, proofs from premises in such calculi  have a lot of applications.
Thus already when dealing with FOL with identity, it is more convenient
to employ in proofs premises consisting of equalities than to 
use pure proofs (see Girard's book on Proof Theory). Moreover: the 
whole resolution calculus is based on
inferring non-valid clauses from other non-valid clauses (note that
clauses  are nothing but sequents consisting solely of atomic formulas).
In fact, the completeness of the resolution rule (in the sense it is
complete) is an easy corollary of the following  generalization
(for proofs from premises) of the original cut elimination theorem:

If G is derivable  from a set S of premises in LK+substitution
then there is a proof of G from S in which
all cuts are on instances of formulas occuring in S. 

(details can be found in my paper: "Gentzen-type Systems, Resolution
and Tableaux", Journal of Automated Reasoning, vol. 10: 265-281, 1993).

Because of the jewish new year and a trip, I am taking a two-weeks break
from FOM. I wish everybody a happy, peaceful  new  year!

Arnon Avron