View source for Reversibility and focalization

== 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} := [ 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> \mathcal{I}_\one := [[]] </math>,
<math> \mathcal{I}_\zero := [] </math>,
<math> \mathcal{I}_{X_i} := [[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.