Re: Re: Deep cirquent calculus

Dear Giorgi,

On Fri, 14 Sep 2007, Giorgi Japaridze wrote:

> > This rule [extension] ... can simulate exactly the sharing or cirquents.
>
> Generally speaking, this is not so. Let me point out two things:

I am sorry, but I think that here we have something where we disagree.

> POINT 1. Cirquents are generally more expressive and flexible than 
> formalisms without sharing. For example, they allow us to capture binary 
> tautologies that other systems fail to axiomatize (after all, it should 
> be remembered that this was the original impulse for introducing 
> cirquent calculus).

I guess you mean balanced tautologies where each atom occurs once positive 
and once negative. Then, what do you mean by "capturing these objects"? I 
am sure you are aware of the fact that testing such a formula for being a 
tautology is coNP-complete. So, you certainly do not have a polynomial 
proof system for them (otherwise you would be famous by now).

You should give some clarification.

> POINT 2. As for proof efficiency, here I again doubt that extension or 
> substitution can fully simulate sharing. Imagine a large component A 
> shared between n different parents in a cirquent. And imagine a given 
> stage of a proof transforms (only) A. In cirquent calculus, such a 
> transformation would have to be performed only once, within the single 
> shared copy of A. But with substitution or extension (used to abbreviate 
> A), without sharing, the identical transformation will have to be 
> performed n times, once per each parent.

No. That's the whole point of the extension, since there is nothing you 
can do to transform a formula consisting of only one atom.

> And iterating this effect might produce an exponential slowdown.

This is exacly the reason why "Frege + extension" is supposed to be better 
than "Frege without extension"

> Well, one cannot rule out that there are some ways around, but at least 
> this is not obvious.

Right. Nobody knows. But I still claim that your sharing does exactly the 
same as the extension rule. This might not be entirely obvious when you 
look at Frege systems. But it is obvious when you look at CoS + extention.

> However, what you say is indeed true for the particular case of the 
> pigeonhole proof given in my paper. Because there, by good luck, no 
> transformations are taking place inside shared components, with such 
> components being just "archival" ones. That is, sharing is used for 
> reducing the otherwise exponential sizes of formulas (and this effect 
> can indeed be simulated by extension), but not for reducing the number 
> of steps in the proof which is polynomial anyway.

I don't think PHP is so "particular" in that respect.

> Anyway, I was cautious enough in Section 7 to only say that the given 
> pigeonhole proof illustrated a speedup over "traditional systems", with 
> CoS+extension obviously not counting as such. That proof can apparently 
> serve the cause of promoting not only cirquent calculus, but also 
> promoting --- even if less directly --- CoS and deep inference in 
> general.
>
> The quesion about whether my pigeonhole proof brings to light any moral 
> differences between CL8 and CoS+extension, again, comes down to how one 
> understands analyticity. Do you folks see CL8 as an analytic system? If 
> not, what is that makes it non-analytic (as opposed to the analytic 
> CoS)? And if yes, is CoS with extension or finitary cut also analytic? 
> Or... perhaps it is time to forget analyticity altogether as an 
> old-fashioned concept, meaningful only in the context of sequent 
> calculus?

Honestly, I do not care much about "traditional" vs "non-traditional", or 
"analytic" vs "non-analytic". Alessio has mentioned some of the reasons in 
his previous mail to that list.

All I am saying is that we should not insist on differences where in fact 
we have only a slightly different syntax for the thing.

Ciao,
Lutz