Subject: Re: Deduction modulo in CoS
Newsgroups: gmane.science.mathematics.frogs
Date: 2006-02-28 21:50:55 GMT (2 years, 10 weeks, 2 days, 18 hours and 16 minutes ago)
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
-------------------------------------------------