Re: Re: Deep cirquent calculus

Dear Giorgi and Alessio,

Let me add, that in CoS, you can also have polynomial size proofs of PHP 
without using the finitary cuts that Alessio was mentioning:

Alessio wrote:
> Now, the atomic cuts you get are analytic (in your sense), and so you 
> have analytic polynomial proofs of pigeonhole. In fact, you have cuts of 
> this shape
>
>    C(a ^ -a)
>    --------- ,   where a appears in C{ }.
>      C{f}
>
> We call these cuts finitary cuts.

Avoiding this cut is done by adding a different version of the extenstion 
rule as it is done in the paper by Paola and Alessio: 
<http://cs.bath.ac.uk/ag/p/PrComplDI.pdf>

The rule I have in mind is

   C{a_i}
   ------
   C{A_i}

(with the usual side conditions for the extension rule)

This rule can be used independently from the cut, and can simulate exactly 
the sharing or cirquents. Conversly, cirquents are a way to hide the 
additional proposional variables used by the extension rule (or 
equivalently, the substitution rule), i.e., instead of adding 
abbreviations a_i for formulas A_i, you use sharing nodes.

-Lutz

PS: see also the previous messages:
http://article.gmane.org/gmane.science.mathematics.frogs/446
http://article.gmane.org/gmane.science.mathematics.frogs/450