Re: Computability Logic

OK Giorgi, let's see, let me ask some questions, but please keep in 
mind that I still know almost nothing of computability logic. I also 
need you to check the following before proceeding.

Since --F = F, we can push negation to atoms; this way we don't have 
to worry about positive and negative contexts; this is very good when 
doing deep inference because we can avoid looking at the context in a 
non-local way and it halves the number of inference rules.

Let's use A for \sqcap and U for \sqcup. I assume that the operators 
A and U are commutative and that there are equations on formulae 
dealing with this.

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

Rule (b) becomes

        F{{G}}
    b ---------- ;
      F{{G U H}}

and we don't need any other rules, except for those that transform a 
formula into stable form (trivial) and then check for its validity 
(system SKS would do fine).

Is what I wrote above correct?

If so, the next step would be for me to try and remove the condition 
on having to work on surface occurrences: 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?

-Alessio


At 2:05 -0400 19.4.04, Giorgi Japaridze wrote:
>     Probably the simplest fragment to look at would be CL1. If nothing
>interesting comes out this time, there are a couple of other "the simplest"
>fragments to try. CL1 is presented in Section 6 of
>"Computability logic: a formal theory of interaction" at
>http://www.csc.villanova.edu/~japaridz/CL/CLFTI.pdf
>     Here I am attaching a page that reproduces the relevant pieces of that
>section. The paper was written for a different sort of readers and my
>apologies if some explanations or examples seem redundant.
>     - Giorgi