CoS and computability logic

Hello,

with this email I'd like to summarise the information needed for 
solving the very nice problem Giorgi and I have been discussing. I 
hope this way that all the young and clever people on this list might 
be able to work on the problem without investing too much time for 
starting up.

By the way, the solution of the problem is of independent interest 
and could provide some useful tools and insights for our research on 
deep inference.

I'll now translate Giorgi's definitions into CoS syntax:


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


(All details can be found in Kai's thesis at 
<http://www.iam.unibe.ch/%7ekai/Papers/phd.pdf>---available for sale 
with a nice frog on the cover, BUY IT!.)

After working a bit on this, I think the following problem is 
interesting, meaning: if you prove it it's great, if you disprove it 
with a counterexample it's also good because we will understand 
something nontrivial:


*** Problem 1    Prove or disprove that BKS proves M.


It's easy to see that everything that BKS proves is in M, by just 
inspecting its rules. My guess is that the converse is also true.

An independent problem is the following:


*** Problem 2   Prove that cut is admissible for BKS.


I'm almost sure this is true, because in my 
cut-elimination-with-splitting proof attempt for SKS all rules are 
independent, meaning that if no atomic contraction is there to start 
with, no contraction is needed for eliminating cuts. Can you confirm 
this, Charles? I guess the need for contraction is the reason Kai's 
elegant proof can't be used in this case.

Are there other reasonable ways for proving this theorem 
constructively? Could we use completeness of BKS for M for proving 
cut elimination non-constructively?

Another problem, almost certainly the most challenging:


*** Problem 3   Prove that deep inference is needed for BKS.


A clue about how to proceed for proving this is trying to do what 
Alwen did with his counterexample. Alwen makes crucial use of 
relation web semantics, what can be challenging here because of the 
presence of weakening and medial. But please notice that *there is no 
contraction*, what makes for a reasonable situation (but still 
difficult!!).

On the other hand, this is very exciting, because we could make a 
point about deep inference being necessary for a logic without any 
fancy self-dual, non-commutative, deviant, mutant connective.

(For those who don't know about Alwen's counterexample: this is one 
of the most fascinating objects I ever saw in mathematics, and 
certainly the most beautiful in logic, look at 
<http://www.cse.psu.edu/%7etiu/thesisc.pdf>.)

Of course, it might be the case that deep inference is not necessary 
in the end: a counterexample would be most instructive, then

The more I think about them, the more I like these problems. I think 
managing to do some of this stuff would make for a very fine piece of 
research.

-Alessio