Re: Computability Logic

Dear Giorgi,

thanks to your counterexample, now I see the problem of my rule for 
(a). I checked what you posted and it looks correct to me.

I thought a bit about how to fix the problem, but so far I found 
nothing. I'll keep thinking to this, but in the meantime perhaps you 
can help.

It probably was obvious, but maybe it helps stating what I'm trying 
to do. The main trick of the trade when dealing with deep inference 
in CoS is trying to get rules that do as little as possible. In other 
words, instead of having a rule that gets to a conclusion by juggling 
a lot of complicated premises, we look for rules that do minimal 
interventions.

As a consequence, many rule instances become necessary in place of 
just one, and it might happen that their semantic interpretation is 
not the most obvious. On the other hand, this way you get more proof 
theoretical properties, because you deal with small atoms instead of 
big proteins, and you can recombine them in many more ways.

So, the question is: could you simplify your rule (a) in such a way 
that the number of premises involved is bounded? It would not be a 
problem having several `small' rules in the place of (a).

After reading your counterexample, I also started noticing the 
subtlety of the stability condition. Right now, I think doing it our 
way might be very challenging, at least if we don't want to introduce 
some sort of modalities into your logic (we don't want, I guess!). 
It's easy to duplicate a formula and check for stability, but this 
goes against the spirit of CoS, where the idea would be *not* to 
duplicate the formula and checking its stability *together* with the 
rest.

But anyway, one problem at the time. Let's try to get (a).

-Alessio