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

[Alessio Guglielmi]

Hello,

At 11:48 +0300 14.9.04, Arnon Avron wrote:
>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)*.

I'd like to make an observation here.

As I think it has been noted already, the situation is similar for 
certain rules involving modalities. For example, in linear logic, the 
`promotion' rule

    ?Gamma, A
    ----------
    ?Gamma, !A

is sound but

    (?Gamma # A) -o (?Gamma # !A)

does not hold (here Gamma is a multiset of formulae, # is par and -o 
is linear implication). Analogous situations happen in modal logic.

So, there is a mismatch between making inferences and implications, 
and this mismatch does not just involve variables, since it happens 
in propositional logics as well. It can be understood analogously 
with frame semantics, but then my question is whether we are really 
happy with justifying the problem, or wouldn't we be happier by 
getting rid of it? Isn't it (at the very least aesthetically) 
disturbing that most inference rules present no mismatch, while only 
a few do?

However, there are also technical issues involved, not just 
aesthetical ones. For example, there is, in fact, another disturbing 
coincidence here: the `mismatch rules' require some sort of non-local 
condition on sequents for their being applicable: the universal 
quantification rule needs a check for a variable to be free, the 
promotion rule above needs a check for all formulae in Gamma to be 
modalised by ?. (This is already a departure from the pure form of 
Gentzen-type systems.)

Now, to get to the point: it seems unlikely to me that a Gentzen-type 
system can be designed where this mismatch does not appear. In fact, 
I take the mismatch (and the non-locality of rules) as evidence of an 
*inherent* problem of Gentzen-type systems. The problem is in their 
being based on *shallow inference*, while moving to *deep inference* 
provides for a solution, which is completely satisfying (in my 
opinion) because it retains the essential characteristics of 
Gentzen-type systems.

Without getting into the technicalities of deep inference (which you 
can find at <http://alessio.guglielmi.name/res/cos>), let me just 
show the rules corresponding to universal quantification and 
promotion:

     FA x.(A v B)           !(A # B)
    ---------------   and   -------- .
    FA x.A v EX x.B         !A # ?B

The first rule corresponds to Quine's axiom (mentioned already here 
by Charles Parsons), the second one has been found by Lutz 
Strassburger.

These rules have no mismatch and are local. Moreover, they are 
similar to all other rules one naturally designs in deep inference: 
connectives, quantifiers and modalities are defined in dual pairs 
instead of in isolation, and all with the same, simple pattern shown 
above. The scheme works for classical, linear and modal logics, 
including those that are `difficult' for Gentzen-type systems, like 
S5.

The crucial idea is that, instead of distinguishing an object and a 
meta level (as in shallow inference), everything is done at the 
object level (deep inference) *by taking care of preserving the 
subformula property*.

Well, I don't want to make this email too long. Just know that it is 
possible to do proof theory without the mismatch, and it's actually 
very pleasant, both aesthetically and technically.

Ciao,

-Alessio