Re: Deep inference and speed-up in proof search

On Sat, 14 Aug 2004, Alessio Guglielmi wrote:

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

I think we just have a misunderstanding here. We agree on all points. 
Morally the "absence of branching" or the "absence of mismatch" is the 
reason for the speed-up. All I was trying to say is that the particular 
example you showed does not make this 100% clear.

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

I am working on it.

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

I am working on that too.

-Lutz