Re: Deep cirquent calculus

Guten Tag (or bon jour?), Lutz.

> This rule [extension] ... can simulate exactly the sharing or cirquents. 

Generally speaking, this is not so. Let me point out two things:

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 foresee that 
the ability to differentiate between shared and unshared nodes will become 
even more crucial when one tries to capture additive- and exponential-style 
(as seen in computability logic) connectives. E.g., semantically an additive 
gate shared between two parents is not the same as two separate additive getes 
(with the same content), one per parent. In the case of CL8, this is only true 
for terminals but not gates, which is accounted for by the presence of 
globalization and its dual, allowing us to merge or separate gates (but not 
terminals) at will. The same rule would have to be absent for additive gates. 

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. And iterating this effect might produce an exponential slowdown. Well, 
one cannot rule out that there are some ways around, but at least this is not 
obvious.

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.  

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?