% Master File: gencomp.tex
\documentclass[letter,twoside,draft]{article}
\usepackage[latin1]{inputenc}
\usepackage[round,longnamesfirst]{natbib}
\usepackage{amsfonts,amssymb,amsmath,amsthm}
\usepackage{enumerate}
\usepackage{xspace}
\newcommand{\ie}{\textit{i.e.}\xspace}
\setlength{\columnseprule}{.3pt}
% evil hack straight from TeXbook
%% \def\ifundefined#1{\expandafter\ifx\csname#1\endcsname\relax}
%% \ifundefined{pdfoutput}
%% \usepackage%
%% [ps2pdf,pagebackref]
%% {hyperref}
%% \else
%% \usepackage{thumbpdf}
%% \usepackage%
%% [pdftex,
%% pdftitle={Cut Elimination in Deduction Modulo by Abstract Completion},
%% pdfauthor={Guillaume Burel and Claude Kirchner},
%% pagebackref,
%% bookmarks=true]
%% {hyperref}
%% \fi
\usepackage[cm,headings]{../aacs/myfullpage}
\usepackage{multicol}
\input{entete}
\input{../aacs/sequents}
\input{../sciacs/macros_modified}
\input{calseqmodfull}
\newenvironment{Proof}{\begin{proof}}{\end{proof}}
\newcommand{\todo}{\texttt}
\newcommand{\withappendix}[2]{#2}
\title{\bfseries Cut Elimination in Deduction Modulo\\ by Abstract
Completion (Full Version)}
\author{Guillaume Burel \and Claude Kirchner}
%
%\authorrunning{Guillaume Burel \and Claude Kirchner} % abbreviated author list (for running head)
%
%%%% modified list of authors for the TOC (add the affiliations)
%\tocauthor{Guillaume Burel \and Claude Kirchner (LORIA Nancy)}
%
%% \institute{%
%% École Normale Supérieure de Lyon \& LORIA\inst{3}
%% %\\\email{guillaume.burel@ens-lyon.org}
%% \and INRIA \& LORIA\inst{3}
%% %\\\email{Claude.Kirchner@loria.fr}
%% \and{\scriptsize UMR 7503 CNRS-INPL-INRIA-Nancy2-UHP}
%% }
\pagestyle{myheadings}
\markboth{Guillaume Burel and Claude Kirchner}{Cut Elimination in Deduction Modulo by Abstract Completion}
\begin{document}
\maketitle
\begin{center}
\begin{minipage}{.7\textwidth}
\begin{abstract}
Deduction Modulo implements Poincaré's principle by identifying deduction and computation
as different par\-a\-digms and making their interaction possible. This leads to logical
systems like the sequent calculus or natural deduction modulo. Even if deduction modulo is
logically equivalent to first-order logic, proofs in such systems are quite different and
dramatically simpler with one cost: cut elimination may not hold anymore. We prove
first that it is even undecidable to know, given a congruence over
propositions, if cuts can be eliminated in the sequent calculus modulo
this congruence.
Second, to recover the cut admissibility, we show how computation rules can be added following
the classical idea of completion \textit{a la} Knuth and Bendix. Because in deduction
modulo, rewriting acts on terms as well as on propositions, the objects are much more
elaborated than for standard completion. Under appropriate hypothesis, we prove that the
sequent calculus modulo is an instance of the powerful framework of \emph{abstract
canonical systems} and that therefore, cuts correspond to critical proofs that abstract
completion allows us to eliminate.
In addition to an original and deep understanding of the interactions between deduction
and computation and of the expressivity of abstract canonical systems, this provides a
mechanical way to transform a sequent calculus modulo into an
equivalent one admitting the cut rule, therefore extending in a significant way the applicability of
mechanized proof search in deduction modulo.
\textbf{Keywords:} Automated deduction and interactive theorem proving,
Knuth-Bendix completion, critical proofs, cut elimination, deduction modulo, proof ordering
\end{abstract}
\end{minipage}
\end{center}
\begin{multicols}{2}
\section{Introduction}
The complementarity and interaction between computation and deduction
is known since at least Henri Poincaré and deduction
modulo \citep{DHK-TPM-JAR} is a way to present first-order logic taking
advantage from this complementarity. Deduction modulo is at the heart
of proof assistants and proof search methods, either implicitly or
explicitly \citep[see for instance][]{PS81,BarendregtBarendsenJAR2002,DHK-TPM-JAR,Bonichon04} and
getting a deep understanding of its logical behavior is of prime
interest either for theoretical or practical purposes.
In deduction modulo, computations are modeled by a congruence relation between terms and
between propositions. The logical deductions are done modulo this congruence that is
often better represented by a rewrite relation over first-order terms and propositions,
leading to the asymmetric sequent calculus~\citep{DBLP:conf/rta/Dowek03}.
In the sequent calculus modulo, the Hauptsatz, \ie the fact that cuts
are not needed to build proofs, is no longer true as one can see from
an example derived from Crabbé's proof of the non-normalization
of Zermelo's theory \citeyearpar{Crabbe} \citep[see for
instance][]{DHK-TPM-JAR}. But we know that the admissibility of the
cut rule is fundamental for at least two related reasons: first, if a
system admits it, then the formul\ae\ needed to
build a sequent calculus proof of some sequent are
subformul\ae\footnote{In the case of deduction modulo, the intuitive
notion of subformula must take the considered rewrite relation into
account.}\ of the ones appearing in it, so that the search space is,
in a sense, limited. Such proofs are sometimes called \emph{analytic} \citep{DBLP:conf/rta/Dowek03}. The tableaux method is based on
this fact, and for instance TaMeD \citep{Bonichon04}, a tableaux method
based on deduction modulo, is shown to be complete only for cut-free
systems.
%This is the origin of the tableaux method.
On the other hand, it has been shown by \citet{hermantThese} that a proof search method for
deduction modulo like ENAR \citep{DHK-TPM-JAR}---which generalizes resolution and
narrowing---is equivalent to the cut-free fragment of deduction modulo. ENAR is therefore
complete if and only if the cut rule is admissible.
So on the one hand, we like to have a powerful congruence but this may
be at the price of loosing cut admissibility. How can we get both? It
has been shown by \citet{DBLP:conf/rta/Dowek03} that cut admissibility
is equivalent to the confluence of the rewrite system, provided only
first-order \textit{terms} are rewritten. It is no longer true when
\textit{propositions} are also rewritten, and the cut admissibility
property is in that case a stronger notion than confluence. Gilles
Dowek wanted therefore to build a generalized completion procedure
whose input is a rewrite system over first-order terms and atomic
propositions and computing a rewrite system such that the associated
sequent calculus modulo has the cut-elimination property. Such a
completion procedure was proposed for the quantifier free case by
\citet{dowek:theory}, based on the construction of a model for the
theory associated with the rewrite system.
To solve this question, including \emph{unlimited} use of quantifiers, we use here a quite
different approach based on the notion of abstract canonical system
and inference introduced by \citet{acp,aci}. This abstract framework is based on a proof
ordering whose goal is to apprehend the notion of proof quality from which the notions of
canonicity, completeness and redundancy follow up. It is shown to be adapted to existing completion
procedures such as ground completion \cite{DershowitzFTP2003} and standard
(a.k.a. Knuth-Bendix~\cite{KnuthBendix70}) completion \cite{BurelKirchner06}.
To present the general idea of our approach, let us consider the
simple example of Crabbé's axiom~\citeyearpar{Crabbe}
${A~\Leftrightarrow~B\wedge\neg A}$\footnote{In Crabbé's manuscript, $A$
represents $r_s\in r_s$ and $B$ $r_s\in s$ where $r_s$ is $\{x\in s\st
x\not\in x\}$. Then, there is a proof of $r_s\not\in s$ in
Zermelo's set theory that is not normalizing.}.
Can we find, for the sequent
calculus modulo the associated rewrite system $A\rightarrow
B\wedge\neg A$, a provable sequent without any cut-free proof? Indeed,
let us try to build a minimal example. We will show in
Prop.~\ref{prop:critproofs} that such a proof, in its simplest form,
is necessarily of the shape:
$$\Cut{A}{\seq}{ \Upl{A\seq}{ \infer*{A,B\wedge\neg A\seq}{}}}
{\Upr{\seq A}{ \infer*{\seq B\wedge\neg A,A}{}}}$$
\noindent where the rules
labeled ``\textrule{$\uparrow$-r}'' and ``\textrule{$\uparrow$-l}''
allow to apply the oriented axioms respectively on the right or on the
left. In order to validate this proof pattern, we have to check if it
is possible to close both sides of the proof tree, possibly adding
informations in the initial sequent.
First, we can trivially close the left part as follows:
$$\Andl{A,B\wedge\neg A\seq}{
\Notl{A,B,\neg A\seq}{
\Axiomm{A,B\seq A}}}\enspace.$$
Second, to close the right part, we must have a proof in the form:
$$ \Andr{\seq B\wedge\neg A,A} {\seq B,A} {\Notr{\seq \neg A,A}{
\Axiomm{A\seq A}}}\enspace.$$
To enforce the proof of $\seq B,A$, we must add either $A$ or $B$ to
the left of the sequent, and we only have to consider $B$, since we
have cut around $A$. We obtain the critical proof:
$$\Cut{A}{B\seq}{ \Upl{B,A\seq}{ \Andl{B,A,B\wedge\neg A\seq}{
\Notl{A,B,\neg A\seq}{ \Axiomm{A,B\seq A}}}}} {\Upr{B\seq A}{
\Andr{B\seq B\wedge\neg A,A} {\Axiomm{B\seq B,A}} {\Notr{B\seq
\neg A,A}{ \Axiomm{B,A\seq A}}}}}\enspace.$$
We can also easily show that there are no cut-free proof of $B\seq$,
simply because no inference rule is applicable to it except \textrule{Cut}.
If we
want to have a cut-free proof, we need to make $B$ reducible by the
congruence, hence the idea to complete the initial system with a new
rule which is a logical consequence of the current system. In our
case, we must therefore add the rule $B\rightarrow \bot$.
With this new rule, we will show that there are no more critical proofs and that therefore
the sequent calculus modulo the proposition rewrite system
$$\left\{\begin{array}{l}
A\rightarrow B\wedge\neg A\\
B\rightarrow \bot
\end{array}\right.$$ admits the cut rule and has the same expressive power as the
initial one.
The study of this question indeed reveals general properties of the sequent calculus
modulo and our contributions are the following:
\begin{itemize}
\item We provide an appropriate Noetherian ordering on the proofs of the sequent calculus
modulo a rewrite system; This ordering allows us to set on the proof space of sequent
calculus modulo a structure of abstract canonical system;
\item We characterize the critical proofs in deduction modulo as simple cuts;
\item By an appropriate correspondence between sequents and rewrite systems, we establish a
precise correspondence between the limit of a completion process and a cut free sequent
calculus;
\item We show the applicability of the general results, in particular on sequent calculus
modulo rewrite systems involving quantifiers, therefore generalizing all previously
known results;
\end{itemize}
As an important by-product of these results, we demonstrate the expressive power of
abstract canonical systems (ACS for short).
The next section will present the minimal knowledge needed on
deduction modulo and abstract canonical systems to make the paper
self-contained, and gives a proof of the undecidability of the
cut admissibility in deduction modulo. In Sect.~\ref{Instance of the
ACSI}, we show how to set, on the proof space of sequent calculus
modulo, a structure of abstract canonical system. In particular we
make precise why the postulates of ACS are fulfilled. This allows us
in Sect.~\ref{A Generalized Completion Procedure} to characterize the
critical proofs of deduction modulo and to set-up the completion
process as the appropriate (and indeed non-trivial) instance of the
abstract completion process. We also provide an algorithm to
systematically transform a set of sequents into an appropriate set of
proposition rewrite rule, therefore making the whole framework
operational. We conclude after presenting in more details Crabbé's
example as well as several examples involving quantifiers.
%% All proofs
%% will be found in% \withappendix{ the full version of this
%% %paper~\citep{gencomp_full}}{
%% the appendix.
\section{Prerequisites}\label{sec:prereq}
\subsection{Rewritings}
We define here how propositions are rewritten in deduction modulo.
%% We use standard definitions for terms, predicates, propositions (with
%% connectors $\neg,\imp,\wedge,\vee$ and quantifiers $\forall,\exists$),
%% substitutions, term rewrite rules and term rewriting, as can be found
%% in \cite{allThat,GallierLivreRevised}. The set of terms built from a
%% signature $\Sigma$ and a set of variables $V$ is denoted by
%% $\terms\Sigma V$, the replacement of a variable $x$ by a term $t$ in a
%% proposition $P$ by $\subst Ptx$, the application of a substitution
%% $\sigma$ in a proposition $P$ by $\sigma P$.
We denote by $\terms\Sigma V$ the set of \Def{terms} built from a
signature $\Sigma$ and a set of variables $V$. An \Def{atomic
proposition} is given by a predicate symbol $A$ of arity $n$ and by
$n$ terms $\vect t\in\terms\Sigma V$. It is denoted $A(\vect t)$.
\Def{Propositions} can be built using the following
grammar\footnote{$\inlinedf$ is used for definitions.}:
$$\mathcal P~\df~A~|~\neg \mathcal P~|~\mathcal P\wedge \mathcal
P~|~\mathcal P\vee \mathcal P~|~\mathcal P\imp \mathcal P~|~\forall
x.~\mathcal P~|~\exists x.~\mathcal P$$ where $A$ ranges over atomic
propositions and $x$ over variables. $P\Leftrightarrow Q$ will be
used as a syntactic sugar for ${(P\imp Q)\wedge(Q\imp P)}$, as well as
$\bigwedge\Gamma$ for $P_1\wedge\ldots\wedge P_n$, and $\bigvee\Gamma$ for
$P_1\vee\ldots\vee P_n$ if $\Gamma=\vect P$. Free variables and
substitutions are defined as usual. The replacement of a variable $x$
by a term $t$ in a proposition $P$ is denoted by $\subst Ptx$.
\medskip
A \Def{term rewrite rule} is the pair of terms $l,r$ such that all
free variables of $r$ appear in $l$. It is denoted $l\rightarrow r$. A
\Def{term rewrite system} is a set of term rewrite rules.
A term $s$ can be rewritten to a term $t$ by a term rewrite rule
$l\rightarrow r$ if there exists some substitution $\sigma$ and some
position $\mathfrak p$ in $s$ such that $\sigma l=\subterm s{\mathfrak
p}$ and $t = \replacement s{\sigma r}{\mathfrak p}$.
An atomic
proposition $A(s_1,\ldots,s_i,\ldots,s_n)$ can be rewritten to the
atomic proposition $A(s_1,\ldots,t_i,\ldots,s_n)$ by a term rewrite
rule $l\rightarrow r$ if $s_i$ can be rewritten to $t_i$ by
$l\rightarrow r$.
A \Def{proposition rewrite rule} is the pair of an atomic proposition
$A$ and a proposition $P$, such that all free variables of $P$ appear
in $A$. It is denoted $A\rightarrow P$. A \Def{proposition rewrite
system} is a set of proposition rewrite
rules. The set of all proposition rewrite systems is denoted
$\mathcal{PRS}$.
An atomic proposition $A$ can be rewritten to a proposition $P$ by a
proposition rewrite rule $B\rightarrow Q$ if there exists some
substitution $\sigma$ such that $\sigma B=A$ and $\sigma
Q=P$. Semantically, this proposition rewrite relation must be seen as
a logical equivalence between propositions.
Note that we do not define how to rewrite non-atomic propositions by
proposition rewrite rules, as in \citet{DHK-TPM-JAR}, because this
can be simulated in the sequent calculus modulo we present in the
next section.
In the following, the term rewrite system used in addition to all the
proposition rewrite systems we will consider is fixed. It is supposed
to be \emph{terminating and confluent}. It will be denoted $\Rterms$.
The \Def{subformula relation} $\subformula$ is the least transitive
relation such that:
\begin{itemize}
\item $P\subformula P_i$ if $P=P_1\wedge P_2$, $P=P_1\vee P_2$ or
$P=\neg P_1$;
\item $P\subformula \subst Qtx$ if $P=\forall x.~Q$ or $P=\exists x.~Q$;
\item $P\subformula Q$ if $P$ can be rewritten to $Q$ by $\Rterms$
\end{itemize}
for all terms $t$, variables $x$ and propositions
$P,Q,P_1,P_2$. It is well-founded because of the termination of $\Rterms$.
\subsection{Sequent Calculus Modulo}
Sequent calculus modulo can be seen as an extension of the sequent
calculus of \citet{gentzen:untersuchungen}. We will use the
denominations of \citet{GallierLivreRevised}.
A \Def{sequent} is a pair of multisets of propositions $\Gamma,\Delta$. It is
denoted by $\Gamma\seq\Delta$. The sets of all sequents will be
denoted $\Sequents$. For a sequent $\Gamma\seq\Delta$, if $\vect x$
are the free variables of $\Gamma,\Delta$, we will denote by
$\Prop\Gamma\Delta$ the proposition $\forall\vect x.~\left(\bigwedge\Gamma\imp\bigvee\Delta\right)$.
In Fig. \ref{fig:seqmod} we present the inference rules of our
\Def{sequent calculus modulo}. They differ from the ones of
\citet{DBLP:conf/rta/Dowek03} because the congruence is externalized
through specific inference rules \textrule{$\uparrow$-l} and
\textrule{$\uparrow$-r} \citep[as can be found][]{hermantThese,wack},
whereas contraction is internalized. \Def{Proofs} are trees labeled
by sequents built using these rules, and where all leaves are
\textrule{Axiom}s. The root sequent is called the \Def{conclusion}. In
the following, a double horizontal bar will mean several applications
of an inference rule. A proof is said to be built in the proposition
rewrite system $R$ if all \textrule{$\uparrow$-l} and
\textrule{$\uparrow$-r} use only rules that appear in
$R\cup\Rterms$. The set of all proofs will be denoted by
$\mathcal{SQM}$.
%
\begin{rules}[ht]{fig:seqmod}{Sequent Calculus Modulo}
\Rule{Identity Group:}
\begin{center}
~~~~~~~~~~~~~~$\Axiomm{\Gamma,P\seq\Delta,P}$~~~~~~~
$\Cut{P}{\Gamma\seq\Delta}{\Gamma,P\seq\Delta}{\Gamma\seq P,\Delta}$
\end{center}
\bigskip
\Rule{Logical Rules:}
\begin{center}
\begin{tabular}{r@{~~~~~~~}l}
$\Notl{\Gamma,\neg P\seq\Delta}{\Gamma\seq P,\Delta}$ &
$\Notr{\Gamma\seq\neg P,\Delta}{\Gamma,P\seq\Delta}$
\\
\\
$\Andl{\Gamma,P\wedge Q\seq\Delta}{\Gamma,P,Q\seq\Delta}$&
$\Andr{\Gamma\seq P\wedge Q,\Delta}{\Gamma\seq P,\Delta}{\Gamma\seq Q,\Delta}$
\\ \\
$\Orl{\Gamma, P\vee Q\seq\Delta}{\Gamma, P\seq\Delta}{\Gamma,
Q\seq\Delta}$ &
$\Orr{\Gamma\seq P\vee Q,\Delta}{\Gamma\seq P,Q,\Delta}$
\\ \\
$\Impl{\Gamma, P\imp Q\seq\Delta}{\Gamma, Q\seq\Delta}{\Gamma,
\seq P,\Delta}$ &
$\Impr{\Gamma\seq P \imp Q,\Delta}{\Gamma,P\seq Q,\Delta}$
\\ \\
$\Alll{\Gamma,\forall x.~P\seq\Delta}{\Gamma,\forall x.~P,\subst
Ptx\seq\Delta}$, $t\in\terms\Sigma V$
&
\begin{tabular}{l}$\Allr{\Gamma\seq\forall x.~P,\Delta}{\Gamma\seq\subst
Pcx,\Delta}$,\\ $c$ free constant ($c\not\in\Sigma\cup V$)
\end{tabular}
\\ \\
\begin{tabular}{r}
$\Exl{\Gamma,\exists x.~P\seq\Delta}{\Gamma,\subst
Pcx\seq\Delta}$,\\ $c$ free constant ($c\not\in\Sigma\cup V$)
\end{tabular}
&
$\Exr{\Gamma\seq\exists x.~P,\Delta}{\Gamma\seq\exists x.~P,\subst
Ptx,\Delta}$, $t\in\terms\Sigma V$
\end{tabular}
\end{center}
\bigskip
\Rule{Rewrite Rules:}
if $A$ can be rewritten to $P$, either by a term
or a proposition rewrite rule (in one step),
\begin{center}
$\Upl{\Gamma,A\seq\Delta}{\Gamma,A,P\seq \Delta}$~~~~~~~
$\Upr{\Gamma\seq A,\Delta}{\Gamma\seq A, P,\Delta}$
\end{center}
\end{rules}
% \begin{rules}[t]{fig:seqmod}{Sequent calculus modulo}
%% \begin{minipage}{.90\textwidth}
%% \smallskip
%% \begin{tabular}{@{}lc@{~~~~~}c}
%% \Rule{Identity Group:}&$\Axiomm{\Gamma,P\seq\Delta,P}$ &
%% $\Cut{P}{\Gamma\seq\Delta}{\Gamma,P\seq\Delta}{\Gamma\seq
%% P,\Delta}$\\
%% \\
%% \Rule{Logical Rules:}&$\Notl{\Gamma,\neg P\seq\Delta}{\Gamma,\neg P\seq P,\Delta}$ &
%% $\Exr{\Gamma\seq\exists x.~P,\Delta}{\Gamma\seq\exists x.~P,\subst
%% Ptx,\Delta}$, $t\in\terms\Sigma V$
%% \\\\ \end{tabular}
%% \Rule{Rewrite Rules:} if $A$ can be rewritten to $P$, either by a term
%% or a proposition rewrite rule (in one step),\smallskip\\
%% \parbox{\textwidth}{\centering
%% $\Upl{\Gamma,A\seq\Delta}{\Gamma,A,P\seq \Delta}$~~~~~
%% $\Upr{\Gamma\seq A,\Delta}{\Gamma\seq A, P,\Delta}$
%% }\smallskip
%% \end{minipage}
%% \end{rules}
\textrule{Cut($P$)} permits essentially to extend the proof search space
with the proposition $P$. Logical Rules decompose some proposition
which is called \Def{principal}. Rewrite Rules, that do not appear in
Gentzen's sequent calculus, introduce proposition rewriting into the
proof system. Note that only atomic propositions are rewritten.
A proposition rewrite system $R$ is said to \Def{admit \RCut} if for
all sequents $s\in\Sequents$, $s$ has a proof in $R$ if and only if
$s$ has a proof in $R$ without using \RCut. It is well-known
(Gentzen's Hauptsatz \citeyearpar{gentzen:untersuchungen}, or more accuratly
\cite{DBLP:conf/rta/Dowek03} because of $\Rterms$) that
$\emptyset$ admits \RCut.
It is important to be aware that free variables appearing in a
sequents play the same role as fresh constants, because no inference
rules can modify them. As a consequence, one can restrict oneself to
closed sequents, as indicated by \citet[Proposition 1.5]{DHK-TPM-JAR}.
\longv{%
\begin{lemma}[Weakening Lemma]\label{lemma:weakening}
If there exist a proof of $\Gamma\seq\Delta$, then for all
propositions $P$ there exists proofs of $\Gamma,P\seq\Delta$ and
$\Gamma\seq P,\Delta$.
\end{lemma}
\begin{Proof}
$P$ can be propagated in the first proof until \textrule{Axiom}s.
\end{Proof}
\begin{lemma}[Contraction Lemma]\label{lemma:contraction}
There exist a proof of $\Gamma,P\seq\Delta$ if and only if there exists
a proof of $\Gamma,P,P\seq\Delta$.
There exist a proof of $\Gamma\seq P,\Delta$ if and only if there exists
a proof of $\Gamma\seq P,P,\Delta$.
\end{lemma}
\begin{Proof}
By induction on the structure of the proof. See Kleene Lemma \citep[Lemme 3.3]{hermantThese}.
\end{Proof}
\begin{note}
The premises $\Gamma$ and conclusions $\Delta$ of sequent
$\Gamma\seq\Delta$ can therefore be considered as sets.
\end{note}
%% \begin{lemma}[Axiom Lemma]
%% For all propositions $P$ and propositions multisets $\Gamma,\Delta$,
%% there exists a proof of $\Gamma, P\seq\Delta,P$.
%% \end{lemma}
%% \begin{proof}
%% By induction on $P$. If $P$ is atomic use \textrule{Axiom}. If the
%% root of $P$ is a connector $\delta$, use \textrule{$\delta$-l} and
%% apply \textrule{$\delta$-r} to the premises; one can apply the
%% induction hypothesis to the resulting premises. If $P$ is $\forall
%% x.~Q$ first use \textrule{$\forall$-r}, which introduce a fresh
%% constant $c$. Then apply \textrule{$\forall$-l} with $t=c$. We can
%% finish the proof using the induction hypothesis. The case
%% $P=\exists x.~Q$ is dual.
%% \end{proof}
\begin{lemma}[Rewrite Lemma]\label{lemma:rewrite}
If $P\rewrite^* Q$ and there exists a proof of $\Gamma, Q\seq\Delta$,
then there exists a proof of $\Gamma, P\seq\Delta$.
\end{lemma}
\begin{Proof}
If $P\rewrite Q$, then there exists some atomic proposition $A$ in
$P$ at some position $p$, and some rewrite rule $A\ra R$ such that
$Q=\replacement P R p$. Therefore, we can apply to $P$ all the
logical rules applied to $Q$ in the proof of $\Gamma, Q\seq\Delta$,
except the one applying to $R$ because it is replaced by $A$. We must
here first apply the rewrite rule $A\ra R$, and then follow on. We
obtain by this process a proof of $\Gamma, P\seq\Delta$.
We can conclude by induction on the length of the rewrite derivation
$P\rewrite^* Q$.
\end{Proof}
}
\shortv{This sequent calculus has the weakening and the contraction properties:
\begin{itemize}
\item if there exist a proof of $\Gamma\seq\Delta$, then for all
propositions $P$ there exists proofs of $\Gamma,P\seq\Delta$ and
$\Gamma\seq P,\Delta$;
\item there exist a proof of $\Gamma,P\seq\Delta$ if and only if there
exists a proof of $\Gamma,P,P\seq\Delta$, and there exist a proof of
$\Gamma\seq P,\Delta$ if and only if there exists a proof of
$\Gamma\seq P,P,\Delta$.
\end{itemize}
%%
%% One can also show that one can simulate the rewriting of a non-atomic
%% proposition, essentially because rewriting only atoms does not break
%% the logical structure of propositions.
}
\begin{proposition}[Equivalence]\label{prop:equiv}
The sequent calculus modulo presented in Figure \ref{fig:seqmod} is
equivalent to the Asymmetric Sequent Calculus Modulo of
\citet{DBLP:conf/rta/Dowek03} (also w.r.t to cut-free proofs).
\end{proposition}
\begin{Proof}
It is quite clear that the inference rules of our system can be
derived in G. Dowek's one.
Conversely, the absence of a weakening rule can be solved by the fact
that our \textrule{Axiom} rule accepts side propositions, so that the
weakened propositions can be kept until the \textrule{Axiom}s.
The absence of contraction rule is not a problem, because the only
inference rules where it could be problematic are
$\forall\textrule{-l}$, $\exists\textrule{-r}$,
$\uparrow\textrule{-l}$ and $\uparrow\textrule{-r}$, and the
contraction is
integrated in them.
Then, one can show that for a proposition rewrite rule $A\rightarrow
P$, if there exists a proof of $\Gamma, C[P]\seq\Delta$ for some
propositional context $C$, then there exists a proof of $\Gamma,
C[A]\seq\Delta$: we can apply to $C[A]$ all the
logical rules applied to $C[P]$ in the proof of $\Gamma,
C[P]\seq\Delta$, except the one applying to $P$ because it is replaced
by $A$. We must here first apply the rewrite rule $A\ra P$, and then
follow on. We obtain by this process a proof of $\Gamma,
C[A]\seq\Delta$. The same is true at the right of a
sequent. Consequently one can simulate rewriting non-atomic proposition.
Using this, one can transform the side conditions of G. Dowek's system
into applications of \textrule{$\uparrow$-l} and
\textrule{$\uparrow$-r}. This implies that a proof in Dowek's system
can be transformed into a proof in our system.
Of course, as we have seen, both system are also equivalent regarding
cut-free proofs, since we did not need any \textrule{Cut}.
\end{Proof}
\longv{\begin{Proof}
This is a consequence of the four previous lemmata. We can embed
\textrule{$\uparrow$-l} and \textrule{$\uparrow$-r} into the other
rules to obtain the rules of \citet{DBLP:conf/rta/Dowek03}.
\end{Proof}}
\subsection{Properties of the Sequent Calculus Modulo}
We present here some properties of the sequent calculus modulo, which
are slight generalization of \citet{hermant-stpeter}
\citep[and][]{hermantThese}. In particular, we introduce the notion of
semantically sound rewrite systems, which implies cut admissibility,
and we prove that the cut admissibility is not decidable.
\smallskip
Our system satisfies the Kleene Lemma: \lsv{ \todo{Detailed version of
Kleene Lemma + proof} } {\begin{lemma}[Kleene Lemma {\citep[Lemme
3.3]{hermantThese}}]\label{lemma:kleene} If a sequent,
containing the non-atomic formula $P$, has a proof (resp. cut-free
proof) in $R$, then it has a proof (resp. cut-free proof) in $R$
whose first rule is a logical rule with principal proposition $P$.
\end{lemma}
\begin{proof}
This is slightly more general than \citet[Lemme 3.3]{hermantThese},
because we also look at $\forall\textrule{-l}$ and
$\exists\textrule{-r}$. But, for instance, if there is a proof $\Gamma, \forall
x.~P\seq\Delta$, by weakening there is a proof of $\Gamma, \forall
x.~P, \subst Ptx\seq\Delta$.
\end{proof}
}
We need the following definitions, whose motivations can be found in
\citet{hermant-stpeter}:
\begin{definition}[Properties of a theory]
Given a rewrite system $R$, a theory $\Gamma$:
\begin{itemize}
\item is \Def{complete} iff for all propositions $P$, either $\Gamma,
P\seq$ or $\Gamma\seq P$ has a cut-free proof in $R$;
\item is \Def{consistent} iff there is no cut-free proof of $\Gamma\seq$
in $R$;
\item \Def{admits Henkin witnesses} iff for all propositions $Q$ with one free
variable $x$, there is a constant $c$ of the language such that
\begin{itemize}
\item if $\Gamma, \exists x.~Q\seq$ has no cut-free proof in $R$, then
$\subst Qcx$ is in $\Gamma$;
\item if $\Gamma\seq \forall x.~Q$ has no cut-free proof in $R$, then
$\neg\subst Qcx$ is in $\Gamma$.
\end{itemize}
\end{itemize}
\end{definition}
Models in deduction modulo are standard boolean models, except that
they are compatible with the rewrite system:
\begin{definition}[Model for a rewrite system]
A boolean model $\mathcal M$ is a \Def{model for the rewrite system}
$R$ if for all propositions $P$ and $Q$, $P\sRew[R] Q$ implies that $P$
and $Q$ are interpreted the same way in $\mathcal M$.
\end{definition}
We introduce the new notion of semantically sound rewrite system:
\begin{definition}[Semantical soundness]
A rewrite system $R$ is said \Def{semantically sound} if every
complete, consistent theory which admits Henkin
witnesses has a model for $R$.
\end{definition}
\begin{proposition}[Semantical soundness implies cut admissibility]\label{prop:sc=>ca}
If $R$ is semantically sound, then $R$ admits \RCut.
\end{proposition}
\begin{proof}
As proved by \citet[Lemma 3]{hermant-stpeter}, if
$\Gamma\seq\Delta$ has a proof in $R$, then any model
$\mathcal M$ for $R$ interprete $\neg\Gamma,\Delta$ as true.
It remains to be proved that if any model
$\mathcal M$ for $R$ interprete $\neg\Gamma,\Delta$ as true then
$\Gamma\seq\Delta$ has a \emph{cut-free} proof in $R$.
If $\Gamma,\neg\Delta$ is inconsistent, by definition $\Gamma,\neg\Delta\seq$ has a proof in
$R$, and by Lemma \ref{lemma:kleene} so does $\Gamma\seq\Delta$.
If $\Gamma,\neg\Delta$ is consistent, then using \citet[Section
6.1]{hermant-stpeter}, we can complete it into a consistent,
complete theory $\Gamma'$ which admits Henkin witnesses. By hypothesis
(semantical soundness), $\Gamma'$ has a model $\mathcal M$ for $R$.
Furthermore, by construction of $\Gamma'$ this model is also a model
for $\Gamma,\neg\Delta$. Consequently, this model for $R$ does not
interprete $\neg\Gamma,\Delta$ as true.
\end{proof}
This proposition permits to prove the main theorem of this first section:
\begin{theorem}[Undecidability of the Cut Admissibility]
The problem
\begin{quote}
Input: A propositional rewrite system $\mathcal R$
Decide if $\mathcal R$ admits \RCut.
\end{quote}
is undecidable.
\end{theorem}
\end{multicols}
\begin{proof}
We reduce to the validity problem in first-order logic. We recall
the reader that this problem is undecidable in the empty theory when
the language contains at least a binary predicate.
Let $P$ be a first-order proposition.
Let $R$ be a constant and $\in$ a 2-ary predicate not appearing in
$P$. Consider the propositional rewrite system
\citep[inspired by][Chapter 8]{hermantThese}
$$\mathcal R=\Big\{R\in R\ra \forall y.~(\forall x.~y\in x\imp R\in
x)\imp y\in R\imp P\enspace.$$
Then we show that $P$ is valid if and only if $\mathcal R$
admits \RCut:
If $P$ is valid, then $R$ is semantically sound: given a complete,
consistent theory $\Gamma$ which admits Henkin witnesses, let
$\mathcal M$ be the model defined as follows: Its support is the set
of closed terms. The atomic predicate $A$ is interpreted as true by
$\mathcal M$ iff $\Gamma\seq A$ has a cut-free proof in $R$. Because
of the completeness of the theory, and the fact that it admits
Henkin witness, this permits to define the model for all
propositions \citep[see][Lemma 8]{hermant-stpeter}. This definition
is well-founded by consistency. Then $R\in R$ has the following
cut-free proof in $R$:
$$\Upr{\seq R\in R}{\Allr{\seq R\in R,\forall y.~y\simeq R\imp y\in R\imp P}{ \Impr{\seq
R\in R,c_0\simeq R\imp c_0\in R\imp P}{ \Impr{c_0\simeq R\seq R\in
R,c_0\in R\imp P}{ \Alll{c_0\simeq R,c_0\in R\seq R\in R,P}{
\Impl{c_0\in R\imp R\in R,c_0\in R\seq R\in R, P}{
\Axiomm{R\in R,c_0\in R\seq R\in R, P}}{\Axiomm{c_0\in R\seq c_0\in
R,R\in R, P}}}}}}}\enspace.
$$ By weakening $\Gamma\seq R\in R$ has a cut-free proof in $R$, and
$R\in R$ is interpreted as true by $\mathcal M$. As $P$ is valid, it
is interpreted as true in particular in $\mathcal M$. Therefore, the
interpretation of $\forall y.~(\forall x.~y\in x\imp R\in
x)\imp y\in R\imp P$ is also true. Thus, if $P_1\sRew[R]P_2$ then
they have the same interpretation in $\mathcal M$, which is
therefore a model for $R$. Therefore $R$ is semantically sound and by
Proposition \ref{prop:sc=>ca} it admits \RCut.
Reciprocally, suppose $P$ is not valid. By soundness of the
sequent calculus of Gentzen, $\seq P$ does not have any proof in
$\emptyset$. Consequently, it does not have any cut-free proof in
$\mathcal R$. Indeed, since $R$ and $\in$ do not appear in $P$,
they cannot appear in a cut-free proof of $\seq P$, so that no
rewrite rule could be applied in a cut-free proof of $\seq P$.
Nevertheless, there is a proof of $P$ in $\mathcal R$: above is a
proof of $\seq R\in R$, and here is a proof of $R\in R\seq P$
$$ \Upl{R\in R\seq P}{\Alll{R\in R,\forall y.~y\simeq R\imp y\in R\imp P\seq P}{ \Impl{R\in
R,R\simeq R\imp R\in R\imp P\seq P}{ \Impl{R\in R,R\in R\imp
P\seq P}{\Axiomm{ R\in R,P\seq P}}{\Axiomm{R\in R\seq P, R\in R}}}{ \Allr{R\in
R\seq P, R\simeq R}{ \Impr{R\in R\seq P, R\in c_1\imp R\in c_1}{
\Axiomm{R\in R, R\in c_1\seq P, R\in c_1}}}}}}\enspace.
$$ Consequently, $\mathcal R$ does not admit \RCut.
\end{proof}
\begin{multicols}{2}
\begin{note}
This proof was deeply inspired by the proof of \citet[Chapter
8]{hermantThese} that there exists terminating and confluent rewrite
systems that admits \RCut, but in which some proof is not normalizing.
\end{note}
\subsection{Abstract Canonical Systems and Inference}\label{section ACSI}
The results in this section are extracted from \citet{DershowitzKirchner-lics2003,acp,aci}, which
should be consulted for motivations, details and proofs. %% The proofs mentioned here, unless
%% otherwise specified by a reference, are corrections from the original
%% ones.
Let $\A$ be the set of all formul\ae\ over
some fixed vocabulary. Let $\P$ be the set
of all proofs. These sets are linked by two functions: $\Ax\cdot:\P\rightarrow 2^\A$ gives
the \Def{premises} in a proof, and
$\Cl\cdot:\P\rightarrow \A$ gives its
\Def{conclusion}. Both are extended to sets of proofs in the usual
fashion. The set of proofs built using assumptions in $A\subseteq\A$
is denoted by $$\Pf A\df \left\{p\in\P :
\Ax p\subseteq A\right\}\enspace.$$
The framework described here is predicated on two {\em well-founded}
partial orderings over $\P$: a \Def{proof ordering} $>$ and a
\Def{subproof relation} $\rhd$. They are related by a monotonicity
requirement (postulate \ref{post:replacement}). We assume for
convenience that the proof ordering only compares proofs with the same
conclusion ($p> q\Rightarrow \Cl p=\Cl q$), rather than mention this
condition each time we have cause to compare proofs.
We will use the term \Def{presentation} to mean a set of
formul\ae, and \Def{justification} to mean a set of proofs. We
reserve the term \Def{theory} for deductively closed
presentations:
$$
\Th A ~~\df~~ \Cl{\Pf A} ~~=~~ \{\Cl p \st p\in\P,~ \Ax p
\subseteq A\}\enspace.
$$
%% Theories are monotonic:
%% \begin{proposition}[Monotonicity~{\cite[Prop. 12]{acp}}]\label{prop:mono}
%% For all presentations $A$, $B$:
%% $$ A\subseteq B \imp \Th A\subseteq \Th B$$
%% \end{proposition}
Presentations $A$ and $B$ are \Def{equivalent}
($A ~\equiv ~ B $) if their theories are
identical: $\Th A = \Th B$.
In addition to this, we assume the two following postulates:
\begin{post}[Reflexivity]\label{post:refl}
For all presentations $A$:
$$ A\subseteq \Th A$$
\end{post}
\begin{post}[Closure]\label{post:closure}
For all presentations $A$:
$$ \Th{\Th A}\subseteq \Th A$$
\end{post}
We call a proof
\Def{trivial} when it proves only its unique assumption and has no
subproofs other than itself, that is, if $\Ax p = \{\Cl p\}$ and
$p\unrhd q\Rightarrow p=q$, where $\unrhd$ is the reflexive closure of
the subproof ordering $\rhd$. We denote by $\triva
a$ such a trivial proof of $a\in\A$
and by $\triva A$ the set of trivial proofs of each $a\in A$.
We assume that proofs use their assumptions (postulate
\ref{post:premSubproofs}), that subproofs don't use non-existent
assumptions (postulate \ref{post:premMono}), and that proof orderings
are monotonic with respect to subproofs (postulate \ref{post:replacement}):
\begin{post}[Trivia]\label{post:premSubproofs}
For all proofs $p$ and formul\ae\ $a$:
$$a\in\Ax p \imp p\unrhd\triva a$$
\end{post}
\begin{post}[Subproofs Premises Monotonicity]
\label{post:premMono}
For all proofs $p$ and $q$:
$$p\unrhd q\imp \Ax p\supseteq \Ax q$$
\end{post}
\begin{post}[Replacement]\label{post:replacement}
For all proofs $p$, $q$ and $r$:
$$p\rhd q > r \imp \exists v\in \Pfa{\Ax p\cup\Ax r}.~ p > v\rhd r$$
\end{post}
We make no other assumptions regarding proofs or their structure and
the proof ordering $>$ is lifted to a quasi-ordering $\simpler$ over
presentations:
$$A\simpler B\mbox{ if }A~\equiv~ B\mbox{ and }\forall p\in\Pf A.~\exists q\in\Pf B.~p\geq q\enspace.$$
We define what a \emph{normal-form proof} is, i.e. one of the
minimal proofs of $\Pf{\Th A}$:$$\Nf A \begin{array}[t]{l@{}}\df\mu\Pf{\Th A}\\
\df \{p\in\Pf{\Th A}~:~\neg\exists q\in\Pf{\Th
A}.~p>q\}
\end{array}
$$
The \Def{canonical presentation} contains those formul\ae\ that
appear as assumptions of normal-form
proofs:
\[ A^\sharp \df \Ax{\Nf A}\enspace. \]
So, we will say that $A$ is \Def{canonical} if $A=A^\sharp$.
A presentation $A$ is \Def{complete} if every theorem has a
normal-form proof:
$$\Th A=\Cl{\Pf A\cap\Nf A}$$ Canonicity implies completeness, but the
converse is not true.
%% The set of all \Def{redundant formul\ae} of a given presentation $A$
%% will be denoted as follows:
%% \[
%% \Red A ~~\df~~ \left\{r \in A \st A \simpler A\setminus
%% \{r\}\right\} \enspace .\]
%% and a presentation $A$ is \Def{contracted} if
%% $$ \Red A = \emptyset \enspace.$$
%% The following main result can then be derived~\cite{DershowitzKirchner-lics2003}:
%% \begin{theorem}[{\cite[Proposition 63]{acp}}]
%% A presentation is canonical iff it is saturated and contracted.
%% \end{theorem}
We now consider inference and deduction mechanisms.
A \Def{deduction mechanism} $\infers$ is a function from
presentations to presentations and we call the relation
$A \infers B$ a \Def{deduction step}.
%
A sequence of presentations $A_0 \leadsto A_1 \leadsto \cdots$ is
called a \Def{derivation}.
%
The \emph{result} of the derivation is, as usual, its
\Def{persisting} formul\ae:
$$A_\infty \df \liminf_{j\rightarrow\infty} A_j ~=~ \bigcup\limits_{j>0}
\bigcap\limits_{i>j} A_i \enspace.$$
%% We also define the set of all generated
%% formul\ae:
%% $$A_*=\bigcup\limits_{i>0}A_i$$
%% A deduction mechanism $\infers$ is \Def{sound} if $A \infers B$
%% implies $\Th B \subseteq \Th A$. It is \Def{adequate} if $A \infers
%% B$ implies $\Th A \subseteq \Th B$. It is \Def{good} if proofs only
%% get better:
%% $$
%% \infers ~\subseteq~ \simpler
%% \enspace.$$
%% A derivation $A_0 \leadsto A_1 \leadsto \cdots$ is \Def{good} if
%% $A_i \simpler A_{i+1} $ for all $i$.
%% We now extend the notion of saturation and contraction to
%% derivations:
%% \begin{itemize}
%% \item A derivation $\{A_i\}_i$ is \Def{saturating} if $A_\infty$ is
%% saturated.
%% \item It is \Def{contracting} if $A_\infty$ is contracted.
%% \item It is \Def{canonical} if both saturating
%% and contracting.
%% \end{itemize}
%% \medskip
A deduction mechanism is \Def{completing} if for each step $A\leadsto
B$, $A\simpler B$, and the limit $A_\infty$ is
complete.
A completing mechanism can be used to build normal-form proofs of
theorems of the initial presentation:
\begin{theorem}[{\citet[Lemma 5.13]{aci}}]\label{lemma:limit_canon}
A deduction mechanism is completing if and only if for all derivations
$A_0 \leadsto A_1 \leadsto \cdots$,
$$\Th{A_0}\subseteq \Cl{\Pf{A_\infty}\cap\Nf{A_0}}\enspace.$$
\end{theorem}
A \Def{critical proof} is a minimal proof which is not in normal form, but
whose strict subproofs are:
$$\Crit A\df\left\{
\begin{array}{l}
p\in\mu\Pf{A}\setminus\Nf{A}\st\\\forall q\in\Pf{A}.~p\rhd
q\imp q\in\Nf{A}
\end{array}\right\}$$
\Def{Completing formul\ae}\ are conclusions of
proofs smaller than critical proofs:
$$\Comp{A}\df\bigcup_{p\in\Crit A~\wedge~p'\text{ is any proof
such that }p>p'}\Ax{p'}
$$
In this paper, we use a completing deduction mechanism in the
following way:
$$A\infers A\cup \textsf C(A)$$
where $\Comp{A}\subseteq\textsf C(A)\subseteq\Th{A}$.
\begin{proposition}[{\citet[Lemma 10]{DershowitzKirchner-lics2003}}]
\label{prop:satcpc}
This deduction mechanism is completing.
\end{proposition}
\section{Deduction Modulo is an Instance of ACS}\label{Instance of the ACSI}
We want to show that the sequent calculus modulo can be seen as an
instance of ACS. For this purpose, we have to define
what the formul\ae, the proofs, the premises and conclusions are, and
to give the appropriate orderings. After this, we need to check that
the postulates are verified by the defined instance.
\subsection{Proofs and Formulae}
%% We restrict here the formul\ae\ that one can use in the sequents. This
%% is due to the fact that we need a correspondence between sequents and
%% proposition rewrite systems. Such a restriction will be presented in
%% Section \ref{sec:restriction}.
We aim to obtain cut-free proofs, so that the natural candidate for
ACS proofs are sequent calculus proofs. \longv{Because of Lemmata
\ref{lemma:weakening} and \ref{lemma:contraction}}\shortv{Because of
the weakening and contraction properties}, we can restrict ourselves
to proofs using minimal sets of propositions in their
conclusions. More precisely, we can consider only proofs where all the
propositions appearing in the conclusion are used as principal
propositions somewhere in the proof, or in one of the
\textrule{Axiom}s.
\medskip
The completion procedure we want to establish deals with rewrite rules
over atomic propositions. Nevertheless, the conclusions of the
proofs, from which we want to generate the rewrite rules added by the
completion mechanism, are sequents. In other words, sequents must
be identified with proposition rewrite systems.
Therefore we suppose that there exists a function between sequents and
proposition rewrite systems
$Rew:~\Sequents~\rightarrow \mathcal{PRS}$ such that:
\begin{property}\label{hyp:compat} For all sequents $\Gamma\seq\Delta$,
$R=Rew(\Gamma\seq\Delta)$ and $\Prop\Gamma\Delta$ are
strongly compatible% in the sense of Definition 1.4 of \cite{DHK-TPM-JAR} (in
% fact, we present here a stronger hypothesis)
:\begin{enumerate}[(a)]
\item\label{hyp:compattheory} for all propositions $P,Q$,
$P\mathop{\longleftrightarrow}\limits_R^*Q$ implies that there
exists a proof of ${\Prop\Gamma\Delta\seq
P\Leftrightarrow Q}$ in $\emptyset$ (i.e. without rewrite rules);
\item\label{hyp:compatproof} there exists a cut-free proof of
$\seq\Prop\Gamma\Delta$ in $R$.
\end{enumerate}
\end{property}
\begin{property}
\label{hyp:samecf} For all proposition rewrite system $R$, for all sequents $s$ and
$s'$, if $Rew(s)=Rew(s')$ then $s$ has a proof (resp. cut-free
proof) in $R$ iff
$s'$ has a proof (resp. cut-free proof) in $R$.
\end{property}
Property \ref{hyp:compat} implies compatibility in the sense of
Definition 1.4 of \citet{DHK-TPM-JAR}, which is the same except that we
need here a \emph{cut-free} proof in \ref{hyp:compatproof}).
Section \ref{sec:restriction} provides an instance of such a
function $Rew$.
\medskip
With respect to the definitions of ACSs (see Sect.~\ref{section ACSI})
deduction modulo can be seen as an ACS, in the following way:
--- $\P$: \Def{proofs} are sequent calculus
proofs using minimal sets of propositions in their conclusion:
$$\P \df \left\{p\in\mathcal{SQM}\st\neg\left(\exists
q\in\mathcal{SQM}.~\text{Weak}(q,p)\right)\right\}$$
where Weak$(q,p)$ says that \lsv{Lemma
\ref{lemma:weakening} can be applied to $q$ to give $p$}{the proof $p$
can be obtained from $q$ by weakening}.
--- $\A$: \Def{formul\ae} are proposition rewrite
systems corresponding to some sequent: $$\A\df
Rew(\Sequents)~\subseteq~\mathcal{PRS}\enspace.$$
--- The \Def{conclusion} of an ACS proof is the rewrite system
associated by $Rew$ to the conclusion of the
sequent calculus proof: for all proofs $p$,
$$\Cl p\df Rew(\Gamma\seq\Delta)\mbox{ when } p =
\infer{\Gamma\seq\Delta}{\vdots&\vdots}\enspace.$$
--- The \Def{premises} of a proof are the rewrite system consisting in
the proposition rewrite rules appearing in the proof or its subproofs:
for all proofs $p$,
$$
\Ax p\df\left\{\begin{array}{@{}l@{}}\left\{A\rightarrow P\st\begin{array}{l}
\text{ there exists a
}\textrule{$\uparrow$-l}\text{ or }\\\textrule{$\uparrow$-r}
\text{ using }A\rightarrow
P\text{ in }q
\end{array}\right\}\st\\
q\text{ is a subproof of } p
\end{array}
\right\}
$$ This definition implies that we consider only proofs using proposition rewrite
systems corresponding to some sequent.
\subsection{Orderings on Proofs}\label{sec:ordering}
We define the following (infinite, but Noetherian) precedence $>$ :
for all formul\ae\ $P,Q$, if $P$ is greater than $Q$ for the
subformula relation, then $\textrule{Cut}(P)>\textrule{Cut}(Q)$, and
for all other inference rules $\textrule{r}$ of Fig. \ref{fig:seqmod},
$\textrule{Cut}(P)>\textrule{r}$.
We order proofs using the RPO \citep{Dershowitz82} based on this
precedence. Since the precedence is well-founded, so is the RPO
\citep{Dershowitz82}. We restrict this ordering to proofs which have
the same \emph{sequent} as conclusion, modulo weakening.
Because we work modulo weakening and contraction, it is important to
note that a proof and its weakened and contracted versions are
equivalent with respect to the ordering we have just defined, because
they have the same cuts and the same labeled tree structure.
Notice also that with this ordering, a cut-free proof is always strictly
smaller than a proof with at least one cut at root.
\medskip
Subproofs of a proof $p$ are defined as the subproofs of $p$ for the
sequent calculus, modulo weakening and contraction (subproofs may use
less propositions than their parents).
Unfortunately, this definition is not sufficient to define trivial
proofs, because if we use a premise through a \textrule{$\uparrow$-l}
or \textrule{$\uparrow$-r} rule, there will always be a strict
subproof, so that there are no proofs using premises without strict
subproofs.
To solve this problem, we can add manually the trivial proofs,
i.e. $\P$ is in fact $\P\cup\triva{\A}$, where formul\ae\ are identified with
their trivial proof.
%% From a sequent calculus point of view, this is not a problem: the
%% trivial proofs can be simulated by other proofs. Indeed, for
%% $R\in\A=Rew(\Sequents)$, there exists some sequent $\Gamma\seq\Delta$
%% such that $Rew(\Gamma\seq\Delta)=R$. Because of Property
%% \ref{hyp:compat}\ref{hyp:compatproof}) there is a cut-free proof of
%% $\seq\Prop\Gamma\Delta$ in $R$, and therefore, as a
%% consequence of Lemma \ref{lemma:kleene}, a cut-free proof of
%% $\Gamma\seq\Delta$. (Remember that free variables and fresh constants
%% play the same role in a proof.) This proof can simulate $\triva R$ (it has the
%% same premises and conclusion, but it has strict subproofs).
We have to extend the ordering $>$ to trivial proofs: it can be simply done
by saying that
%% trivial proofs will be compared as the minimal proofs
%% that can simulate it:
%% $$\begin{array}{c}
%% p>\triva a\text{ if }p>q\text{ for all }q\in\mu\left\{q\st\Ax q=\{\Cl
%% q\}=\{a\}\right\}\\
%% \triva a>p\text{ if }q>p\text{ for all }q\in\mu\left\{q\st\Ax q=\{\Cl
%% q\}=\{a\} \right\}
%% \end{array}
%% $$
they cannot be compared with other proofs. ($>$ over $\P\cup\triva\A$
is the same relation as $>$ over the original $\P$.)
For Postulate \ref{post:premSubproofs} to be verified, we have to
extend the subproof relation:
$$p\unrhd q~\text{ if \begin{tabular}[t]{@{}l@{}}
-- $q$ is a subproof modulo weakening of $p$
in $\mathcal{SQM}$\\
-- or $q=\triva a$
with $a\in\Ax p$.\end{tabular}}$$
This relation is well-founded because of the wellfoundedness of the
subproof relation in sequent calculus, and because trivial proofs
cannot have strict subproofs.
\medskip
With these definitions we can prove the main theorem of this section:
\begin{theorem}[Instance of ACS]\label{theo:adequacy}
The sequent calculus modulo is an instance of ACS, with the definitions of $\A$, $\P$, $\Ax\cdot$, $\Cl\cdot$,
$>$ and $\rhd$ given above.
\end{theorem}
\begin{Proof}~
\begin{itemize}
\item Postulate \ref{post:refl}: suppose $R\in A$, we want to show that
$R$ is the conclusion of a proof built with $A$. Because
$R\in\A=Rew(\Sequents)$, there exists some sequent $\Gamma\seq\Delta$
such that ${Rew(\Gamma\seq\Delta)}=R$. Using Property
\ref{hyp:compat}\ref{hyp:compatproof}), we know that there is a proof of
$\Prop\Gamma\Delta$ in $R$. As a consequence of
Lemma \ref{lemma:kleene}, we know that there is a proof of
$\Gamma\seq\Delta$ in $R$, i.e. a proof in $A$ proving
$Rew(\Gamma\seq\Delta)=R$. (Remember that free variables can be
treated as fresh constants in the construction of a proof.)
\item Postulate \ref{post:closure}: let $R$ be in $\Th{\Th A}$. By
definition there is a proof $p\in\Pf{\Th A}$ such that $\Cl p =
Rew(\Gamma\seq\Delta) = R$ for some sequent
$\Gamma\seq\Delta$. Let $R'$ be the rewrite system used in $p$,
therefore $R'\in\Ax p\subseteq\Th A$. By definition, there is a
proof $q\in\Pf A$ such that $\Cl q= Rew(\Gamma'\seq\Delta') = R'$
for some sequent $\Gamma'\seq\Delta'$. Using Property
\ref{hyp:compat}, we know that $R'$ is compatible with
$\Prop{\Gamma'}{\Delta'}$. Using Proposition 1.8 of
\citet{DHK-TPM-JAR}, because $p$ is a proof of $\Gamma\seq\Delta$
in $R'$, we know that there exists a proof $r$ of
$\Prop{\Gamma'}{\Delta'},\Gamma\seq\Delta$ in $\emptyset$
(i.e. without rewriting). The proof
$$\Cut{P'}{\Gamma\seq\Delta} {\infer*{\Gamma, P'\seq\Delta}{r}}
{\infer=[\textrule{Logical rules}]{\Gamma\seq P',\Delta}
{\infer*{\Gamma,\sigma\Gamma'\seq\sigma\Delta',\Delta}{q}}}$$
where $P'$ means $\Prop{\Gamma'}{\Delta'}$ and $\sigma$ is a
substitution replacing the free variables of $\Gamma',\Delta'$ by
fresh constants, is a proof of $Rew(\Gamma\seq\Delta) = R$ in $\Pf
A$, because it uses the same rewrite system as $q$ which is in
$\Pf A$. ($q$ is indeed a proof of
$\sigma\Gamma'\seq\sigma\Delta'$, because free variables can be
considered as fresh constants.) Therefore ${R\in\Th A}$.
\item Postulate \ref{post:premSubproofs}: it holds by definition of the
subproof relation $\unrhd$.
\item Postulate \ref{post:premMono}: suppose $p\unrhd q$. If $q$ is
a subproof of $p$ in the sequent calculus modulo, then by definition
of $\Ax\cdot$ and by transitivity of the subproof relation, $\Ax
p\supseteq\Ax q$. If $q=\triva a$ with $a\in\Ax p$, $\Ax
q=\{a\}\subseteq\Ax p$.
\item Postulate \ref{post:replacement}: suppose $p\rhd q>r$. Because
$q$ is comparable with $r$, both of them are sequent calculus
proofs, and not trivial proofs. As $q$ is a subproof of $p$ in
the sequent calculus modulo, we can replace $q$ by $r$ in $p$ to
obtain some proof $v$, because $q>r$ implies that they have the
same sequent as conclusion, modulo weakening. Because an RPO is
reduction ordering, $p>v$.
\end{itemize}
\end{Proof}
%% \begin{Proof}
%% A more detailed proof can be found in Appendix \ref{sec:adequacy}.
%% Postulate \ref{post:refl} comes from Property
%% \ref{hyp:compat}\ref{hyp:compatproof}). Postulate \ref{post:closure}
%% from Property \ref{hyp:compat} and Proposition 1.8 of
%% \cite{DHK-TPM-JAR}. Postulate \ref{post:premSubproofs} is a consequence
%% of the definition of $\rhd$. Postulate \ref{post:premMono} comes from
%% the definition of $\Ax\cdot$. Postulate \ref{post:replacement} holds
%% because an RPO is a reduction ordering.
%% \end{Proof}
\section{A Generalized Completion Procedure}\label{A Generalized Completion Procedure}
We want to define a completion procedure
through critical proofs. For this, we first need some characterizations of the normal-form
proofs and the critical proofs. The limit of this completion procedure
will be an equivalent rewrite
system modulo whom the sequent calculus admits \RCut.
\subsection{Normal-form Proofs and Critical Proofs in Deduction Modulo}
\begin{proposition}[Characterization of Normal-Form Proofs]
\label{prop:nfproofs}
A proof in deduction modulo is in normal form iff it is either a
trivial proof or a cut-free proof with no useless logical rules.
\end{proposition}
\begin{Proof}
If a proof $p$ in $\Pf{A}$ is not a trivial proof, and possesses a cut at position
$\mathfrak p$, then using Property \ref{hyp:compat}(\ref{hyp:compatproof}), we know
that there exists a
cut-free proof of the sequent $\seq\Prop\Gamma\Delta$ where
$\Gamma\seq\Delta$ is the conclusion of $\subterm p{\mathfrak p}$. Using Lemma \ref{lemma:kleene} we obtain a
cut-free proof $q$ of $\Gamma\seq\Delta$. Replacing $\subterm
p{\mathfrak p}$ by $q$ in $p$ using Postulate \ref{post:replacement},
we obtain a smaller proof than $p$ which is in $\Pf{Th A}$ because $q$
is by assumption in $Rew(Gamma\seq\Delta)=\Cl{\subterm p{\mathfrak
p}}$. Therefore $p$ cannot be in normal-form.
If a proof $p$ is not a trivial proof, is cut-free, and has a useless
logical rule at position $\mathfrak p$, then the direct subproofs of
$\subterm p{\mathfrak p}$ shows the same conclusion as $\subterm
p{\mathfrak p}$ (because we work modulo weakening, and because the
propositions resulting from the logical rule are not needed), and are
smaller because an RPO is a simplification ordering. By using Postulate
\ref{post:replacement} we can obtain a proof smaller than $p$, and
therefore $p$ cannot be in normal-form.
Due to our definition of the precedence of the RPO, if a non-trivial proof $p$ is not
minimal in every presentation of a theory, i.e. there exists a smaller
proof $q$, then either $p$ contains a $\textrule{Cut}$ or $q$ is a
subproof of $p$, i.e. useless rules were applied in $p$.
A trivial proof in $\Pf{A}$ is not comparable with any other proof, in
particular in $\Pf{\Th A}$, so that it is in normal form.
\end{Proof}
%% It is important to remark that trivial proofs can be simulated by
%% \emph{cut-free} proofs, so that all normal-form proofs can be
%% considered as cut-free, and the canonical presentation does have
%% the cut-elimination property.
We give now a characterization of the critical proofs in deduction
modulo.
\begin{proposition}[Critical Proofs in Deduction Modulo]\label{prop:critproofs}
Critical proofs in deduction modulo are of the form
$$\Cut{A}{\Gamma\seq\Delta}{\Upl{\Gamma,A\seq\Delta}{\infer*{\Gamma,A,P\seq\Delta}{\pi}}}{\Upr{\Gamma\seq A,\Delta}{\infer*{\Gamma\seq
Q,A,\Delta}{\pi'}}}$$
where $\pi$ and $\pi'$ are cut-free and do not use unneeded logical
rules, and at least one of $A\rightarrow P$ or $A\rightarrow Q$ is not
a \emph{term} rewriting.
\end{proposition}
\end{multicols}
\begin{Proof}
We essentially follow the proof of the Hauptsatz of \citet[Chapter
13]{GirardLafontTaylor89}.
%% We want to show that if a proof doesn't have the above form, then it
%% is:
%% \begin{enumerate}
%% \item\label{enu:nf}
%% either in normal form,
%% \item\label{enu:sbnf}or one of its subproofs isn't in normal form,
%% \item\label{enu:mp}or it is not minimal for the presentation
%% considered
%% \end{enumerate}
%% (converse of the
%% definition of a critical proof).
Because of Proposition \ref{prop:nfproofs}, subproofs of a critical
proof (which are by definition in normal form) that are not trivial
must be cut-free. Furthermore, because a critical proof is not in
normal form, then it possesses either a cut, or a unneeded logical
rule. In the second case, we can find a smaller proof in the same
presentation, contradicting the minimality of critical proofs.
Therefore a cut-free proof has a cut at its root. It is a proof of the
form
$$\Cut{P}{\Gamma\seq\Delta}{\pi\left\{
\begin{array}{c}
\pi_1 ~~~\cdots~~~\pi_n\\\hline
\Gamma,P\seq\Delta
\end{array}
\right.\textrule{r}}{~~~~&\left.
\begin{array}{c}
\pi'_1 ~~~\cdots~~~\pi'_m\\\hline
\Gamma\seq P,\Delta
\end{array}\textrule{r'}\right\}\pi'}$$
where $\pi$ and $\pi'$ are cut-free without useless rules.
In the following, $\varpi,\varpi',\vect\varpi,\vect[m]{\varpi'}$ are
proof obtained from $\pi,\pi',\vect\pi,\vect[m]{\pi'}$ by \lsv{the Weakening Lemma
\ref{lemma:weakening}}{weakening}.
We can now check the different cases that can be found in Section
13.2 of \citet{GirardLafontTaylor89} (note that we do not have to
consider structural rules in our sequent calculus):
\begin{enumerate}
\item\label{enu:axiom} \textrule{r} is \textrule{Axiom}. There are two cases :
\begin{itemize}
\item the principal proposition of the \textrule{Axiom} is
$P$, then we have necessarily $P\in\Delta$ and $\pi'$ is therefore a
proof of $ \Gamma\seq\Delta$ which is smaller than the initial
proof, contradicting its minimality;
\item the principal proposition of the \textrule{Axiom} is another
proposition $Q$, then $Q\in\Gamma$ and $Q\in\Delta$, so that we can
build the proof $\Axiomm{\Gamma\seq\Delta}$ which is smaller than
the initial proof, contradicting its minimality.
\end{itemize}
\item \textrule{r'} is \textrule{Axiom}. This case is handled as case
\ref{enu:axiom}.
\item\label{enu:logical} \textrule{r} is a logical rule other than a
left one with principal formula $P$. In this case, the conclusion of
a subproof $\pi_i$ has the form $\Gamma_i, P\seq\Delta_i$, because
\textrule{r} does not touch $P$. The proof
$$\infer[\textrule{r}]{\Gamma,\Gamma\seq\Delta,\Delta}{
\Cut{P}{\Gamma,\Gamma_1\seq\Delta,\Delta_1}
{\infer*{\Gamma,\Gamma_1,P\seq\Delta,\Delta_1}{\varpi_1}}
{\infer*{\Gamma,\Gamma_1\seq P,\Delta,\Delta_1}{\varpi'}}
&
\Cut{P}{\Gamma,\Gamma_n\seq\Delta,\Delta_n}
{\infer*{\Gamma,\Gamma_n,P\seq\Delta,\Delta_n}{\varpi_n}}
{\infer*{\Gamma,\Gamma_n\seq P,\Delta,\Delta_n}{\varpi'}}}
$$
is smaller than the initial proof,
contradicting its minimality.
\item \textrule{r'} is a logical rule other than a right one with
principal formula $P$. This case is handled as case
\ref{enu:logical}.
\item Both \textrule{r} and \textrule{r'} are logical rules,
\textrule{r} a left one and \textrule{r'} a right one, of principal
proposition $P$. This is one of the key cases as given in Section
13.1 of~\citet{GirardLafontTaylor89} : by replacing the cut over $P$
by cuts over subformul\ae\ of $P$ we obtain a smaller proof, thus
contradicting the minimality of the original proof. For instance, if
$P = P_1\wedge P_2$, the initial proof $$\Cut{P_1\wedge
P_2}{\Gamma\seq\Delta} {\Andl{\Gamma,P_1\wedge
P_2\seq\Delta}{\infer*{\Gamma,P_1,P_2\seq\Delta}{\pi_1}}}
{\Andr{\Gamma\seq P_1\wedge
P_2,\Delta}{\infer*{\Gamma\seq
P_1,\Delta}{\pi'_1}}{\infer*{\Gamma\seq P_2,\Delta}{\pi'_2}}}$$ is
greater than the proof
$$\Cut{P_1}{\Gamma\seq\Delta}{\Cut{P_2}
{\Gamma,P_1\seq\Delta}{\infer*{\Gamma,P_1,P_2\seq\Delta}{\pi_1}}
{\infer*{\Gamma,P_1\seq P_2,\Delta}{\varpi'_2}}}{\infer*{\Gamma\seq
P_1,\Delta}{\pi'_1}}$$
\item\label{enu:rewrite} \textrule{r} or \textrule{r'} is a rewrite rule applying to
another proposition than $P$. This case can in fact be
handled as case \ref{enu:logical}.
%% The initial proof is for
%% instance of the form
%% $$\Cut{P}{\Gamma,A\seq\Delta}
%% {\Upl{\Gamma,A,P\seq\Delta}{\infer*{\Gamma,A,Q,P\seq\Delta}{\pi_1}}}
%% {\infer*{\Gamma,A\seq P,\Delta}{\pi'}}\enspace.$$ It is greater than the
%% following one :
%% $$\Upl{\Gamma,A\seq\Delta}{\Cut{P}{\Gamma,A,Q\seq\Delta}
%% {\infer*{\Gamma,A,Q,P\seq\Delta}{\pi_1}} {\infer*{\Gamma,A,Q\seq
%% P,\Delta}{\varpi'}}}\enspace.$$ This
%% contradicts the minimality of the first proof.
%% \item \textrule{r'} is a rewrite rule applying to another proposition
%% than $P$. This case is handled as case
%% \ref{enu:logical}.
\item\label{enu:conflict} \textrule{r} is a rewrite rule and \textrule{r'}
is a logical rule, both applying to $P$. This case cannot occur,
because if we rewrite $P$, it implies that $P$ is atomic so that no
logical rule can be applied to it.
\item \textrule{r} is a logical rule and \textrule{r'}
is a rewrite rule, both applying to $P$. This case is handled as
case \ref{enu:conflict}.
\item\label{enu:bothrewrite} \textrule{r} and \textrule{r'} are both
rewrite rules applying to $P$. Therefore $P$ has to be atomic, and
is rewritten by $P\rightarrow P_1$ to the left and $P\rightarrow
P_2$ to the right. If both of this rewriting are term rewriting,
then, because of confluence of $\Rterms$, we know that there is some
$P'$ such that
$P_1\mathop{\longrightarrow}\limits_{\Rterms}^*P'\mathop{\longleftarrow}\limits_{\Rterms}^*P_2$.
The proof $$\Cut{P_1}{\Gamma\seq\Delta}{\infer*{\Gamma,P_1\seq\Delta}{\pi_1}}
{\Cut{P_2}{\Gamma\seq P_1,\Delta}
{\infer=[\textrule{Rewrite Rules}]{\Gamma,P_2\seq
P_1,\Delta}{\Axiomm{\Gamma,P'\seq P',\Delta}}}
{\infer*{\Gamma\seq P_1,P_2,\Delta}{\varpi_1'}}}
$$ is smaller than
the initial proof (remind that the term rewrite relation is by
definition included in the subformula relation), contradicting its
minimality. Otherwise, we are exactly in the case stated in the
theorem.
\end{enumerate}
\end{Proof}
%% \begin{Proof}
%% We give here a sketch of proof. The detailed proof is given in
%% Appendix \ref{sec:appendix}.
%% Because of Proposition \ref{prop:nfproofs}, one can show that a
%% critical proof has the form
%% \parbox{\textwidth}{\centering $\Cut{P}{\Gamma\seq\Delta}
%% {\infer[\textrule{r}]{\Gamma,P\seq\Delta}{ \pi_1&\cdots&\pi_n}}
%% {\infer[\textrule{r'}]{\Gamma\seq P,\Delta}{ \pi'_1&\cdots&\pi'_m}}
%% \enspace.$}
%% We can now check the different cases that can be found in Section
%% 13.2 of \cite{GirardLafontTaylor89}: for each of them, a smaller proof
%% can be found, contradicting the minimality of critical proofs. Having
%% the possibility to use rewrite
%% rules adds new cases, but the only one where one cannot find a smaller
%% proof is the case stated in the proposition.
%% \end{Proof}
\begin{multicols}{2}
\begin{note}
If we suppose, as in the order condition of \citet{hermant}, that the
proposition rewrite system is confluent, and that it is included in
an well-founded ordering compatible with the subformula relation,
then we can take this ordering instead of the subformula relation to
compare cuts in the precedence. Doing this, we can prove that there
are no minimal proofs of this form, and consequently \emph{no
critical proofs}. Therefore the admissibility of \RCut\ is
verified.
The main difference with \citet{hermant} is that he gives a
semantic proof of the admissibility of \RCut, whereas we have here
a cut elimination algorithm, i.e. a terminating syntactical process
that transforms a proof into a cut-free one. It remains to be
investigated how this process is related with normalization,
i.e. $\beta$-reduction. (The last case corresponds in fact to an
$\eta$-expansion.) It is proved by \citet{normalization} that such an
order condition provides normalization in the quantifier-free case.
This result was also independently found by \citet{aiguier}, with
the same kind of ordering over proofs.
\end{note}
\begin{theorem}[Undecidability of Critical Proof Search]
The problem
\begin{quote}
Input: A propositional rewrite system $R$ and a sequent $\Gamma\seq\Delta$.
Decide if $\Gamma\seq\Delta$ is the conclusion of a critical proof
in $R$.
\end{quote}
is undecidable.
\end{theorem}
\begin{proof}
We reduce to the problem of validity in first order logic.
Let $P$ be a first order formula.
Let $A,B$ be atomic formul\ae\ not appearing in $P$. Consider the
following propositional rewrite system:
$$\left\{\begin{array}{l}
A\ra A\wedge B\\
A\ra A\vee P
\end{array}\right.\enspace.$$
We can check that $\seq B$ is the conclusion of a critical proof in it
if and only if $P$ is valid.
Indeed, a critical proof is necessarily of the form
$$\Cut{A}{\seq B}{\Upl{A\seq B}{\Andl{A,A\wedge B\seq B}{\Axiomm{A,B\seq
B}}}}
{\Upr{\seq A, B}{\Orr{\seq A\vee P, A, B}{\infer*{\seq
P,A,B}{\text{Proof of $P$ in $\emptyset$}}}}}$$
\end{proof}
Of course, in the quantifier-free case, this problem is decidable. It
remains to be investigated for what fragments of first-order logic it
is decidable, in particular if these fragments are the same that for
the validity problem.
\subsection{The Completion Procedure}
As we wrote in Sect.~\ref{section ACSI}, we want to define a
completing completion procedure by adding to a presentation $A$ a
presentation $\textsf C(A)$ such that $\Comp A\subseteq\textsf
C(A)\subseteq\Th A$.
Here, using Property \ref{hyp:compat}(\ref{hyp:compatproof}), we know
that for all proofs $p$ of a sequent $\Gamma\seq\Delta$ there exists a
cut-free proof of the sequent $\seq\Prop\Gamma\Delta$ in
$Rew(\Gamma\seq\Delta)$. Using Lemma \ref{lemma:kleene} we obtain a
cut-free proof $p'$ of $\Gamma\seq\Delta$ in
$Rew(\Gamma\seq\Delta)$. If the proof $p$ is critical, it has a cut at
its root and thus it is than $p'$, so that we can use this particular
$p'$ in the defintion $\Comp$. We therefore have to add the premises
of $q$, but these premises are in fact in $Rew(\Gamma\seq\Delta)=\Cl
p$:
$$\Comp A\df\{\Cl p\st p\in\Crit A\}\enspace.$$
The best procedure is thus to add only the
conclusions of critical proofs. Nevertheless, searching for these
proofs is undecidable, so that we must use a superset of them. Here we
will add the conclusion of the proofs in the form of Proposition
\ref{prop:critproofs} (note that it is only a necessary condition for
being critical), except the one that we know for sure that they
are not minimal (for instance if $A\in\Gamma\cup\Delta$).
We must consider proofs of the form of
Proposition \ref{prop:critproofs}. As $\pi$ and $\pi'$ are cut-free and
do not use unneeded logical rules, they could be found using for
instance a tableaux method modulo, like TaMeD \citep{Bonichon04}, which
is complete with respect to cut-free proofs, if we knew $\Gamma$ and
$\Delta$, hence the idea to apply the tableaux method to $A,P\seq$ and
$\seq Q,A$, and to complete $\Gamma$ and $\Delta$ in order to close the
remaining tableaux. Because we work modulo weakening, we can restrict
ourselves to the minimal $\Gamma$ and $\Delta$ closing the tableaux.
We can then sort the obtained $\Gamma\seq\Delta$ to remove sequents
where $A\in\Gamma\cup\Delta$. The resulting rewrite system is
obtained by adding all $Rew(\Gamma\seq\Delta)$ to our rewrite system.
\begin{theorem}[Cut Admissibility of the Limit]\label{theo:cutlim}
For all sequents $\Gamma\seq\Delta$, for all proposition rewrite
systems $R_0$, $\Gamma\seq\Delta$ has a proof in $R_0$ if and only
if it has a \emph{cut-free} proof in $R_\infty$.
\end{theorem}
\begin{Proof}
By Proposition \ref{prop:satcpc}, we know that $R_\infty$ is
complete, and therefore by Lemma \ref{lemma:limit_canon}
\begin{equation}\label{eq:satcpc}
\Th{R_0}\subseteq \Cl{\Pf{R_\infty}\cap\Nf{R_0}}\enspace.\end{equation}
The ``if'' part comes from the fact that our
completion is sound. For the ``only if'', suppose that
$\Gamma\seq\Delta$ has a proof in $R_0$, then using
(\ref{eq:satcpc}) it has a proof $p$ in $\Pf{R_\infty}\cap\Nf{R_0}$.
If $p$ is a trivial
proof, then we can use \ref{hyp:compat}(\ref{hyp:compatproof}) to
find a cut-free proof with the same conclusion, otherwise
Proposition \ref{prop:nfproofs} shows that $p$ is cut-free. The
conclusion of the cut-free proof is not necessarily ${\Gamma\seq\Delta}$ but
a sequent $\Gamma'\seq\Delta'$ such that
${Rew(\Gamma\seq\Delta)}={Rew(\Gamma'\seq\Delta')}$, so we can
conclude with Property \ref{hyp:samecf}.
\end{Proof}
\section{Sequents and Rewrite Systems}\label{sec:restriction}
For deduction modulo to be an instance of ACS, we have to define
some function $Rew$ having Properties \ref{hyp:compat} and
\ref{hyp:samecf}. We also want to know how to build proofs that use
the rewrite system associated with some sequent, and therefore this
function has to be effective.
\subsection{An Algorithm \ldots}\label{sec:algo}
If we consider only propositional logic (i.e. without quantifier), we
can use the following (non-deterministic) algorithm to transform a set
of sequents $\Gamma\seq\Delta$ into a set of rewrite rules:
\end{multicols}
\begin{enumerate}[Step 1.]
\item\label{it:step1} Choose a sequent. Push all negated
formul\ae\ on the other side of the sequent. For instance, $A,\neg
B\seq\neg C, D$ becomes $A,C\seq B, D$. If the new $\Gamma$ is
empty, go to step \ref{it:step2}. If the new $\Delta$ is empty, go
to step \ref{it:step3}. If neither are empty, go to either Step
\ref{it:step2} or Step \ref{it:step3}.
\item\label{it:step2}
Decompose the last proposition iteratively:\\
\begin{tabular}{c@{~~~~''~~~~}c}
\multicolumn{1}{c@{~becomes~}}{$\vect P\seq\vect[m]Q$} & $\vect P,\vect[m-1]{\neg Q}\seq
Q_m$
\\ $\vect P\seq Q_1\wedge Q_2$ & $\vect P\seq Q_1~;~\vect
P\seq Q_2$
\\ $\vect P\seq Q_1\vee Q_2$ & $\vect P,\neg Q_1\seq Q_2$
\\ $\vect P\seq Q_1\imp Q_2$ & $\vect P, Q_1\seq Q_2$
\\ $\vect P\seq A$ & $A\ra
A\vee \exists\vect[p]x.~(P_1\wedge\cdots\wedge P_n)$
\end{tabular}\\
($A$ atomic, and the $x_i$
are the free variables appearing in $\vect P$ but not in $A$)\\
for $\vect P\seq\neg Q$, return to Step \ref{it:step1}
\item\label{it:step3}
Decompose the first proposition iteratively, dually from step
\ref{it:step2}. For instance,
\begin{tabular}{c@{~~~~''~~~~}c}
\multicolumn{1}{c@{~becomes~}}
{$P_1\imp P_2\seq\vect[m]Q$} &
$P_2\seq\vect[m]Q~;~\neg P_1\seq\vect[m]Q$
\\ $A\seq \vect[m]Q$ & $A\ra
A\wedge \forall\vect[p]x.~(Q_1\vee\cdots\vee Q_m)$
\end{tabular}\\
($A$ atomic, and the $x_i$
are the free variables appearing in $\vect[m]Q$ but not in $A$)\\
for $\neg P\seq\vect[m]Q$, return to Step \ref{it:step1}.
\end{enumerate}
\begin{multicols}{2}
This algorithm clearly terminates, because each times a step
\ref{it:step2} or \ref{it:step3} begins, either the rewrite rule is
generated, or a formula is decomposed into subformul\ae, so that the
number of connectors different from $\neg$ strictly diminishes. Of
course, we do not pretend that this algorithm is the most optimized
for our purpose.
$Rew(\Gamma\seq\Delta)$ will be the function returning the rewrite
system obtained by applying the algorithm to $\bigl\{\Gamma\seq\Delta\bigr\}$.
This algorithm can be extended to the case with quantifiers. In the
case of a $\forall$ on the left of the sequent, or a $\exists$ on the
right, we will keep the formula in the sequent, but will not decompose
it further. We will therefore denote by $\underline P$ the fact that
$P$ was already decomposed. Then we do not consider underlined formula
in Step \ref{it:step1} to choose between Step \ref{it:step2} or Step
\ref{it:step3}, and at the beginning of Step \ref{it:step2}
(resp. Step \ref{it:step3}),
one keep a non-underlined formula to the right (resp. left)
side.
\noindent We also have to add the following decomposition steps:
\end{multicols}
\begin{itemize}
\item (\ref{it:step2}) $\vect P\seq\forall x.~Q$ becomes
${\vect P\seq\subst Qyx}$ where $y$ does not appear in $\vect P$;
\item (\ref{it:step2}) $\vect P\seq\exists x.~Q$ becomes
${\vect P,\neg\underline{\exists x.~Q}\seq\subst Qtx}$ where $t$ can be
any ground term;
\item (\ref{it:step3}) $\exists x.~P\seq\vect[m]Q$ becomes
${\subst Pyx\seq\vect[m]Q}$ where $y$ does not appear in $\vect[m]Q$;
\item (\ref{it:step3}) $\forall x.~P\seq \vect[m] Q$ becomes
${\subst Ptx\seq\neg\underline{\forall x.~P},\vect[m]Q}$ where $t$
can be any ground term.
\end{itemize}
\begin{multicols}{2}
Of course, at the end, the underlines are removed.
This algorithm does not allow all rewrite systems to be considered as
formul\ae. Nevertheless, one can transform all rewrite systems to
equivalent rewrite systems that are images of sequents by $Rew$, by
splitting the rules: $A\rightarrow P$ becomes $A\rightarrow A\vee P$
and $A\rightarrow A\wedge P$. This is equivalent to the polarized
rewrite systems of \citet{dowek:theory}.
This algorithm can be seen as the attempt to build a cut-free proof of the
conclusion of a critical proof, adding rewrite rules to close the branches
were an atomic formula appears.
\end{multicols}
\subsection{\ldots with the Good Properties}\label{sec:prop}
We first prove Property \ref{hyp:compat} using three lemmata.
\begin{lemma}\label{lemma:1gen}
If the sequent $\Gamma\seq\Delta$ is transformed to the set of
sequents ${\{\Gamma'\seq\Delta'\}}\cup S'$ by the algorithm described
in Sect.~\ref{sec:restriction}, %% and $\vect x$ (resp. $\vect[m]y$)
%% are the free variables of $\Gamma,\Delta$ (resp.$\Gamma',\Delta'$)
then the sequent
$$\Prop\Gamma\Delta\seq\Prop{\Gamma'}{\Delta'}$$
can be proved (without rewrite rules).
\end{lemma}
\begin{Proof}
By case analysis on the transformation. For instance, in Step
\ref{it:step2}, $\vect P\seq Q_1\wedge Q_2$ is transformed into
$\vect P\seq Q_1; \vect P\seq Q_2$. Suppose $\vect x$ (resp. $\vect[m]y$)
are the free variables of $\vect P,Q_1\wedge Q_2$ (resp.$\vect P,Q_1$).
$\{\vect[m]y\}\subseteq\{\vect x\}$ so that we can suppose $y_i=x_i$
for $i\in\vectset[m]$. We have the following proof
(only relevant propositions are written, and the substitutions are
forgotten in the above part of the proof):
$$\infer=[\textrule{$\forall$-r}]{\forall\vect
x.~(\bigwedge_iP_i\imp(Q_1\wedge
Q_2))\seq\forall\vect[m]y.~(\bigwedge_iP_i\imp Q_1)}
{\infer=[\textrule{$\forall$-l}]{\forall\vect
x.~(\bigwedge_iP_i\imp(Q_1\wedge
Q_2))\seq\subst{(\bigwedge_iP_i\imp Q_1)}{c_i}{y_i}}{
\Impr{\subst{\bigwedge_iP_i\imp(Q_1\wedge Q_2)}{c_i}{x_i}\seq
\subst{\bigwedge_iP_i\imp
Q_1}{c_i}{y_i}}{\Impl{\bigwedge_iP_i\imp(Q_1\wedge Q_2),
\bigwedge_iP_i\seq Q_1}{\Andl{Q_1\wedge Q_2\seq
Q_1}{\Axiomm{Q_1, Q_2\seq
Q_1}}}{\Axiomm{\bigwedge_iP_i\seq \bigwedge_iP_i}}}}}$$
where $c_i$ are fresh constants.
\end{Proof}
\begin{lemma}\label{lemma:1af}
For all propositions $A,\vect P$, if $\vect[p]x$ the free
variables of $\vect P$ not appearing freely in $A$, then the
sequents $$\Prop{\vect P}A\seq A\Leftrightarrow
A\vee\exists\vect[p]x.~\bigwedge_iP_i$$
$$\Prop A{\vect P}\seq A\Leftrightarrow
A\wedge\forall\vect[p]x.~\bigvee_iP_i$$ can be proved (without
rewrite rules).
\end{lemma}
\begin{Proof} Suppose $\vect[m]y$ are the free
variables of $A,\vect P$. Note that $\{\vect[p]x\}\subseteq\{\vect[m]y\}$ so that we can suppose $y_i=x_i$
for $i\in\vectset[p]$. We can construct the following proofs (only
relevant propositions are written):
\begin{equation}\label{eq:lemp1}
\Impr{\forall\vect[m]y.~(\bigwedge_iP_i\imp A)\seq A\imp
A\vee\exists\vect[p]x.~\bigwedge_iP_i}{\Orr{\forall\vect[m]y.~(\bigwedge_iP_i\imp A), A\seq
A\vee\exists\vect[p]x.~\bigwedge_iP_i}{\Axiomm{\forall\vect[m]y.~(\bigwedge_iP_i\imp A), A\seq
A,\exists\vect[p]x.~\bigwedge_iP_i}}}
\end{equation}
\begin{equation}\label{eq:lemp2}
\Impr{\forall\vect[m]y.~(\bigwedge_iP_i\imp A)\seq
A\vee\exists\vect[p]x.~\bigwedge_iP_i\imp A}
{\Orl{\forall\vect[m]y.~(\bigwedge_iP_i\imp A),
A\vee\exists\vect[p]x.~\bigwedge_iP_i\seq A}{\Axiomm{A\seq A}}{%
\infer=[\textrule{$\exists$-l}]{\forall\vect[m]y.~(\bigwedge_iP_i\imp
A),\exists\vect[p]x.~\bigwedge_iP_i\seq A}
{\infer=[\textrule{$\forall$-l}]{\forall\vect[m]y.~(\bigwedge_iP_i\imp
A),\sigma\bigwedge_iP_i\seq A}
{\Impl{\sigma(\bigwedge_iP_i\imp
A),\sigma\bigwedge_iP_i\seq
A}{\Axiomm{A\seq A}}{\Axiomm{\sigma\bigwedge_iP_i\seq\sigma\bigwedge_iP_i}}}}}}
\end{equation}
$$\Andr{\forall\vect[m]y.~(\bigwedge_iP_i\imp A)\seq A\Leftrightarrow
A\vee\exists\vect[p]x.~\bigwedge_iP_i}
{\infer*{}{\textrm{(\ref{eq:lemp1})}}&~~~~~~~~~~~~~~~~~~~~~~~~~~~~}
{\infer*{}{\textrm{(\ref{eq:lemp2})}}}$$
where $\sigma$ is the substitution replacing $x_i$ by a fresh constant
$c_i$ for $i\in\vectset[p]$, leaving all other variables unchanged.
The proof of the other sequent is dual.
\end{Proof}
\begin{lemma}\label{lemma:1bf}
For all atomic propositions $A$ and propositions $\vect P$, if
$\vect[p]x$ the free variables of $\vect P$ not appearing freely in
$A$, then we can prove the sequent $$\seq\Prop{\vect P}A$$ in the
rewrite system consisting of the rule $A\ra A\vee
\exists\vect[p]x.~(P_1\wedge\cdots\wedge P_n)$, and the
sequent $$\seq\Prop A{\vect P}$$ in the rewrite system consisting of
the rule $A\ra A\wedge \exists\vect[p]x.~(P_1\vee\cdots\vee P_n)$.
\end{lemma}
\begin{proof}
Suppose $\vect[m]y$ are the free variables of $A,\vect P$. Note that
$\{\vect[p]x\}\subseteq\{\vect[m]y\}$ so that we can suppose
$y_i=x_i$ for $i\in\vectset[p]$. Because $\vect[p]x$ do not appear
in $A$, $\subst A{t_i}{y_i}={\subst A{t_i}{y_i:i>p}}$. Only
relevant propositions are written:
$$\infer=[\textrule{$\forall$-r}]{\seq\forall\vect[m]y.~(\bigwedge_iP_i\imp
A)}
{\Impr{\seq\subst{\bigwedge_iP_i\imp
A}{c_i}{y_i}}{\Upr{\subst{\bigwedge_iP_i}{c_i}{y_i}\seq\subst
A{c_i}{y_i:i>p}}{\Orr{\subst{\bigwedge_iP_i}{c_i}{y_i}\seq\subst{(A\vee
\exists\vect[p]x.~(P_1\wedge\cdots\wedge
P_n))}{c_i}{y_i:i> p}}{\infer=[\textrule{$\exists$-r}]
{\subst{\bigwedge_iP_i}{c_i}{y_i}\seq\subst A{c_i}{y_i},\subst
{\exists\vect[p]x.~(P_1\wedge\cdots\wedge
P_n)}{c_i}{y_i:i>p}}
{\infer=[\textrule{$\wedge$-l}]{\subst{\bigwedge_iP_i}{c_i}{y_i}\seq\subst A{c_i}{y_i},\subst
{(\subst{P_1\wedge\cdots\wedge
P_n}{c_i}{x_i})}{c_i}{y_i:i>p}}
{\infer=[\textrule{$\wedge$-r}]{\subst{P_1}{c_i}{y_i},\ldots,\subst{P_n}{c_i}{y_i},\seq\subst
A{c_i}{y_i},\subst{P_1\wedge\cdots\wedge
P_n}{c_i}{y_i}}{\Axiomm{\subst{P_1}{c_i}{y_i}\seq\subst{P_1}{c_i}{y_i}}
&\cdots & \Axiomm{\subst{P_n}{c_i}{y_i}\seq\subst{P_n}{c_i}{y_i}}}}}}}}}$$
\end{proof}
\begin{multicols}{2}
We can prove Property \ref{hyp:samecf} using the following lemma:
\begin{lemma}\label{lemma:2gen} For all proposition rewrite system $R$, if the set of sequents $S$ is transformed into the set of sequents
$S'$ by the algorithm of Sect.~\ref{sec:restriction}, then all
sequents of $S$ have a (resp. cut-free) proof in $R$ iff all
sequents of $S'$ have a (resp. cut-free)
proof in $R$.
\end{lemma}
\begin{Proof}
By case analysis on the transformation. The ``if'' part is the
application of logical rules, whereas the ``only if'' part is a
consequence of Lemma \ref{lemma:kleene}.
For instance, $\vect P\seq\forall x.~Q$ is transformed into $\vect
P\seq\subst Qyx$ where $y$ does not appear in $\vect P$. If $\vect
P\seq\subst Qyx$ has a proof in $R$, then because $y$ does not appear in
$\vect P$, $\vect P\seq\subst Qcx$ has a proof in $R$ for any fresh
constant $c$, so that $\vect P\seq\forall x.~Q$ has a proof in $R$ by
application of \textrule{$\forall$-r}. Conversely, if $\vect
P\seq\forall x.~Q$ has a proof in $R$, then by Lemma
\ref{lemma:kleene} there exists a proof of $\vect P\seq\subst Qcx$ in
$R$ for a fresh constant $c$. As $c$ is fresh, it can be replaced by a
variable $y$ which does not appear in $\vect P$, so that $\vect
P\seq\subst Qyx$ has a proof in $R$.
In the preceding paragraph, if proofs are supposed cut-free, then the
resulting proofs have the same property.
\end{Proof}
\end{multicols}
We can now prove the main result of this subsection:
\begin{proposition}
The $Rew$ function defined in Sect.~\ref{sec:algo} has the
Properties \ref{hyp:compat} and \ref{hyp:samecf}.
\end{proposition}
\begin{Proof}
We proceed by induction on the execution of the algorithm of
Sect.~\ref{sec:restriction}
For Property \ref{hyp:compat}\ref{hyp:compattheory}), one can restrict
oneself to one step rewrite for
$P\mathop{\longleftrightarrow}\limits_R^*Q$. Lemma \ref{lemma:1af}
permits to prove the property at the end of the algorithm, when
sequents are transformed into rules. Lemma \ref{lemma:1gen} permits to
prove the inductive case: suppose $\Gamma\seq\Delta$ is transformed
into $\{\Gamma'\seq\Delta'\}\cup\cdots$. Suppose $\Prop{\Gamma'}{\Delta'}\seq
A\Leftrightarrow P$ has a proof $p$ without rewrite rules. By Lemma
\ref{lemma:1gen}, there is a proof $q$ of $\Prop\Gamma\Delta\seq \Prop{\Gamma'}{\Delta'}$. Therefore, we
can construct the proof $$\Cut{\Prop{\Gamma'}{\Delta'}}{\Prop\Gamma\Delta\seq A\Leftrightarrow
P}{\infer*{\Prop\Gamma\Delta, \Prop{\Gamma'}{\Delta'}\seq A\Leftrightarrow P}{p}}{\infer*{\Prop\Gamma\Delta\seq
\Prop{\Gamma'}{\Delta'},A\Leftrightarrow P}{q}}$$ without rewrite rules.
For Property \ref{hyp:compat}\ref{hyp:compatproof}), the base case a
consequence of Lemma \ref{lemma:1bf}, whereas the inductive case is a
consequence of Lemma \ref{lemma:kleene}. For instance, suppose $\vect
P\seq Q_1\wedge Q_2$ is transformed into $\vect P\seq Q_1; \vect P\seq
Q_2$. For $i\in\{1,2\}$, suppose $\seq \Prop{\vect P}{Q_i}$ has a
cut-free proof in some rewrite system $R_i$. By Lemma
\ref{lemma:kleene}, there is a cut-free proof $p_i$ of $\vect{\sigma
P}\seq \sigma Q_i$ in $R_i$, where $\sigma$ is a substitution
replacing the free variables of $\vect P,Q_i$ by fresh
constants. Consequently we can construct the cut-free proof
$$\infer=[\textrule{$\forall$-r},\textrule{$\imp$-r},\textrule{$\wedge$-l},\textrule{$\wedge$-r}]{\seq
\Prop{\vect P}{Q_1\wedge Q_2} }{\infer*{\vect{\sigma P}\seq \sigma
Q_1}{p_1} &\infer*{\vect{\sigma P}\seq \sigma Q_2}{p_2}}$$ in
$R_1\cup R_2$.
For Property \ref{hyp:samecf}, the base case is trivial, and the
inductive case is a consequence of Lemma \ref{lemma:2gen}.
\end{Proof}
\begin{multicols}{2}\section{Examples}
In the case of Crabbé's example presented in the introduction, the input is the rewrite
system $A\rightarrow B\wedge\neg A$ and the completion procedure generates $B\rightarrow B\wedge\bot$
which is equivalent to $B\rightarrow\bot$.
With this new rule, we can show that there are no more critical proofs. The proposition
rewrite system
$$\left\{\begin{array}{l}
A\rightarrow B\wedge\neg A\\
B\rightarrow \bot
\end{array}\right.$$ admits \RCut.
The next example deals with quantifiers and is extracted from \citet{hermant}:
$$R\in R~\rightarrow~\forall y.~y\simeq R\imp y\in R \imp C$$ where
$y\simeq z\df\forall x.~(y\in x\imp z\in x)$. It is terminating and
confluent, but does not admits \RCut.
\end{multicols}
The critical proofs have the
form$$\Cut{R\in R}{\seq}{ \Upl{R\in R\seq}{\infer*{R\in R,\forall
y.~y\simeq R\imp y\in R\imp C\seq}{}}} { \Upl{\seq R\in R}{%
\infer*{\seq R\in R,\forall y.~y\simeq R\imp y\in R\imp C}{}}}
$$
The left part can be developed as$$ \Alll{R\in R,\forall y.~y\simeq R\imp y\in R\imp C\seq}{ \Impl{R\in
R,t_1\simeq R\imp t_1\in R\imp C\seq}{ \Impl{R\in R,t_1\in R\imp
C\seq}{ R\in R,C\seq}{R\in R\seq t_1\in R}}{ \Allr{R\in
R\seq t_1\simeq R}{ \Impr{R\in R\seq t_1\in c_1\imp R\in c_1}{
R\in R, t_1\in c_1\seq R\in c_1}}}}
$$
and the right part
as
$$\Allr{\seq R\in R,\forall y.~y\simeq R\imp y\in R\imp C}{ \Impr{\seq
R\in R,c_0\simeq R\imp c_0\in R\imp C}{ \Impr{c_0\simeq R\seq R\in
R,c_0\in R\imp C}{ \Alll{c_0\simeq R,c_0\in R\seq R\in R,C}{
\Impl{c_0\in t_0\imp R\in t_0,c_0\in R\seq R\in R, C}{
R\in t_0,c_0\in R\seq R\in R, C}{c_0\in R\seq c_0\in
t_0,R\in R, C}}}}}\enspace.
$$
To close the proofs, we can for instance have $t_0=R=t_1$, and $C$
in the right part of the sequent (to close $R\in R,C\seq$). One can
see that other choices will not produce critical proofs. The resulting
sequent is therefore $\seq C$, and the added rule is $C\rightarrow
C\vee\top$. This rule does not generate new critical proofs, and
consequently, the proposition rewrite system
$$\left\{\begin{array}{l}
R\in R~\rightarrow~\forall y.~y\simeq R\imp y\in R \imp C\\
C\rightarrow C\vee\top
\end{array}\right.
$$ admits \RCut.
One can also think of another example, where there remains quantifiers
in the conclusion: one can think of a rule derived from Crabbé's example
$A\rightarrow {(\exists x.~\forall y.~B\wedge P(x,y))\wedge \neg A}$ where $A$ and
$B$ are atomic propositions, and $P$ a predicate of arity 2. We have a
critical proof
{\footnotesize
$$\Cut{A}{\exists x.~\forall y.~B\wedge P(x,y)\seq}{ \Upl{\exists x.~\forall y.~B\wedge P(x,y),A\seq}{ \Andl{\exists x.\forall y.B\wedge P(x,y),A,(\exists x.\forall y.B\wedge P(x,y))\wedge\neg A\seq}{
\Notl{A,\exists x.~\forall y.~B\wedge P(x,y),\neg A\seq}{ \Axiomm{A,\exists x.~\forall y.~B\wedge P(x,y)\seq A}}}}} {\Upr{\exists x.~\forall y.~B\wedge P(x,y)\seq A}{
\Andr{\exists x.~\forall y.~B\wedge P(x,y)\seq (\exists x.~\forall y.~B\wedge P(x,y))\wedge\neg A,A} {\Axiomm{\exists x.~\forall y.~B\wedge P(x,y)\seq \exists x.~\forall y.~B\wedge P(x,y),A}} {\Notr{\exists x.\forall y.B\wedge P(x,y)\seq
\neg A,A}{ \Axiomm{\exists x.\forall y.B\wedge P(x,y),A\seq A}}}}}.$$}%
The sequent of the conclusion is transformed into a rewrite rule:\\
$\begin{array}{@{}r@{\text{ becomes }}l@{}}
\exists x.~\forall y.~B\wedge P(x,y)\seq & \forall y.~B\wedge
P(z,y)\seq\\
&B\wedge P(z,a)\seq\neg\underline{\forall y.~B\wedge P(z,y)}\\
& B\seq\neg P(z,a),\neg\underline{\forall y.~B\wedge P(z,y)}\\
&B\ra B\wedge\forall
z.~\left(\neg P(z,a)\vee\neg\forall y.~B\wedge P(z,y)\right) .
\end{array}
$
Then, a cut free proof of $\exists x.~\forall y.~B\wedge P(x,y)\seq$ can
be:
$$\Exl{\exists x.~\forall y.~B\wedge P(x,y)\seq}{
\Alll{\forall y.~B\wedge P(c,y)\seq}{
\Andl{\forall y.~B\wedge P(c,y),B\wedge P(c,a)\seq}{
\Upl{\forall y.~B\wedge P(c,y),B,P(c,a)\seq}{
\Andl{\forall y.~B\wedge P(c,y),B, B\wedge\forall
z.~\left(\neg P(z,a)\vee\neg\forall y.~B\wedge P(z,y)\right),
P(c,a)\seq}{
\Alll{\forall y.~B\wedge P(c,y),B,\forall
z.~\left(\neg P(z,a)\vee\neg\forall y.~B\wedge P(z,y)\right),
P(c,a)\seq}{
\Orl{\forall y.~B\wedge P(c,y),B,\neg P(c,a)\vee\neg\forall y.~B\wedge P(c,y),
P(c,a)\seq}{
\Notl{\forall y.~B\wedge P(c,y),B,\neg P(c,a),P(c,a)\seq}{
\Axiomm{\forall y.~B\wedge P(c,y),B,P(c,a)\seq P(c,a)}}} {
\Notl{\forall y.~B\wedge P(c,y),B,\neg\forall y.~B\wedge P(c,y),
P(c,a)\seq}{
\Allr{\forall y.~B\wedge P(c,y),B,
P(c,a)\seq\forall y.~B\wedge P(c,y)}{
\Alll{\forall y.~B\wedge P(c,y),B,
P(c,a)\seq B\wedge P(c,d)}{
\Axiomm{B\wedge P(c,d),B,
P(c,a)\seq B\wedge P(c,d)}}}}}}}}}}}$$
\begin{multicols}{2}
In these three examples, only one step was needed to produce a saturated
system. But the system
$$R = \left\{\begin{array}{l}
A\rightarrow A\vee B\\
A\rightarrow A\wedge C\\
D\rightarrow D\wedge B\\
D\rightarrow D\vee E
\end{array}\right.
$$ may need two step to produce the completed system
$$R~\cup~\left\{\begin{array}{l}
B\rightarrow B\wedge C\\
B\rightarrow B\vee E\\
C\rightarrow C\vee E
\end{array}\right.\enspace.
$$
Indeed, the first two rules of $R$ create the critical proof
$$\Cut{A}{B\seq C}{
\Upl{B,A\seq C}{
\Andl{B,A,A\wedge C\seq C}{
\Axiomm{B,A,C\seq C}}}}{
\Upr{B\seq A,C}{
\Orr{B\seq A\vee B,A,C}{
\Axiomm{B\seq A,B,C}}}}$$ that leads for instance to the rewrite rule
$B\ra B\wedge C$. Similarly the two other rules may complete the system by the
rewrite rule $B\ra B\vee E$. Consequently, after one step the system has a
critical proof $$\Cut{B}{E\seq C}{
\Upl{E,B\seq C}{
\Andl{E,B,B\wedge C\seq C}{
\Axiomm{E,B,C\seq C}}}}{
\Upr{E\seq B,C}{
\Orr{E\seq B\vee E,B,C}{
\Axiomm{E\seq B,E,C}}}}$$ and may be completed by the rewrite rule $C\ra
C\vee E$.
We nevertheless conjecture that if the initial proposition rewrite
system is confluent, the completion procedure is terminating, possibly
in one step.
\section{Conclusion and Perspectives}
We have shown how, by setting the right abstract canonical system
structure on the proof space of a sequent calculus modulo, we can use
abstract completion to recover the admissibility of \RCut. This
abstract completion is precise enough to be operational, and it is
actually implemented. It also reveals a deep logical correspondence
between the sequent calculus, proof orderings and completion. This
opens many questions that we are now considering.
The ordering on proofs we are using is adapted to consider
cut-freeness as a normal-form property of an ACS, but produces too
much critical proofs, in particular in the case when quantifiers are
involved, because some of the rules produced by the completion
procedure subsumes other one. (For instance $A\ra A\vee\exists
x.~P(x)$ subsumes $A\ra A\vee P(t)$ for a particular $t\in\terms\Sigma
V$.) This ordering has therefore to be refined in order to restrict
oneself to the more relevant critical proofs.
Furthermore, our procedure can be used to determine if a system admits
\RCut. Indeed, if a proposition rewrite system is a fixpoint of this
procedure, then we know that it admits \RCut. Nevertheless, the
converse is not true, essentially because we have to use a superset of
the critical proofs. We have to check what results this procedure will
give on system that are proved to admits \RCut,
like Higher Order Logic \citep{hollambdasigma} or arithmetic
\citep{arith}.
Lastly, our procedure only guarantees the admissibility of \RCut,
not the normalization. For instance, with Crabb\'e's rule, once the
system is completed, the initial proof of $B\seq$ can still be
constructed, and it is still not normalizing, i.e. the $\lambda$-term
that is associated to the proof can be infinitely
$\beta$-reduced. In other words, we do not have a process that
transform proofs with cuts to cut-free ones. We probably have to
introduce some simplification rules in order to suppress the
possibility to build non-normalizing proofs. Moreover, with such
simplification rules, we may obtain the canonical
presentation of the system.
\bibliographystyle{plainnat}
\bibliography{../aacs/abbrev,aacs,../aacs/protheo}
\end{multicols}
\end{document}