Re: Deduction modulo in CoS

Dear Guillaume,

I'm not an expert on deduction modulo, but I work on sequent systems with 
definition (of atoms) that, in some way, is related to your work. 

I've been thinking myself if it is possible (and worthy) to add the notion of 
definitions (together with some other concepts, like polarities) to CoS. The 
idea behind definitions is that, whenever you encounter an atom, instead of 
stopping the proof you continue by substituting the atomic predicate by its 
defined body, just like in your example, and go on. If you have the notion of 
polarites as well, the assymetry of sequent calculus guarantees interesting 
different proofs.

About your example:

> consider the (proposition) rewrite rule  A -> B ^ -A

It is the same as defining A = B ^ -A. This is something we don't allow, since 
the resulting system is not consistent (if B is not false). The problem is the 
definition of A via not A: no fix point.

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

This problem is undecidable in general. And any translation from SC to CoS 
will preserve the cut elimination property. So it does not depend on the 
formalism. Of course, there may be systems that don't have cut elimination and 
can't be expressed in SC...

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

As I said before, in the presence of definition, "confluence" means existence 
of fixed points. But it is a necessary condition, not a characterization.

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

I might be wrong, but quantifiers are difficult to handle also in CoS...

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

Well, this can be done also in CS, I think, in the same way as in CoS. Do you 
have a counter example?

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

I'm not sure if deep inference will help in your or mine cases, but I'm very 
much interested on these kind of thinking. 

Best regards,

Elaine.
-------------------------------------------------
Elaine Pimentel  - DMat/UFMG

Address: Departamento de Matematica
         Universidade Federal de Minas Gerais
         Av Antonio Carlos, 6627 - C.P. 702
         Pampulha - CEP 30.123-970
         Belo Horizonte - Minas Gerais - Brazil
Phone:   55 31 3499-5970
Fax:     55 31 3499-5797
http://www.mat.ufmg.br/~elaine
-------------------------------------------------