Re: Computability Logic

Alessio - I'm back. Sorry for the late response.

> You were mentioning a couple other fragments of computability logic.
> Can we have a look?

Ok. Let us call this one M. Its language is exactly that of classical propositional logic
(as an aside: computability logic has two sorts of atoms depending on what
interpretations they allow; the atoms of M are different from those of CL1, and
hence CL1 and M may disagree on some formulas).

The valid formulas of M are exactly those that are substitutional instances of binary
tautologies. "Binary tautology" means a classical tautology which, for every atom p,
contains at most one positive and at most one negative occurrence of p.

For example,  -aV(aVa)  is in M because it is a substitutional instance of the binary
tautology  -pV(qVp). On the other hand,  -aV(a&a)  is not in M.

M is a fragment of logic CL2 described in Section 6 of "Computability Logic: A
Formal Theory of Interaction". *Fragment* in the sense that CL2 is a conservative
extension of M. There is an  axiomatization for CL2 in a style similar to CL1, but
even if we are happy with that axiomatization, it cannot be mechanically restricted to
M because it essentially requires a stronger language than that of M.

So, the question now is: can we come up with a reasonable axiomatization directly
for M?

A first naive thought could be that Affine logic (linear logic + weakening) might fit
the bill. But this is not so: M can be shown to be strictly stronger. And, roughly
speaking, the reason - or one of the reasons - is that Affine logic only uses shallow
inference. Here is an example of a formula that is in M but not in Affine logic:
                          ((-aV-b) & (-cV-d)) V ((aVc) & (bVd))

- Giorgi
http://www.cis.upenn.edu/~giorgi/cl.html