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".
>
>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.


Aaaargh! Lutz, always you!!   -Alessio