Re: CoS and computability logic

Alessio,

I am sorry to disappoint you, but there is a "simple" counterexample to your 
conjecture "M=BKS".

On Friday 14 May 2004 16:40, Alessio Guglielmi wrote:
> *** Definition   A *binary tautology* is a classical propositional
> tautology which, for every atom a, contains at most one positive and
> at most one negative occurrence of a. Let's call M the language of
> formulas which are *substitutional instances* of binary tautologies.
>
>
> For example, [-a,a,a] is in M because it is a substitutional instance
> of the binary tautology [-b,c,b]. On the other hand, [-a,(a,a)] is
> not in M.
>
> Let us now consider the system obtained from KS by removing atomic
> contraction, which I call BKS (is this name well chosen? Does it obey
> the scheme we have? B=`binary').
>
>
> *** Definition   System BKS is
>
>           t          (R,[T,U])       [(R,U),(T,V)]          f
>     ai_ ------ ,   s --------- ,   m ------------- ,   aw_ --- ;
>         [a,-a]       [(R,T),U]       ([R,T],[U,V])          a
>
> the usual conventions apply: rules are deep, t and f are units,
> conjunction (...) and disjunction [...] are associative and
> commutative, the equations (f,f) = f and [t,t] = t may be used, and
> Augustus takes care of negation.
>
> *** 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.

In fact, this example is a version of the pidgeon-hole principle (here three 
pidgeons, four holes) that I found useful, but could not find in the 
literature. Can anybody name a reference where this version of the 
pidgeonhole principle appears? I cannot really believe that I am the first 
one who came up with it.

> *** Problem 2   Prove that cut is admissible for BKS.
>
> I'm almost sure this is true, 

Actually, I am not so sure about this. But I cannot really explain why. I 
need more time to think about this. 

-Lutz