Re: Deep inference and speed-up in proof search

At 13:23 +0200 13.8.04, Lutz Strassburger wrote:

> I would like to make some clarifying
> comments on Alessio's example.
> 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.

Hey clarifier! The size of Gn looks quadratic to me. If we agree on this, the other comments you make on the size are also wrong.

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

I also maintain my statement that the secret of success is CoS absence of branching. This is a moral statement, and we can disagree on this, but my reasons are as follow. What do you mean by `if one builds in associativity and commutativity in the sequent calculus'? You can't do that *precisely* because of the *branching* nature of conjunction in the sequent calculus.

You can mimic my proof only *after* having transformed the original Gn formula into a suitable one. The only way you can do this by the sequent calculus (as we know and love it) is by using cuts (and I don't even enter into the business of assessing the complexity here, since the point is not using cuts).

But then, why not going ahead and build into the sequent calculus also some simplification mechanism, like distributivity laws? They would work well in this case.

If you think to all this business from the point of view of the subformula property, what you (should) see is that the sequent calculus would need the same notion that we have: instead of tearing apart pieces of formulae in branches, it would need to build new formulae from pieces of old ones. This is again, precisely, the absence of branching, and not just built-in associativity.

Finally, my remark was (I thought obviously) about CoS: in computing the complexity *for CoS*, one has to take into account the cost of associativity, which, contrary to the sequent calculus, is hidden in the use of equations. I guess I'm not wrong if I estimate this cost to be at most linear in n (do you agree?), and so, it doesn't change the fact that we have an exponential speed-up.

-Alessio