Re: Deep inference and speed-up in proof search

Hello,

I would like to make some clarifying comments on Alessio's example.

> POLYNOMIAL CUT-FREE PROVABILITY OF A CLASS OF TAUTOLOGIES
> ---------------------------------------------------------
>
> We start from propositional variables ci and di, for i >= 1.  We then
> define:
>
>         k
>   Fk = /\ (cj V dj) ,   for k >= 1 ;
>        j=1
>
>   A1 = c1 ;
>   B1 = d1 ;
>   ...
>   A{i+1} = Fi -> c{i+1} ;
>   B{i+1} = Fi -> d{i+1} ;
>
>   Gn = ((A1 V B1) ^ ... ^ (An V Bn)) -> (cn V dn) .
>

An important observation to make here is that the size of the formulas Gn 
(that is the number of atoms in it)  is exponential in n. That means that 
the size of any proof of Gn (if we count the number of symbols) must also 
be exponential in n. We should therefore measure the size of the proof wrt 
the size of Gn.

> In the cut free CoS system KS, there are linear proofs.  I show just
> an example for G3 but the general pattern is the same (the syntax 
> below
> is the CoS one):
>
>                 t
>     i_ -------------------
>        [(-c3,-d3) , c3,d3]
>   2*i_ ------------------------------------------------
>        [([c2,d2,(-c2,-d2)],-c3,[c2,d2,(-c2,-d2)],-d3) ,
>         c3,d3]
>    2*s ------------------------------------------------
>        [(-c2,-d2),(-c2,-d2) ,
>         ([c2,d2],-c3,[c2,d2],-d3) ,
>         c3,d3]
>   1*c_ ----------------------------
>        [(-c2,-d2) ,
>         ([c2,d2],-c3,[c2,d2],-d3) ,
>         c3,d3]
>   4*i_ ------------------------------------------------------------
>        [([c1,d1,(-c1,-d1)],-c2,[c1,d1,(-c1,-d1)],-d2) ,
>         ([c1,d1,(-c1,-d1)],[c2,d2],-c3,[c1,d1,(-c1,-d1)],[c2,d2],-d3),
>         c3,d3]
>    4*s ----------------------------------------------------------
>        [(-c1,-d1),(-c1,-d1),(-c1,-d1),(-c1,-d1) ,
>         ([c1,d1],-c2,[c1,d1],-d2) ,
>         ([c1,d1],[c2,d2],-c3,[c1,d1],[c2,d2],-d3) ,
>         c3,d3]
>   3*c_ -------------------------------------------- .
>        [(-c1,-d1) ,
>         ([c1,d1],-c2,[c1,d1],-d2) ,
>         ([c1,d1],[c2,d2],-c3,[c1,d1],[c2,d2],-d3) ,
>         c3,d3]
>

The size of the CoS proof (that is the number of rule instances) for Gn 
is quadratic in the size of Gn.

Let us now look at the sequent calculus.

> The following is a possible proof, of which one branch is shown in part
> (all the others are similar):
>
>                                  .
>                                  .
>                                  .
>   ----------------------------------------------------------------
>   |- -c1 , (c1 V d1) ^ -d2 , (c1 V d1) ^ (c2 V d2) ^ -c3 , c3 , d3
>                  =
>       |- -A1, -B2, -A3, c3, d3
>       ------------------------
>                  .                           .      .      .
>             .    .    .                        .    .    .
>               .  .  .                            .  .  .
>                 ...                                ...
>   --------------------------------   --------------------------------
>   |- -A1, -A2^-B2, -A3^-B3, c3, d3   |- -B1, -A2^-B2, -A3^-B3, c3, d3
>   -------------------------------------------------------------------
>   |- -A1^-B1, -A2^-B2, -A3^-B3, c3, d3
>
> Clearly, for Gn there are 2^n branches.  Statman [*] proved that in a
> cut free system the size of proofs always grows exponentially with n.

From the argumentation in Alessio's mail it only follows that the size of 
the proof (again, the number of rule instances) is exponential in n, 
because there are 2^n branches. But observe that the height of each branch 
is polynomial in n.

Hence, with this naive argumentation we did not get any speed-up. However, 
I am sure we can show that the size of the cut-free sequent calculus proof 
must be exponential in the size of Gn (I have right now no access to the 
paper by Statman, so I cannot say what he actually did).
The reason is that the sequent calculus makes a lot of duplications that 
are not necessary and that are not done in the CoS.

> The secret of success here is, of course, the absence of branching in 
> CoS.

No.
In this particular example the branching is innocent. The evil is hidden 
in the associativity and the commutativity. If you build in associativity 
and commutativity for conjunction in the sequent calculus, you can mimic 
the CoS proof, because then

A3^B3 = ((c1 V d1) ^ (c2 V d2) ^ -c3) ^ ((c1 V d1) ^ (c2 V d2) ^ -d3)
       = (c1 V d1) ^ (c1 V d1) ^ (c2 V d2) ^ (c2 V d2) ^ -c3 ^ -d3

and you can split this anywhere and not only at the conjunction between A3 
and B3.

However, there are examples where this is not sufficient, and where one 
really has to bring parts of formulas deep inside other formulas and apply 
the identity deep inside, in order to avoid unnecessary duplications.

> Remark: to be precise, one has to be more careful than I was with
> parentheses and associativity; however, in all the arguments above, the
> substance would not change.

This is an important point. Although in this example the sequent calculus 
can mimic the short CoS proof if there is access to associativity and
commutativity, the CoS could also provide a short proof if there were 
no access to associativity and commutativity. And the reason is deep 
inference.

-Lutz