Re:Back to computability logic

At 19:26 -0400 28/6/05, Giorgi Japaridze wrote:
>Hello everyone. About a year ago we have collectively attempted but
>failed to axiomatize various fragments of computability logic. Finding
>good deductive systems for computability logic has been on the problems
>list of the main CoS webpage since then. I see a light at the end of
>the tunnel in the paper advertised below.  Its last paragraph kinda
>contains a marriage proposal to CoS, so I'd be curious to know how the
>other party feels before going any farther.
>
>The preprint is available at http://arxiv.org/abs/math.LO/0506553

Hi Giorgi and everybody,

I didn't answer before because I was away from email, but I managed 
to print your paper before leaving and I'm enthusiastic about this 
new development, despite only having a superficial reading of it 
(sorry for that, I couldn't really find the time).

However, I think I know enough to say that your notion of sharing is 
elegant and new, and I'm very intrigued by your ability to deal with 
binary tautologies. This logic reminds me a bit of pomset logic, in 
the sense of being a very hard nut to crack. Pomset logic led us to 
deep inference; if binary tautologies do something similar it would 
be fantastic, I think. I encourage everybody to read this paper and 
share opinions. It `smells' good to me.

The question now is whether one can do proof theory with the cirquent 
calculus. I cannot say I understand your system (with my guts, I 
mean), but I'll play with it as soon as I can. Unfortunately, it 
won't be very soon, because I'm relocating. If anybody finds 
anything, I'd be happy to know.

Question: how does cut elimination for CL5 look like? Of course, one 
has to design a cut rule, but I guess the obvious degeneration of 
your and-introduction would do fine.

I'm not sure the marriage with CoS could work easily. My very 
preliminary impression is that your system's unique feature (sharing) 
could be somehow adopted by CoS (or other deep inference formalisms). 
However, the cirquent calculus still has a separation between object 
and meta-level, what breaks with one of the fundamental tenets of 
deep inference.

The way I would proceed myself would be to start from CoS (or wired 
deduction, my last pet) and see how to design sharing. What could a 
geometrical notion of sharing be? Then, I would try a cut elimination.

Maybe, you might try starting from the cirquent rules you have and 
try to make them local following the CoS guidelines, what should 
force you to adopt some notion of deep inference.

I don't know, it's too early to say. I think this thing will develop. 
By the way, this would be another confirmation that good proof theory 
comes from semantics. There always is an independent structure behind 
good design.

It would be interesting to discuss in person, can you make it to Lisbon?

Ciao,

-Alessio