Reversibility and focalization - Revision history

Emmanuel Beffara: /* Focalization */ improved terminology

2012-08-31T21:50:29Z

‎Focalization: improved terminology

Emmanuel Beffara: /* Generalized connectives and rules */

2012-08-31T21:27:46Z

‎Generalized connectives and rules

Emmanuel Beffara: Creation

2012-08-31T21:10:58Z

Creation

New page

== Reversibility ==

{{Theorem|
Negative connectives are reversible:

* A sequent <math>\vdash\Gamma,A\parr B</math> is provable if and only if <math>\vdash\Gamma,A,B</math> is provable.
* A sequent <math>\vdash\Gamma,A\with B</math> is provable if and only if <math>\vdash\Gamma,A</math> and <math>\vdash\Gamma,B</math> are provable.
* A sequent <math>\vdash\Gamma,\bot</math> is provable if and only if <math>\vdash\Gamma</math> is provable.
* A sequent <math>\vdash\Gamma,\forall\xi A</math> is provable if and only if <math>\vdash\Gamma,A</math> is provable, for some fresh variable <math>\xi</math>.
}}

{{Proof|
We start with the case of the <math>\parr</math> connective.
If <math>\vdash\Gamma,A,B</math> is provable, then by the introduction rule for <math>\parr</math>
we know that <math>\vdash\Gamma,A\parr B</math> is provable.
For the reverse implication we proceed by induction on a proof <math>\pi</math> of
<math>\vdash\Gamma,A\parr B</math>.

* If the last rule of <math>\pi</math> is the introduction of the <math>\parr</math> in <math>A\parr B</math>, then the premiss is exacty <math>\vdash\Gamma,A,B</math> so we can conclude.
* The other case where the last rule introduces <math>A\parr B</math> is when <math>\pi</math> is an axiom rule, hence <math>\Gamma=A\orth\tens B\orth</math>. Then we can conclude with the proof
* Otherwise <math>A\parr B</math> is in the context of the last rule. If the last rule is a tensor, then <math>\pi</math> has the shape
* or the same with <math>A\parr B</math> in the conclusion of <math>\pi_2</math> instead. By induction hypothesis on <math>\pi_1</math> we get a proof <math>\pi'_1</math> of <math>\vdash\Gamma_1,A,B,C</math>, 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 <math>\with</math> rule, we have <math>A\with B</math> in both premisses and we conclude similarly, using the induction hypothesis on both <math>\pi_1</math> and <math>\pi_2</math>.
* If <math>A\parr B</math> is in the context of a rules for <math>\parr</math>, <math>\plus</math>, <math>\bot</math> or quantifiers, or in the context of a dereliction, weakening or contraction, the situation is similar as for <math>\tens</math> except that we have only one premiss.
* If <math>A\parr B</math> is in the context of <math>\top</math> 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 <math>1</math> or a promotion. By the constraints these rules impose on the contexts, these cases cannot happen.
The <math>\with</math> connective is treated in the same way.
In this cases where <math>A\with B</math> 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 <math>A</math> and one in the premiss for <math>B</math>.

The <math>\forall</math> connective is also treated similarly.
Its peculiarity is that introducing <math>\forall\xi</math> requires that <math>\xi</math> 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 <math>\xi</math> 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 <math>\vdash\Gamma</math>, one can always start by decomposing negative
connectives in <math>\Gamma</math> without losing provability.
Applying this result to successive connectives, we can get generalized
formulations for more complex formulas. For instance:

* <math>\vdash\Gamma,(A\parr B)\parr(B\with C)</math> is provable
* iff <math>\vdash\Gamma,A\parr B,B\with C</math> is provable
* iff <math>\vdash\Gamma,A\parr B,B</math> and <math>\vdash\Gamma,A\parr B,C</math> are provable
* iff <math>\vdash\Gamma,A,B,B</math> and <math>\vdash\Gamma,A,B,C</math> are provable
So without loss of generality, we can assume that any proof of
<math>\vdash\Gamma,(A\parr B)\parr(B\with C)</math> ends like

<math>
\AxRule{ \vdash \Gamma, A, B, B }
\UnaRule{ \vdash \Gamma, A\parr B, B }
\AxRule{ \vdash \Gamma, A, B, C }
\UnaRule{ \vdash \Gamma, A\parr B, C }
\BinRule{ \vdash \Gamma, A\parr B, B\with C }
\UnaRule{ \vdash \Gamma, (A\parr B)\parr(B\with C) }
\DisplayProof
</math>

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 ==

{{Definition|
A ''positive generalized connective'' is a parametrized formula
<math>P[X_1,\ldots,X_n]</math> made from the variables <math>X_i</math> using the connectives
<math>\tens</math>, <math>\plus</math>, <math>\one</math>, <math>\zero</math>.

A ''negative generalized connective'' is a parametrized formula
<math>N[X_1,\ldots,X_n]</math> made from the variables <math>X_i</math> using the connectives
<math>\parr</math>, <math>\with</math>, <math>\bot</math>, <math>\top</math>.

If <math>C[X_1,\ldots,X_n]</math> is a generalized connectives (of any polarity), the
''dual'' of <math>C</math> is the connective <math>C^*</math> such that
<math>C^*[X_1\orth,\ldots,X_n\orth]=C[X_1,\ldots,X_n]\orth</math>.
}}

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 <math>\plus</math> and 0 for <math>\zero</math>. 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
<math>N[X_1,X_2,X_3]=(X_1\parr X_2)\parr(X_2\with X_3)</math>, we can derive an
introduction rule for <math>N</math> as

<math>
\AxRule{ \vdash \Gamma, X_1, X_2, X_2 }
\UnaRule{ \vdash \Gamma, X_1\parr X_2, X_2 }
\AxRule{ \vdash \Gamma, X_1, X_2, X_3 }
\UnaRule{ \vdash \Gamma, X_1\parr X_2, X_3 }
\BinRule{ \vdash \Gamma, X_1\parr X_2, X_2\with X_3 }
\UnaRule{ \vdash \Gamma, (X_1\parr X_2)\parr(X_2\with X_3) }
\DisplayProof
\quad\text{or}\quad
\AxRule{ \vdash \Gamma, X_1, X_2, X_2 }
\AxRule{ \vdash \Gamma, X_1, X_2, X_3 }
\BinRule{ \vdash \Gamma, X_1, X_2, X_2\with X_3 }
\UnaRule{ \vdash \Gamma, X_1\parr X_2, X_2\with X_3 }
\UnaRule{ \vdash \Gamma, (X_1\parr X_2)\parr(X_2\with X_3) }
\DisplayProof
</math>

but these rules only differ by the commutation of independent rules.
In particular, their premisses are the same.
The dual of <math>N</math> is <math>P[X_1,X_2,X_3]=(X_1\tens X_2)\tens(X_2\plus X_3)</math>, for
which we have two possible derivations:

<math>
\AxRule{ \vdash \Gamma_1, X_1 }
\AxRule{ \vdash \Gamma_2, X_2 }
\BinRule{ \vdash \Gamma_1, \Gamma_2, X_1\tens X_2 }
\AxRule{ \vdash \Gamma_3, X_2 }
\UnaRule{ \vdash \Gamma_3, X_2\plus X_3 }
\BinRule{ \vdash \Gamma_1, \Gamma_2, \Gamma_3, (X_1\tens X_2)\tens(X_2\plus X_3) }
\DisplayProof
\qquad
\AxRule{ \vdash \Gamma_1, X_1 }
\AxRule{ \vdash \Gamma_2, X_2 }
\BinRule{ \vdash \Gamma_1, \Gamma_2, X_1\tens X_2 }
\AxRule{ \vdash \Gamma_3, X_3 }
\UnaRule{ \vdash \Gamma_3, X_2\plus X_3 }
\BinRule{ \vdash \Gamma_1, \Gamma_2, \Gamma_3, (X_1\tens X_2)\tens(X_2\plus X_3) }
\DisplayProof
</math>

These are actually different, in particular their premisses differ.
Each possible derivation corresponds to the choice of one side of the <math>\plus</math>
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 <math>X_1,X_2,X_2</math> and the first positive inference has three premisses, holding <math>X_1</math>, <math>X_2</math> and <math>X_2</math> respectively.
* the second branch of the negative inference has a premiss <math>X_1,X_2,X_3</math> and the second positive inference has three premisses, holding <math>X_1</math>, <math>X_2</math> and <math>X_3</math> respectively.
This phenomenon extends to all generalized connectives.

{{Definition|
The ''branching'' of a generalized connective <math>P[X_1,\ldots,X_n]</math> is the
multiset <math>\mathcal{I}_P</math> of multisets over <math>\{1,\ldots,n\}</math> defined
inductively as

{|
|-
| <math>
\mathcal{I}_{P\tens Q} </math>
| <math>:= [ I+J \mid I\in\mathcal{I}_P, J\in\mathcal{I}_Q ]
</math>
| <math> \mathcal{I}_{P\plus Q} </math>
| <math>:= \mathcal{I}_P + \mathcal{I}_Q
</math>
| <math> \mathcal{I}_\one </math>
| <math>:= [[]]
</math>
| <math> \mathcal{I}_\zero </math>
| <math>:= []
</math>
| <math> \mathcal{I}_{X_i} </math>
| <math>:= [[i]]
</math>
|}

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 <math>[[1,2,2],[1,2,3]]</math>, which
corresponds to the granches of the negative inference and to the cases of
positive inference.

{{Definition|
Let <math>\mathcal{I}</math> be a branching.
Write <math>\mathcal{I}</math> as <math>[I_1,\ldots,I_k]</math> and write each <math>I_j</math> as
<math>[i_{j,1},\ldots,i_{j,\ell_j}]</math>.
The derived rule for a negative generalized connective <math>N</math> with
branching <math>\mathcal{I}</math> is

<math>
\AxRule{ \vdash \Gamma, A_{i_{1,1}}, \ldots, A_{i_{1,\ell_1}} }
\AxRule{ \cdots }
\AxRule{ \vdash \Gamma, A_{i_{k,1}}, \ldots, A_{i_{k,\ell_k}} }
\LabelRule{N}
\TriRule{ \vdash \Gamma, N[A_1,\ldots,A_n] }
\DisplayProof
</math>

For each branch <math>I=[i_1,\ldots,i_\ell]</math> of a positive generalized connective
<math>P</math>, the derived rule for branch <math>I</math> of <math>P</math> is

<math>
\AxRule{ \vdash \Gamma_1, A_{i_1} }
\AxRule{ \cdots }
\AxRule{ \vdash \Gamma_\ell, A_{i_\ell} }
\LabelRule{P_I}
\TriRule{ \vdash \Gamma_1, \ldots, \Gamma_\ell, P[A_1,\ldots,A_n] }
\DisplayProof
</math>
}}

The reversibility property of negative connectives can be rephrased in a
generalized way as

{{Theorem|
Let <math>N</math> be a negative generalized connective. A sequent
<math>\vdash\Gamma,N[A_1,\ldots,A_n]</math> is provable if and only if, for each
<math>[i_1,\ldots,i_k]\in\mathcal{I}_N</math>, the sequent
<math>\vdash\Gamma,A_{i_1},\ldots,A_{i_k}</math> is provable.
}}

The corresponding property for positive connectives is the focalization
property, defined in the next section.

== Focalization ==

{{Definition|
A formula is ''positive'' if it has a main connective among
<math>\tens</math>, <math>\plus</math>, <math>\one</math>, <math>\zero</math>.
It is called ''negative'' if it has a main connective among
<math>\parr</math>, <math>\with</math>, <math>\bot</math>, <math>\top</math>.
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.

{{Definition|
A proof <math>\pi\vdash\Gamma,A</math> is said to be ''focalized'' on <math>A</math> if it has
the shape

<math>
\AxRule{ \pi_1 \vdash \Gamma_1, A_{i_1} }
\AxRule{ \cdots }
\AxRule{ \pi_\ell \vdash \Gamma_\ell, A_{i_\ell} }
\LabelRule{P_{[i_1,\ldots,i_\ell]}}
\TriRule{ \vdash \Gamma_1, \ldots, \Gamma_\ell, P[A_1,\ldots,A_n] }
\DisplayProof
</math>

where <math>P</math> is a positive generalized connective, the <math>A_i</math> ar non-positive
and <math>A=P[A_1,\ldots,A_n]</math>. The formula <math>A</math> is called the ''focus'' of the
proof <math>\pi</math>.
}}

In other words, a proof is focalized on a conclusion <math>A</math> if its last rules
build <math>A</math> from some of its non-positive subformulas in one cluster of
inferences. Note that this notion only makes sense for a conclusion made only
of positive formulas, since a proof is obviously focalized on any of its
non-positive conclusions, using the degenerate generalized connective
<math>P[X]=X</math>.

{{Theorem|
A sequent <math>\vdash\Gamma</math> is cut-free provable if and only if it is provable
by a cut-free focalized proof.
}}

{{Proof|
We reason by induction on a proof <math>\pi</math> of <math>\Gamma</math>.
As noted above, the result trivially holds if <math>\Gamma</math> has a non-positive
formula.
We can thus assume that <math>\Gamma</math> 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 <math>\pi</math> introduces a tensor, so that <math>\pi</math> is

<math>
\AxRule{ \rho \vdash \Gamma, A }
\AxRule{ \theta \vdash \Delta, B }
\BinRule{ \vdash \Gamma, \Delta, A\tens B }
\DisplayProof
</math>

By induction hypothesis, there are focalized proofs <math>\rho'\vdash\Gamma,A</math>
and <math>\theta'\vdash\Delta,B</math>.
If <math>A</math> is the focus of <math>\rho'</math> and <math>B</math> is the focus of <math>\theta'</math>, then the
proof

<math>
\AxRule{ \rho' \vdash \Gamma, A }
\AxRule{ \theta' \vdash \Delta, B }
\BinRule{ \vdash \Gamma, \Delta, A\tens B }
\DisplayProof
</math>

is focalized on <math>A\tens B</math>, so we can conclude.
Otherwise, one of the two proofs is focalized on another conclusion.
Without loss of generality, suppose that <math>\rho'</math> is not focalized on <math>A</math>.
Then it decomposes as

<math>
\AxRule{ \rho_1 \vdash \Gamma_1, C_{i_1} }
\AxRule{ \cdots }
\AxRule{ \rho_\ell \vdash \Gamma_\ell, C_{i_\ell} }
\TriRule{ \vdash \Gamma_1, \ldots, \Gamma_\ell, P[C_1,\ldots,C_n] }
\DisplayProof
</math>

where the <math>C_i</math> are not positive and <math>A</math> belongs to some context <math>\Gamma_j</math>
that we will write <math>\Gamma'_j,A</math>.
Then we can conclude with the proof

<math>
\AxRule{ \rho_1 \vdash \Gamma_1, C_{i_1} \quad\cdots }
\AxRule{ \rho_j \vdash \Gamma_j, A, C_{i_j} }
\AxRule{ \theta \vdash \Delta, B }
\BinRule{ \vdash \Gamma_j, \Delta, A\tens B, C_{i_j} }
\AxRule{ \cdots\quad \rho_\ell \vdash \Gamma_\ell, C_{i_\ell} }
\TriRule{ \vdash \Gamma_1, \ldots, \Gamma_\ell, \Delta, A\tens B, P[C_1,\ldots,C_n] }
\DisplayProof
</math>

which is focalized on <math>P[C_1,\ldots,C_n]</math>.

If the last rule of <math>\pi</math> introduces a <math>\plus</math>, we proceed the same way
except that there is only one premiss.
If the last rule of <math>\pi</math> introduces a <math>\one</math>, then it is the only rule of
<math>\pi</math>, which is thus focalized on this <math>\one</math>.
}}

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.

@@ Line 162: / Line 162: @@
 inductively as
-{|
+<math> \mathcal{I}_{P\tens Q} := [ I+J \mid I\in\mathcal{I}_P, J\in\mathcal{I}_Q ] </math>,
-|-
+<math> \mathcal{I}_{P\plus Q} := \mathcal{I}_P + \mathcal{I}_Q </math>,
-| <math>
+<math> \mathcal{I}_\one := [[]] </math>,
-    \mathcal{I}_{P\tens Q} </math>
+<math> \mathcal{I}_\zero := [] </math>,
-| <math>:= [ I+J \mid I\in\mathcal{I}_P, J\in\mathcal{I}_Q ]
+<math> \mathcal{I}_{X_i} := [[i]] </math>.
 The branching of a negative generalized connective is the branching of its

@@ Line 233: / Line 233: @@
 {{Definition|
-A proof <math>\pi\vdash\Gamma,A</math> is said to be ''focalized'' on <math>A</math> if it has
+A proof <math>\pi\vdash\Gamma,A</math> is said to be ''positively focused on <math>A</math>'' if it has the shape
 <math>
@@ Line 249: / Line 249: @@
 }}
-In other words, a proof is focalized on a conclusion <math>A</math> if its last rules
+In other words, a proof is positively focused on a conclusion <math>A</math> if its last rules
 build <math>A</math> from some of its non-positive subformulas in one cluster of
-inferences. Note that this notion only makes sense for a conclusion made only
+inferences. Note that this notion only makes sense for a sequent made only
-of positive formulas, since a proof is obviously focalized on any of its
+of positive formulas, since by this definition a proof is obviously positively focused on
-non-positive conclusions, using the degenerate generalized connective
+any of its non-positive conclusions, using the degenerate generalized
-<math>P[X]=X</math>.
+connective <math>P[X]=X</math>.
 {{Theorem|
 A sequent <math>\vdash\Gamma</math> is cut-free provable if and only if it is provable
-by a cut-free focalized proof.
+by a cut-free proof that is positively focused.
 }}
@@ Line 279: / Line 279: @@
   </math>
-By induction hypothesis, there are focalized proofs <math>\rho'\vdash\Gamma,A</math>
+By induction hypothesis, there are positively focused proofs <math>\rho'\vdash\Gamma,A</math>
 and <math>\theta'\vdash\Delta,B</math>.
 If <math>A</math> is the focus of <math>\rho'</math> and <math>B</math> is the focus of <math>\theta'</math>, then the
@@ Line 291: / Line 291: @@
   </math>
-is focalized on <math>A\tens B</math>, so we can conclude.
+is positively focused on <math>A\tens B</math>, so we can conclude.
-Otherwise, one of the two proofs is focalized on another conclusion.
+Otherwise, one of the two proofs is positively focused on another conclusion.
-Without loss of generality, suppose that <math>\rho'</math> is not focalized on <math>A</math>.
+Without loss of generality, suppose that <math>\rho'</math> is not positively focused on <math>A</math>.
 Then it decomposes as
@@ Line 318: / Line 318: @@
   </math>
-which is focalized on <math>P[C_1,\ldots,C_n]</math>.
+which is positively focused on <math>P[C_1,\ldots,C_n]</math>.
 If the last rule of <math>\pi</math> introduces a <math>\plus</math>, we proceed the same way
 except that there is only one premiss.
 If the last rule of <math>\pi</math> introduces a <math>\one</math>, then it is the only rule of
-<math>\pi</math>, which is thus focalized on this <math>\one</math>.
+<math>\pi</math>, which is thus positively focused on this <math>\one</math>.
 }}