Deduction modulo in CoS

Hello,

I am currently working on cut elimination in deduction modulo, and I
have the impression that the Calculus of Structures could help to better
understand what's going on. I recently spoke with Alessio who seems
interested as well.

First, let me give a (well-known in the community of deduction modulo)
example which shows that the cut-elimination property does not hold in
sequent calculus modulo:
consider the (proposition) rewrite rule  A -> B ^ -A
there is a proof of B |- involving one cut:

           --------
           A,B |- A
        ---------------
        A, B, B ^ -A |-
        ---------------
            A, B |-
   ------   -------    --------
   B |- B   B |- -A    A,B |- A
   ----------------   ------------
     B |- B ^ -A      A, B ^ -A |-
     -----------      ------------
       B |- A             A |-
       ----------------------- Cut
                 B |-

but there are no proofs of B |- without cut.

There are two ways to solve this problem: one is to restrict oneself to
systems having the cut elimination property, the other one is to
complete the rewrite system to recover it. Related to this, I see at
least two points where the CoS could help:

1. Conditions for Cut Elimination
---------------------------------

As far as I know, there is no exact characterization of systems in
deduction modulo for which the cut elimination holds, but only
sufficient or necessary conditions. It is not clear how it depends on
the formalism (the sequent calculus). I think that this is a subcase of
a more general question in the CoS: what deductive systems (with a cut
rule) have the cut elimination property ? (How) can they be characterized ?

In deduction modulo, if only *terms* are rewritten, then it has been
shown by Dowek that the cut elimination property is equivalent to the
confluence of the rewrite system. It is not the case when one rewrites
propositions (as in the example above). A naive reasoning could be: as
the CoS can be seen as a rewrite system, the cut elimination corresponds
perhaps to some "confluence" property of the deductive systems.


2. Completion of Proposition Rewrite Systems
--------------------------------------------

As said before, one way to recover the cut elimination property is to
complete the rewrite system (in a kind of generalization of the
Knuth-Bendix completion). For instance the proposition rewrite system

 A -> B ^ -A
 B -> False

has the cut elimination property. To complete a rewrite system, one has
to add to it the conclusions of so-called critical proofs, i.e. minimal
counter-examples that shows that the required property does not hold.
One must therefore link these conclusions, which are sequents for the
sequent calculus modulo, with rewrite rules.

The problem with deduction modulo, in the way it is currently stated, is
that, essentially due to the fact that one work in the sequent calculus,
one considers only rules that rewrite *atomic* propositions. There is
therefore no simple way to add rewrite rules corresponding to a sequent
involving quantifiers.

On the contrary, in the CoS, a critical proofs, or better a critical
derivation

  U
  ‖
  ‖
  V

could be introduced as a new inference rule

    U
new -
    V

Therefore, I think that the CoS could a much better formalism to define
this completion procedure. And I think that this procedure would not be
restricted to deduction modulo.


I hope I have exposed my main concerns clearly enough. I would be very
glad to receive comments, questions, or (even better) answers about
these remarks. In particular, could you tell me if you think that deep
inference can or not help me, and if you will be interested by such results?

Best regards,

Guillaume Burel