Re: Computability Logic

Dear Giorgi,

in system KS for classical logic we decomposed the contraction rule into 
two rules: a rule for contracting atoms and a rule that we call "medial" 
(you call it Blass' principle).

Now, the formula you provide as an example of what is provable in your 
fragment M but not in affine logic _is_ medial (a.k.a Blass principle). 
It's thus not surprising that it is provable in system KS without atomic 
contraction, which is nothing else than affine logic plus medial. (It 
stays provable even without Bowmore 17.)

So, I agree with Alessio: this could be the right formalisation. If so, 
then that would be just wonderful. Girard dropped too much, and he 
dropped too much because the sequent calculus didn't allow him to keep 
medial simply because it wasn't there, haha.

I'll give it a try to check whether your definition of M coincides with 
KS minus atomic contraction. But what does your intuition say: is Blass' 
principle in some sense the only formula provable in M that is not 
provable in affine logic?

-Kai