Reversibility and focalization
Remark that this result is proved using only commutation rules, except when the formula is introduced by an axiom rule. Furthermore, if axioms are applied only on atoms, this particular case disappears.
A consequence of this fact is that, when searching for a proof of some sequent , one can always start by decomposing negative connectives in Γ without losing provability. Applying this result to successive connectives, we can get generalized formulations for more complex formulas. For instance:
- is provable
- iff is provable
- iff and are provable
- iff and are provable
So without loss of generality, we can assume that any proof of ends like
In order to define a general statement for compound formulas, as well as an analogous result for positive connectives, we need to give a proper status to clusters of connectives of the same polarity.
Generalized connectives and rules
It is clear that dualization of generalized connectives is involutive and exchanges polarities. We do not include quantifiers in this definition, mainly for simplicity. Extending the notion to quantifiers would only require taking proper care of the scope of variables.
Sequent calculus provides introduction rules for each connective. Negative connectives have one rule, positive ones may have any number of rules, namely 2 for and 0 for . We can derive introduction rules for the generalized connectives by combining the different possible introduction rules for each of their components.
Considering the previous example , we can derive an introduction rule for N as
but these rules only differ by the commutation of independent rules. In particular, their premisses are the same. The dual of N is , for which we have two possible derivations:
These are actually different, in particular their premisses differ. Each possible derivation corresponds to the choice of one side of the connective.
We can remark that the branches of the negative inference precisely correspond to the possible positive inferences:
- the first branch of the negative inference has a premiss X1,X2,X2 and the first positive inference has three premisses, holding X1, X2 and X2 respectively.
- the second branch of the negative inference has a premiss X1,X2,X3 and the second positive inference has three premisses, holding X1, X2 and X3 respectively.
This phenomenon extends to all generalized connectives.
In the example above, the branching will be [[1,2,2],[1,2,3]], which corresponds to the granches of the negative inference and to the cases of positive inference.
The reversibility property of negative connectives can be rephrased in a generalized way as
The corresponding property for positive connectives is the focalization property, defined in the next section.
If we extended the theory to include quantifiers in generalized connectives, then the definition of positive and negative formulas would be extended to include them too.
In other words, a proof is positively focused on a conclusion A if its last rules build A from some of its non-positive subformulas in one cluster of inferences. Note that this notion only makes sense for a sequent made only of positive formulas, since by this definition a proof is obviously positively focused on any of its non-positive conclusions, using the degenerate generalized connective P[X] = X.
As in the reversibility theorem, this proof only makes use of commutation of independent rules.
These results say nothing about exponential modalities, because they respect neither reversibility nor focalization. However, if we consider the fragment of LL which consists only of multiplicative and additive connectives, we can restrict the proof rules to enforce focalization without loss of expressiveness.