Re: Computability Logic

At 7:20 PM -0400 24.4.04, Giorgi Japaridze wrote:
>>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).

Yes, I agree, I thought a bit more on this and I see that the problem 
is difficult.

You were mentioning a couple other fragments of computability logic. 
Can we have a look?

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

Normally, symmetry is good, but I don't see how this can help in this 
case. In any case, it would be good to have around a document 
containing also these results.

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

It's what I hope, your case is definitely interesting.

The problem, as I see it, is that rule (a) is `eager': when read 
bottom-up, it asks for trying immediately all variants obtained by 
substitution. Moreover, there is a `problem' with stability, in the 
sense that a formula might be stable while formulae obtained from its 
subformulae might not; this makes hard to decompose rule (a) into 
rules that operate on its premises in successive stages. But these 
things could perhaps be fixed, we saw this happening already in sort 
of similar cases.

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

I agree.

I'm thinking about opening a new section on the CoS web site 
dedicated to open problems and/or other approaches requiring deep 
inference, and we could start with yours, if you agree.

It would be useful to have a short description of the problem, let's 
say a few lines of text, and then perhaps a link to a more thorough 
description. Would it be fine with you if I linked the page you sent 
us? Or, can you put it online? Would you like to write a short text 
describing the problem?

-Alessio