Re: CoS and computability logic

At 17:46 +0200 14.5.04, Lutz Strassburger wrote:
>I am sorry to disappoint you, but there is a "simple" counterexample to your
>conjecture "M=BKS".
>
>  > *** Problem 1    Prove or disprove that BKS proves M.
>
>consider the following example (in SKS notation)
>
>  [ ( [ a, b, c] , [ d, e, f] , [ g, h, j] ) ,
>    ( [ k, l,-a] , [ m, n,-d] , [ o, p,-g] ) ,
>    ( [ q,-b,-k] , [ r,-e,-m] , [ s,-h,-o] ) ,
>    ( [-c,-l,-q] , [-f,-n,-r] , [-j,-p,-s] ) ]
>
>It is a tautology. It is easily seen to be *binary*. Hence it is in M.
>It is not provable in BKS. Any rule application leads immediately to a
>formula which is not a tautology.
>Therefore BKS does not prove M.

I checked it (rather quickly) and it looks you're right. Nice! 
Shouldn't the simpler case with two pigeons work equally well?

Now capturing M with reasonable rules looks hard. We should add 
something to BKS, but what?? Giorgi, would changing the way M is 
defined, in order for it to match BKS, make any semantic sense?

Is there a nice characterisation of the language that BKS recognises? 
If we found one, question 3 about whether BKS is intrinsically deep 
would still be meaningful enough to consider serious thinking.

Question 2, checking cut admissibility for BKS, should be a trivial 
exercise once we are done with splitting for SKS.

-Alessio