Re:Deduction modulo in CoS

Hello,

I think that deep inference is more natural than 
the sequent calculus for deduction modulo and 
that it should lead to more expressive systems, 
but proving cut elimination in deep inference is 
harder and we should expect this to be the case 
also in the future.

However, I think that it is possible, with some 
hard work, to find completion procedures in deep 
inference that guarantee (weak) analyticity for a 
larger class of systems than those that can be 
characterised in the sequent calculus. In 
particular, I agree with Guillaume that deep 
inference should allow to lift the restriction on 
rewriting atomic propositions.

A few considerations:


1) In the propositional case, things are 
(deceptively?) simple. If you take Kai's cut 
elimination proof, you see that rewrite rules 
don't disturb cut elimination provided that 
substituting atoms with `true' doesn't break the 
proof irreparably. So, for example, if you add a 
rewrite rule like

   a -> a ^ b

to a system, you can immediately conclude that you maintain cut elimination.

This argument would not work with the (strange!) rule

   a -> -a ^ b ,

because the substitution [a/t] would mean [-a/f], 
and this could break irreparably identity axioms 
in a proof. However, adding also

   b -> f

would fix the procedure, much in the same way as 
it does it in the sequent calculus (if I 
understand it correctly).

The case of predicate logic is much more 
difficult, see Kai in Studia Logica 
<http://www.iam.unibe.ch/~kai/Papers/q.pdf>.


2) The thing that excites me most, is that deep 
inference and deduction modulo seem to agree on a 
fundamental objective: make proofs shorter. In 
this respect, I'd say that deduction modulo in 
deep inference makes even more sense than in the 
sequent calculus. This, especially when generic 
rewrite rules might be considered.

In this case, rules like

   R -> T ,

where R and T are generic formulae, might play 
the same role of Tseitin's extension, and provide 
for exponential speed-ups.

With these rules, one, for example, could realise a mechanism like

   R -> a
   a -> R

where a (complex formula) R is replaced by a 
fresh atom a and then restored again by a -> R. 
By recursively applying this mechanism, which 
corresponds to Tseitin's extension (in Frege 
systems), one can achieve exponential speed-ups.

This speed-ups would be *on top* of the 
exponential speed ups that deep inference already 
provides over shallow inference.


3) In relation to a remark by Guillaume (which 
perhaps I misunderstood): the ability of getting 
analytic systems does depend on the formalism. 
For example, we know that using a linear, 
non-commutative, self-dual connective in a linear 
logic gives rise to a logic for which no cut-free 
sequent calculus is possible, while there's a 
very simple analytic system in deep inference. 
For this, see Alwen in Logical Methods in 
Computer Science 
<http://arxiv.org/pdf/cs.LO/0512036>.


4) Elaine says that what Guillaume proposes about 
making rules out of derivations is possible also 
in the sequent calculus. This is true, but only 
in the sense of replacing a formula, in a 
sequent, with another arbitrarily complex one, 
while going up in a proof, which is not very much 
in the spirit of sequent calculus. I'd say that 
deep inference is more natural for this, it's a 
more convenient language.

In any case, if one restricts the use of the cut 
rule in deep inference in a way that is 
isomorphic to the sequent calculus one, than cut 
elimination is not more difficult than in the 
sequent calculus.


Very much interested in all of this!

-Alessio


At 15:44 +0100 28/2/06, Guillaume Burel wrote:
> 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
>   Åa
>   Åa
>   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