Re: Computability Logic

> The main trick of the trade when dealing with deep inference
> in CoS is trying to get rules that do as little as possible.

Sure, I see that.

> 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).

I wish I had an answer. I do not rule out that some "sexier" formulations
of CL1 are possible - actually I hope that this is so. But then we might
need some more dramatic changes than just trying to modify rule (a).

At present I do not know much about the proof theoretic properties of the logic. One
little
thing I can say is that as long as we only have shallow occurrences of A-subformulas,
nothing
goes wrong if we use the variant of rule (a) that you suggested. Another observation is
that the
two rules of CL1 can be made more symmetric by requiring that rule (b) be applied only
when
the conclusion is insatiable. Also, in the semantically completeness proof for CL1  I
studied the
dual logic CL1' obtained from CL1 by just interchanging "stable" and "insatiable", "A" and
"U" in
its two rules. It turns out that CL1 and CL1' are exact complements of each other: a
formula is
derivable in one if it is not derivable in the other.

But I guess all that is not very comforting. If it turns out that CL1 cannot be tamed,
perhaps
the challenges it presents could stimulate some new ideas within the general spirit of
your approach. I expect that if the rule (a)-style challenge emerged in computability
logic, it may reoccur later in some other and perhaps unexpected contexts as well. What
makes me feel so is
my belief that the semantics of CL is very natural and hence the logic that it induces is
rigid
with respect to a wide range of technical variations in the semantics (this has been
tested
already). So, it is likely that some other - seemingly very different - meaningful
semantics yield
the same logic.

- Giorgi