Re: Computability Logic

Dear Giorgi,

fragment M looks indeed more promising. I'm totally overwhelmed this 
month (and the following), and I cannot check the details, but 
another (naif??) idea is to try to adopt

    multiplicative linear logic + weakening + medial

i.e.

    classical logic - atomic contraction .

Medial is indeed a rule which uses deep inference, in standard 
notation it corresponds to the inference

    (A ^ C) V (B ^ D)
    ----------------- .
    (A V B) ^ (C V D)

This inference rule can be used to reduce normal contraction into 
atomic contraction, i.e.

    contraction = atomic contraction + medial .

Also, after looking at your definition of validity in M, it really 
seems like a deductive system for system M is already in Kai's 
thesis! Just take his propositional system KS and remove the rule ac_ 
(atomic contraction). It does make sense...

Kai, do you have some time to check this thing? At this time it makes 
sense to me, but I just drank a bit of Bowmore 17 years (thanks 
again, Prakash), sorry if I'm wasting your time...

Ah, I just checked the formula Giorgi provides: it is proved, either 
by KS-{ac_} or by Bowmore 17:

                         true
    ai_ -------------------------------------
        [          -c   ,c                  ]
    ai_ -------------------------------------
        [  ([-a,a],-c)  ,c                  ]
      s -------------------------------------
        [  (-a,-c) ,   a,c                  ]
    ai_ -------------------------------------
        [  (-a,-c) , ([a,c],[        -d ,d])]
    ai_ -------------------------------------
        [  (-a,-c) , ([a,c],[([-b,b],-d),d])]
      s -------------------------------------
        [  (-a,-c) , ([a,c],[(-b,-d), b,d]) ]
      s -------------------------------------
        [  (-a,-c),(-b,-d)  , ([a,c],[b,d]) ]
      m ------------------------------------- .
        [ ([-a,-b],[-c,-d]) , ([a,c],[b,d]) ]

-Alessio


At 5:29 -0400 8.5.04, Giorgi Japaridze wrote:
>Alessio - I'm back. Sorry for the late response.
>
>>  You were mentioning a couple other fragments of computability logic.
>>  Can we have a look?
>
>Ok. Let us call this one M. Its language is exactly that of 
>classical propositional logic
>(as an aside: computability logic has two sorts of atoms depending on what
>interpretations they allow; the atoms of M are different from those 
>of CL1, and
>hence CL1 and M may disagree on some formulas).
>
>The valid formulas of M are exactly those that are substitutional 
>instances of binary
>tautologies. "Binary tautology" means a classical tautology which, 
>for every atom p,
>contains at most one positive and at most one negative occurrence of p.
>
>For example,  -aV(aVa)  is in M because it is a substitutional 
>instance of the binary
>tautology  -pV(qVp). On the other hand,  -aV(a&a)  is not in M.
>
>M is a fragment of logic CL2 described in Section 6 of "Computability Logic: A
>Formal Theory of Interaction". *Fragment* in the sense that CL2 is a 
>conservative
>extension of M. There is an  axiomatization for CL2 in a style 
>similar to CL1, but
>even if we are happy with that axiomatization, it cannot be 
>mechanically restricted to
>M because it essentially requires a stronger language than that of M.
>
>So, the question now is: can we come up with a reasonable 
>axiomatization directly
>for M?
>
>A first naive thought could be that Affine logic (linear logic + 
>weakening) might fit
>the bill. But this is not so: M can be shown to be strictly 
>stronger. And, roughly
>speaking, the reason - or one of the reasons - is that Affine logic 
>only uses shallow
>inference. Here is an example of a formula that is in M but not in 
>Affine logic:
>                           ((-aV-b) & (-cV-d)) V ((aVc) & (bVd))
>
>- Giorgi
>http://www.cis.upenn.edu/~giorgi/cl.html