RE: Re: Deep cirquent calculus

Hello,

I elaborate a bit on why I see cirquents as a welcome advance.

Rhetorical question: what is the most natural representation of 
boolean functions, formulae or circuits?

Many of us are in the business of eliminating bureaucracy from proofs 
to get to their essence, so, why not eliminating bureaucracy also 
from formulae and use circuits instead? Of course, one has to prove 
that circuits are convenient enough for whatever purpose one wants to 
use them, and we still have to see whether a proof theory can be 
developed for them. But the fact remains that they are a more natural 
starting point than formulae.

I thought about using them in the place of formulae in the past, but 
did not do it because I had no further motivation than their 
naturalness, and it was already difficult enough to make the 
community accept deep inference. However, Giorgi now has external, 
semantic justification for using circuits, and, in addition, he finds 
that deep inference is the natural proof methodology for them. I see 
this as a very welcome development.

I am convinced that this is not a slightly different syntax from the 
calculus of structures. I remember very well when people were saying 
the same about deep inference vs the sequent calculus, usually 
without thinking much before talking.

Perhaps it will turn out that CoS + some extension can p-simulate 
cirquents. I don't think that this will be easy, if at all possible. 
Anyway, I insist that the point is that circuits are less 
bureaucratic then formulae.

I would like to add that I find Lutz's argument in support of the 
extension rule very unsatisfying. Perhaps he is right on a purely 
technical level, and limited to the cirquent system that Giorgi shows 
in his paper, but there is anyway a difficulty ahead, which I'll try 
to explain here.

Let's start from the CoS derivation

     [(B [A C] D) ([A C] D E)]
   s -------------------------
      [A (B [A C] D) (C D E)]
    s -----------------------
       [A A (B C D) (C D E)]
    c^ --------------------- .
        [A (B C D) (C D E)]

Let's see now how this derivation might look like with circuits:

   A   C
    \ /
     V   D
      \ /
   B   ^   E
    \ / \ /
     ^   ^
      \ /
       V
   ---------- .
     C   D
      \ /
   B   ^   E
    \ / \ /
     ^ A ^
      \|/
       V

It should be clear that circuits can do in one shot and without 
duplication what CoS does essentially in two steps with duplication. 
This mechanism can obviously produce an exponential proof compression 
in the circuits case, when subjected to recursion. If we try to 
simulate circuits with Tseitin extension, and so, by giving a name to 
the shared parts, we find ourselves with something like

   B a   a E   C   D
    \|   |/     \ /
     ^ A ^   a   ^
      \|/     \ /
       V      <-> .
        \     /
         \   /
          \ /
           ^

How can we design a reasonable inference rule that carries A in a 
disjunction next to C, without duplicating anything?

Perhaps I'm missing something, please correct me if I'm wrong.

There are pending questions by Giorgi. I'll set the good example and 
think some more  before answering.

Ciao,

-Alessio