14 Sep 2007 04:48

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

```

Gmane