Re: Computability Logic

Giorgi,

sorry for being slow in replying, I'm having rather full days...

Perhaps I'm missing something totally obvious, but it seems to me 
that the rules I was proposing are able to deal with the situation 
you suggest. In fact, in the example you mention, and by using your 
notation, I have

      F{{top, top}} stable   F{{H, K}}   F{{H, L}}
    a --------------------------------------------
                            |
                            +-------------------------+
                                                      |
      F{{top, top}} stable   F{{G, K}}   F{{G, L}}    |
    a --------------------------------------------    |
                                     |                |
                               -------------   -------------
      F{{top, K A L}} stable   F{{G, K A L}}   F{{H, K A L}}
    a ------------------------------------------------------ .
      F{{G A H, K A L}}

Clearly, there's a lot of redundancy in proving again and again that 
various F{{...,...}} are stable (they are all the same wrt 
stability). But, of course, if this first step is OK, then we'll try 
to manage all these instances in one, common context.

Now, the rule you suggest below for the case in which you have two 
surface occurrences of formulae of shape (... A ...) seems to reduce, 
in the end, the problem to the one I show above.

It looks to me that rule b does not interfere with these things.

Am I right or am I totally off?

-Alessio


At 9:43 AM -0400 20.4.04, Giorgi Japaridze wrote:
>  > Since --F = F, we can push negation to atoms; this way we don't have
>>  to worry about positive and negative contexts;
>
>Right.
>
>>  Let's use A for \sqcap and U for \sqcup. I assume that the operators
>>  A and U are commutative
>
>Either sort of conjunction and disjunction is commutative and 
>associative modulo
>(semantical) equivalence but  - unlike double negation or DeMorgan - 
>not in the sense of
>strict equality. I will not bother you explaining details about what 
>equivalence exactly
>means here, and I guess it is fine if you consider that I just said 
>a definite "yes" to
>your question about commutativity.
>
>>  C{F} is a context C{ } whose hole is filled by formula F; E{{F}} is
>>  like E{F}, but we also ask for F to be a surface occurrence in E{F}.
>
>>  Let me then rephrase your rules (a) and (b) into sort of sequent
>>  calculus style.
>>
>>  Rule (a) becomes
>>
>  >       F{{top}} stable   F{{G}}   F{{H}}
>>      a ---------------------------------------- ;
>>                   F{{G A H}}
>>
>
>This rule, unlike the other one, could be a big troublemaker. Your formulation
>seems to be rephrasing Rule (a) only for the case when F has exactly 
>one surface
>occurrence of the form X A Y. If, for example, F had two such 
>occurrences, we would need
>to write F with two holes and get something like the following:
>
>        F{{top,top}} stable   F{{G, K A L}}   F{{H, K A L}}   F{{G A 
>H, K}}   F{{G A H, L}}
>
>     a
>--------------------------------------------------------------------------------------------------
>;
>                                                 F{{G A H, K A L}}
>
>(sorry if my notation is inconsistent with some established 
>conventions that you use). I
>have no guess regarding whether it is possible or not to rewrite the 
>logic in a
>single-hole fashion.
>
>>  Rule (b) becomes
>>
>>          F{{G}}
>>      b ---------- ;
>>        F{{G U H}}
>>
>
>That's right.
>
>>  what goes wrong if we use
>>  the same rules as above, but we use single curly brackets? Can you
>>  show me a counterexample for me to work on?
>
>Looks like nothing would go wrong. Formally verifying this answer 
>should not be too hard
>I think, but the question about Rule (a) needs to be resolved first.
>
>- Giorgi