Re: CoS and computability logic

On Monday 17 May 2004 11:36, Alessio Guglielmi wrote:
> >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.
>
> No Lutz, this formula looks falsifiable to me, the case with two
> pigeons should be
>
>     [ ( [ a, b] , [ c, d] ) ,
>       ( [-a, e] , [-c, f] ) ,
>       ( [-b,-e] , [-d,-f] ) ] .
>
> I couldn't quickly find a proof inside BKS, can you show one?
>
> -Alessio

Yes, you are right, I typed it too quickly without thinking.

the proof goes as follows (I just show the big steps)

you can get via two medials:
[(a,d),(b,c),(-a,f),(-c,e),([-b,-e],[-d,-f])]

then you do two switches to get
([(b,c),(-c,e),-b,-e],[(a,d),(-a,f),-d,-f])

the rest is easy.

-Lutz