Subject: Re:Deduction modulo in CoS
Newsgroups: gmane.science.mathematics.frogs
Date: 2006-03-06 14:32:44 GMT (2 years, 9 weeks, 3 days, 21 hours and 5 minutes ago)
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