Reversibility and focalization
Negative connectives are reversible:
- A sequent is provable if and only if is provable.
- A sequent is provable if and only if and are provable.
- A sequent is provable if and only if is provable.
- A sequent is provable if and only if is provable, for some fresh variable ξ.
Proof. We start with the case of the connective. If is provable, then by the introduction rule for we know that is provable. For the reverse implication we proceed by induction on a proof π of .
- If the last rule of π is the introduction of the in , then the premiss is exacty so we can conclude.
- The other case where the last rule introduces is when π is an axiom rule, hence . Then we can conclude with the proof
- Otherwise is in the context of the last rule. If the last rule is a tensor, then π has the shape
- or the same with in the conclusion of π2 instead. By induction hypothesis on π1 we get a proof π'1 of , then we can conclude with the proof
- The case of the cut rule has the same structure as the tensor rule.
- In the case of the rule, we have in both premisses and we conclude similarly, using the induction hypothesis on both π1 and π2.
- If is in the context of a rules for , , or quantifiers, or in the context of a dereliction, weakening or contraction, the situation is similar as for except that we have only one premiss.
- If is in the context of rules, we can freely change the context of the rule to get the expected one.
- The two remaining cases are if the last rule is the rule for 1 or a promotion. By the constraints these rules impose on the contexts, these cases cannot happen.
The connective is treated in the same way. In this cases where is in the context of a rule with two premisses, the premiss where this formula is not present will be duplicated, with one copy in the premiss for A and one in the premiss for B.
The connective is also treated similarly. Its peculiarity is that introducing requires that ξ does not appear free in the context. For all rules with one premiss except the quantifier rules, the set of fresh variables in the same in the premiss and the conclusion, so everything works well. Other rules might change the set of free variables, but problems are avoided by choosing for ξ a variable that is fresh for the whole proof we are considering.
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
A positive generalized connective is a parametrized formula made from the variables Xi using the connectives , , , .
A negative generalized connective is a parametrized formula made from the variables Xi using the connectives , , , .
If is a generalized connectives (of any polarity), the
dual of C is the connective C * such that
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.
The branching of a generalized connective is the multiset of multisets over defined inductively as
, , , , .
The branching of a negative generalized connective is the branching of its
dual. Elements of a branching are called branches.
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.
Let be a branching. Write as and write each Ij as . The derived rule for a negative generalized connective N with branching is
For each branch of a positive generalized connective P, the derived rule for branch I of P is
The reversibility property of negative connectives can be rephrased in a generalized way as
Let N be a negative generalized connective. A sequent
is provable if and only if, for each
, the sequent
The corresponding property for positive connectives is the focalization property, defined in the next section.
A formula is positive if it has a main connective among
, , , .
It is called negative if it has a main connective among
, , , .
It is called neutral if it is neither positive nor negative.
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.
A proof is said to be positively focused on A if it has the shape
where P is a positive generalized connective, the Ai ar non-positive
and . The formula A is called the focus of the
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.
A sequent is cut-free provable if and only if it is provable
by a cut-free proof that is positively focused.
Proof. We reason by induction on a proof π of Γ. As noted above, the result trivially holds if Γ has a non-positive formula. We can thus assume that Γ contains only positive formulas and reason on the nature of the last rule, which is necessarily the introduction of a positive connective (it cannot be an axiom rule because an axiom always has at least on non-positive conclusion).
Suppose that the last rule of π introduces a tensor, so that π is
By induction hypothesis, there are positively focused proofs and . If A is the focus of ρ' and B is the focus of θ', then the proof
is positively focused on , so we can conclude. Otherwise, one of the two proofs is positively focused on another conclusion. Without loss of generality, suppose that ρ' is not positively focused on A. Then it decomposes as
where the Ci are not positive and A belongs to some context Γj that we will write Γ'j,A. Then we can conclude with the proof
which is positively focused on .
If the last rule of π introduces a , we proceed the same way except that there is only one premiss. If the last rule of π introduces a , then it is the only rule of π, which is thus positively focused on this .
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.