Re: Computability Logic

Alessio,

I've noticed that the previous two messages did not go through Frogs, so I will repeat a
couple of things. The notation on which we agreed and which I am extending now is:

 A - choice conjunction
 U - choice disjunction
 & - parallel/classical conjunction
 V - parallel/classical disjunction.

We had a consensus regarding Rule (b) and now are discussing the "trouble" Rule (a).
You suggested the following formulation for it:

       F{{top}} stable   F{{G}}   F{{H}}
    a -----------------------------------------;
                      F{{G A H}}

Here F{{E}} is like F{E}, but we ask for E to be a surface occurrence in F{E}.

Unless I am misinterpreting something, your rule (a) is essentially more relaxed than mine,
and hence not an admissible one in CL1. Roughly, what makes it more relaxed is the flexibility
regarding the order in which A-type subformulas can be introduced when a given target
contains several such subformulas.

The following example could shed light on things. I will be using the lowercase g,h.k,l in it
instead of our old G,H,K,L to indicate that g,h,k,l are atoms. So, consider

(*)             ((-gV(-kU-l)) U (-hV(-kU-l)))  V  ((gAh) & (kAl))

Your version of the logic seems to derive (*) as follows:

1. (-gV-k)  V  (g & k) - tautology (has to be provable in any CL1-equivalent system)
2. (-gV(-kU-l))  V  (g & k) - from 1 by Rule (b)
3. (-gV(-kU-l))  V  (g & l) - similarly
4. (-gV(-kU-l))  V  (g & top) - stable
5. (-gV(-kU-l))  V  (g & (kAl)) - from 4,2,3 by Rule (a)
6. ((-gV(-kU-l)) U (-hV(-kU-l)))  V  (g & (kAl)) - from 5 by Rule (b)
7. ((-gV(-kU-l)) U (-hV(-kU-l)))  V  (h & (kAl)) - similarly
8. ((-gV(-kU-l)) U (-hV(-kU-l)))  V  (top & (kAl)) - stable
9. ((-gV(-kU-l)) U (-hV(-kU-l)))  V  ((gAh) & (kAl)) - from 8,6,7 by Rule (a).

Is this correct or I have misread something?

If correct, your system is stronger than CL1, for the latter does not prove (*).
The first 8 steps can be done within CL1, but not the last one.

A proof sketch for the fact that CL1 does not derive (*): If the last rule in a CL1-derivation of
(*)  is (b), either -g or -h would be no longer present in the premise, and it can be seen that
this would eventually make it impossible to derive such a premise because there would be
nothing to match with g or h. And if the last rule in a CL1-proof of (*) is Rule (a), one of the
4 premises that the rule requires is ((-gV(-kU-l)) U (-hV(-kU-l))) V ((gAh) & k) (or/and l instead
of k, of course). The latter is an instable formula, so it cannot be derived by Rule (a). And it
cannot be derived by Rule (b) either, - for the same (above) reason as (*) could not be derived
by that rule.

Comment: There appear to be two major differences between my Rule (a) and the A
(additive conjunction) -introduction rule of linear logic. One is that the former is deep while the
latter is shallow. And the other - more unusual - difference is that, in very rough terms, while
in linear logic this rule can be applied as soon as all conjuncts (with/within the surrounding
context, of course) of SOME A-conjunction are provable, CL1 insists that all conjuncts of ALL
A-conjunctions be provable. As for Rule (b), it only differs from the U (additive disjunction)
-introduction rule of linear logic in that it is deep. A common syntactic intuition is that (a)-steps
are "universal" while (b)-steps are "existential". The above observation regarding (a) makes me
feel that CL1 more consistently materializes this intuition than linear logic does - as long
as the difference is really inherent, of course.

- Giorgi