Re: Deep inference and speed-up in proof search

At 18:21 +0200 13.8.04, Lutz Strassburger wrote:
>  > 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).
>
>Again, in general this is true. But in the case at hand all you need to do is
>dropping all the parentheses whenever you have nested conjunctions, as you
>actually did it. This is what I meant by "building in associativity".
>However, as soon as there are more conjunction-disjunction alternations, it
>doesn't work anymore.

You can't build a deduction system where you 
`drop parentheses' simply like this. It would 
only work for this example! So, since you can't 
do it in general, I still don't see your point.

Or do you mean to conceive an entirely new proof 
theory where you also have a meta connective for 
conjunction, like the display calculus? In that 
case, it wouldn't be the sequent calculus and 
again I don't see your point.

Like in our example, no matter the hypothesis, 
the conclusion is the same: I don't see your 
point.

Perhaps another way of saying what I said, namely 
that the secret of success is absence of 
branching, could be saying `absence of mismatch' 
(between object and meta level). I don't want to 
say it this way to the non-initiated because 
talking about mismatch is difficult, while 
talking about branching is immediately 
understandable.

>  > 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.
>
>Distributivity is duplicating stuff...

I didn't mean to be taken seriously, but then, 
also considering sequents as sets is duplicating 
stuff.

>You know that I agree with you on all these points. All I wanted to point out
>is that there are several sources of the speed-up wrt. the sequent calculus.
>And your example explores only a very little one.

Thanks for the encouragement.

However, I'm not sure there are so many sources, 
I see only two: absence of branching (or absence 
of mismatch) and deep application of rules, which 
are the two distinguishing features of deep 
inference wrt shallow inference (it is worth 
reminding here that Schuette's calculus has deep 
application of rules but it's still branching).

My example is about showing why absence of 
branching works, and I think it does it well 
enough. One complaint I have is that it's not as 
simple as I would like it to be, but it's the 
simplest I could find so far. Another complaint 
is that this example is artificially made up (by 
Statman, I guess) precisely for showing a 
weakness of the sequent calculus, and of course I 
would prefer to resort to a natural, independent 
class of formulae. (Pigeonhole is more natural, 
but unfortunately much too complicated for being 
an introductory example.)

Can you, or anybody else on Frogs, contribute a simpler example?

And: can you contribute a simple example that 
shows how deep application of rules makes for an 
exponential speed-up, and perhaps also for 
polynomial proofs?

As for the general picture: as I said, I know 
already how to transform *every* proof (with or 
without cuts) in the sequent calculus into a 
proof in CoS with the same complexity, modulo a 
polynomial (as measured wrt to the size of 
tautologies of any class), in such a way that no 
infinitary rule is necessary (so, no real cuts).

I promised a post to Frogs about that, but it's 
such a simple matter that I will give the recipe 
here. The necessary transformations are outlined 
in [KB] and [BG]: 1) transform a proof with cuts 
in the sequent calculus into a proof in system 
SKS (see [KB], Theorem 2.3.3); 2) transform this 
proof into one that only employs finite choice 
cuts ([BG], Section 3).

For this transformation to work, absence of 
branching and deep application of rules are both 
essential. So, it does make the point in a very 
general way, also because the complexity industry 
already produced polynomial proofs for several 
classes of tautologies, including pigeonhole, if 
I'm not wrong.

On the conceptual level, this is already rather 
good, in my opinion. That said, there should be 
possibilities of improving this result by making 
it stricter, especially by reducing 
nondeterminism. This is what I'd like to see 
explored in the future, and I think there's a lot 
to do and to say here.

-Alessio


[BG] Kai Brünnler and Alessio Guglielmi. A first 
order system with finite choice of premises. In 
Hendricks et al., editors, First-Order Logic 
Revisited. Logos Verlag, Berlin, 2004. URL: 
http://www.iam.unibe.ch/~kai/Papers/FinitaryFOL.pdf.

[KB] Kai Brünnler. Deep inference and symmetry in 
classical proofs. PhD thesis, Technische 
Universität Dresden, 2003. URL: 
http://www.iam.unibe.ch/~kai/Papers/phd.pdf.