Re: CoS and computability logic

On Sunday 16 May 2004 02:21, Alessio Guglielmi wrote:
> 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?

No. The case with two pidgeons is

  [ ( [ a, b] , [ c, d] , [ e, f] ) ,
    ( [-a, g] , [-c, h] , [-e, k] ) ,
    ( [-b,-g] , [-d,-h] , [-f,-k] ) ]

which can be done without contraction via medial.

-Lutz