|
Organizers |
A Model Based Cut Elimination Proof
by
Olivier Hermant
INRIA (Paris, France)
INTRODUCTION
The sequent calculus modulo, introduced in [1] is a deduction system based on the fact that some axioms can be successfully replaced by rewrite rules on terms an on propositions. This permits to have a faster proof-search and more readable proofs. But in general case, we loose the cut-elimination property that we had for the sequent calculus, the fact that the cut elimination property holds or not depends on the considered rewrite system. On the other hand, we can express with the help of rewrite rules some powerful theories, such as Higher Order Logic [1] or Peano's arithmetic [2].
The paper [1] introduces a proof search system extending resolution for deduction modulo called Extended Narrowing And Resolution (ENAR). This method is proved complete for rewrite systems for which the cut elimination holds. Conversely, in [4] we have proved that the completness of ENAR implies the cut elimination property for sequent calculus modulo the same rewrite system.
Recent results of Stuber [5] prove the completness of ENAR using a semantic approach. Putting these two results together this leads to a new cut elimination theorem for the cases studied by Stuber [5]. In this paper, we give a direct proof of this cut elimination theorem avoiding the detour by the completness of ENAR.
In order to prove the cut-elimination theorem, we prove the completness of the cut-free sequent calculus modulo, that is, Gödel's completness theorem. Conversely, we prove the soundness theorem that is for any provable sequent G |-R D (possibly with cuts), we have G |= D (where G |= D means that for all models that validate G, at least one proposition of D is valid). These two results lead to the cut elimination theorem: if we have G |-R D, then, by soundness G |= D and by the completness theorem G |-Rcf D.
In order to prove the Gödel theorem for cut-free sequent calculus
modulo, we will modify the classical proof based on Henkin witnesses. In a
similar approach than in [5], we construct a model for a consistent,
complete theory that admits Henkin witnesses. We have other
modifications of the usual proof of the completness theorem due to the
fact that we consider cut-free proofs. For example, when we have a
consistent theory, G |-Rcf P does no more imply that we
don't have G, P |-Rcf.
DEDUCTION RULES
Sequent calculus
Sequent calculus is a proof method for propositions that is
equivalent to natural deduction. A sequent is written in the following
way: G |- D where G, D are multisets of
propositions. The proof of a sequent is made with the help of
deduction rules and the cut rule is the only rule where we have a
proposition P in premises that doesn't appears in the
conclusion. A theorem, proved by Gentzen, states that every
sequent that has a proof has also a cut-free proof. This theorem
implies the consistency of sequent calculus. Indeed, this is obvious
that the sequent |- has no cut-free proof.
Sequent calculus modulo
Proofs contain many steps that seem self-evident, because they are
based on computing, not on reasoning. Assume, for instance, that we
are using Peano's axioms, we would like to simplify propositions of
the form 2 + 2 = 4 into 4 = 4. The idea is to use a rewrite rule:
S(x) + y - > S(x + y) instead of the axiom S(x) + y = S(x + y). The
rewrite rules will not appear in the proof tree and thus proofs become
more compact and readable. Proof search is also improved, because we
have to search a more compact proof. Rules of the sequent calculus are
preserved, but we have a more liberal condition between the premises
and the conclusion, for instance, the /\-left rule
becomes:
From G, P, Q |-R D we can deduce G, R
|-R D if R =R (P /\ Q).
DEFINITION 1:
A rewrite rule on a term is a pair of term l - > r such that
variables of r appears in l.
A propositional rewrite rule is a pair of propositions l - >
r such that l is atomic and free variables of r appears in l.
A rewrite system written R is a set of propositional and term
rewrite rules.
Unfortunately, the cut elimination property doesn't hold and depends on the considered rewrite system.
We call the cut-free sequent calculus modulo the sequent calculus
modulo without the cut rule. We will consider this calculus
from now. And we will now write a sequent:
G |-Rcf D
We have a subscripted R to record that we are working with a rewrite
system. We extend the notion of model to the notion of model of the
rewrite rules. Basically, if two propositions are equal modulo the
rewrite rules, they must have the same denotation in the model.
RESULTS
LEMMA 1(Soundness):
If G |-R D (with possible cuts), then G
|= D.
COROLLARY 1:
If G |-Rcf D, then G |= D.
We prove the key lemma, that says that the cut rule is redundant
for normal atomic atoms.
LEMMA 2(Normal Atomic Cut Elimination):
Let G, D be multisets of propositions, and A a normal
atom. If we have G, A1, ..., An |-Rcf D and
G |- Rcf A, D, with A1 = R A2 = R... = R An = R A, we can construct a proof of:
G |-R D
For any consistent theory T, we construct a complete,
consistent theory G that admits Henkin witnesses. We then
construct a Herbrand model that validates G.
We then prove the completness and the cut-elimination theorems.
THEOREM 1(Completness):
Suppose we have a confluent rewrite system, a well-founded order
compatible with the rewrite rules and having the subterm property.
If T is a consistent theory, it has a model.
THEOREM 2(Cut elimination theorem):
If there exists a proof of: G |-R D
there exists a proof of: G |-Rcf D
We give an example of sets of rewrite rules that have the cut
elimination property. Theses rewrite systems are known as quantifier
free rewrite systems [3]. Many rules are quantifier free, for
instance, in set theory:
x in A \/ B - > x in A \/ x in B
x in A /\ B - > x in A /\ x in B
A complete version of the paper can be found at the URL: http://pauillac.inria.fr/~ohermant.
BIBLIOGRAPHY
[1] Dowek G., Hardin Th., Kirchner Cl., Theorem proving modulo, rapport de recherche 3400, INRIA, 1998
[2] Dowek G., Werner B., Peano's arithmetic as a theory modulo, manuscript, 2002
[3] Dowek G., Werner B., Proof Normalization Modulo, Altenkirch T., Naraschewski W., and Rues B. (Eds.), Types for Proofs and Programs 98, Lecture Notes in Computer Science 1657, Springer-Verlag, 1999, pp. 62-77. Rapport de Recherche 3542, INRIA, 1998
[4] Hermant O., Déduction modulo et élimination des coupures, une approche syntaxique, 2002
[5] Stuber J., A Model-based Completness Proof of Extended Narrowing And Resolution, In Proc. 1st Int. Joint Conf. on Automated Reasoning (IJCAR-2001), Siena, Italy, June 2001, LNCS 2083, Springer, Pages 195-210
Date received: March 14, 2003
Copyright © 2003 by the author(s). The author(s) of this document and the organizers of the conference have granted their consent to include this abstract in Atlas Mathematical Conference Abstracts. Document # cajy-09.