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

Alessio Guglielmi Alessio.Guglielmi at inf.tu-dresden.de
Thu Sep 16 09:14:56 EDT 2004

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

```