\documentclass{birkmult}
\usepackage{amsmath,amssymb}

 \newtheorem{thm}{Theorem}[section]
 \newtheorem{cor}[thm]{Corollary}
 \newtheorem{lem}[thm]{Lemma}
 \newtheorem{prop}[thm]{Proposition}
 \theoremstyle{definition}
 \newtheorem{defn}[thm]{Definition}
 \theoremstyle{remark}
 \newtheorem{rem}[thm]{Remark}
 \newtheorem*{ex}{Example}
 \numberwithin{equation}{section}

%\newcommand{\rep}[2]{{}^{#1}_{#2}}       %replace #1 with #2
\newcommand{\ins}[1]{\mathbb{I}_{#1}}    %set of instances of a rule
\newcommand{\ca}{\mathcal{C}}            %calculus
\newcommand{\regel}[2]{\frac{#1}{#2}}
%\newcommand{\regel}[2]{\frac{\displaystyle #1}{\displaystyle #2}}
%\newcommand{\ide}{\triangle}             %identity connective
\newcommand{\true}{\mathbf{true}}        %truth value true
\newcommand{\false}{\mathbf{false}}      %truth value false
\newcommand{\sr}{\blacktriangleright}    %simple rule
\newcommand{\fta}{\mathcal{T}}           %free term algebra with metavars
%\newcommand{\var}{\mathbb{V}}            %set of variables
%\newcommand{\grt}{\mathbb{G}}            %set of ground terms
%\newcommand{\for}{\mathbb{F}}            %set of formulas
\newcommand{\sen}{\mathbb{S}}            %set of sentences
\newcommand{\tup}[1]{\langle #1\rangle}  %tuple
%\newcommand{\dr}{\rhd}                   %deduction relation
%\newcommand{\sdr}{\mathcal{D}}           %set of deduction relations
%\newcommand{\cl}{\mathbb{C}}             %closure
%\newcommand{\clc}[1]{\cl_c(#1)}          %closure under composition
\newcommand{\fap}{\forall^{\mathrm{par}}} %universal closure w.r.t. parameters
\newcommand{\lan}{\mathcal{L}}            %language



\title{Composition of Rules of Frege-Hilbert Calculi}
\author{Elmar Eder}
\address{Department of Computer Sciences,
University of Salzburg\\
Jakob-Haringer-Str.~2,
5020 Salzburg, Austria}
\email{eder@cosy.sbg.ac.at}



\begin{document}

\maketitle


\section{Introduction}
\label{sec:Int}

Inference mechanisms based on backward reasoning in cut-free sequent
calculi have been widely adopted for systems of automated as well as
interactive deduction such as the connection method \cite{Bibel87} or
tableau systems \cite{Beth55}. Since application of the cut rule can
dramatically shorten proofs as Statman \cite{Statm79} and Orevkov have
shown, it seems desirable to incorporate a cut rule in such systems.
For automated reasoning this, however, poses the problem that there is
an infinite number of possible backward applications of the cut rule
at each step of backward reasoning, yielding the backward proof search
intractable.
A remedy is to compute derivation schemes instead of
derivations \cite{eder:backw,27}. For example, instead of proving
$\lnot\lnot\lnot P\vdash\lnot P$ where $P$ is a proposition symbol, we
prove a general rule `$\regel{\lnot\lnot A}{A}$' where `$A$' is a
metavariable standing for an arbitrary formula. A proof is constructed
by repeatedly building the composition of two such rules using
unification on metavariables. In this paper the algebra of rules is
studied for Frege-Hilbert calculi which have a simpler mathematical
structure than sequent calculi. The results carry over to sequent
calculi which are better suited for automation as well as interactive
systems.

Let $\sen$ be the set of \emph{sentences}, i.e.\ of closed formulas. A
\emph{rule} $R$ defines a subset $\ins{R}$ of $\sen^n\times\sen$ where
$n\ge 0$ is the arity of $R$. The elements of $\ins{R}$ are called
\emph{instances} of $R$. The \emph{$k$-th composition} of two rules
$R$ and $\hat R$ is the rule whose instances are those pairs
$\tup{\tup{B_1,\dots,B_{k-1},A_1,\dots,A_m,B_{k+1},\dots,B_n},C}$ for
which there is a $B_k$ such that
$\tup{\tup{A_1,\dots,A_m},B_k}\in\ins{R}$ and
$\tup{\tup{B_1,\dots,B_n},C}\in\ins{\hat R}$. A \emph{Frege-Hilbert
  calculus} is given by a finite set of rules. A rule is
\emph{composable in} a calculus $\ca$, or $\ca$-composable, if it is a
composition of rules of $\ca$. Our goal is to determine the set of
$\ca$-composable rules and the operator of $k$-th composition on it.

A rule $R$ \emph{subsumes} a rule $\hat R$ ($R\le\hat R$) if
$\ins{\hat R}\subset\ins R$. Subsumption is Noetherian on the set of
rules composable in a traditional Frege-Hilbert calculus (though not
on the set of all possible rules). Thus, for each such rule there is a
$\le$-minimal rule subsuming it. An investigation of the set of
$\le$-minimal rules with the operation of composition followed by
subsumption is left for future research.



\section{Examples of Frege-Hilbert Calculi}
\label{sec:Exa}


\subsection*{The Propositional Calculus $\ca_0$}
\begin{gather}
  A\to B\to A\tag{A1}\\
  (A\to B\to C)\to(A\to B)\to A\to C\tag{A2}\\
  (\lnot A\to\lnot B)\to B\to A\tag{A3}\\
  \regel{A\quad A\to B}{B}\tag{R1}
\end{gather}


\subsection*{The First Order Calculus $\ca_1$}
has the rules (A1), (A2), (A3), (R1), and the rules
\begin{gather*}
  \forall xF[x]\to F[t]\tag{A4}\\
  \regel{A\to F[p]}{A\to\forall xF[x]}
  \rlap{\qquad ($p\notin A,F$)}\tag{R2}
\end{gather*}
In (A4), `$t$' denotes a ground term. In (R2), `$p$' denotes a
\emph{parameter}, i.e., an auxiliary constant introduced by the
calculus. The condition `$p\notin A,F$' means that the
\emph{eigenparameter} $p$ of an instance of (R2) must not occur in $A$
or in $F$.


\subsection*{The Propositional Calculus $\ca_1'$}
For a reason to become clear later, we use the symbol $\forall$ in
this calculus to denote the unary propositional connective of identiy:
$\forall\true=\true$ and $\forall\false=\false$.  The calculus
$\ca_1'$ has the rules (A1), (A2), (A3), (R1), and the two rules
\begin{gather*}
  \forall F\to F\tag{A4$'$}\\
  \regel{A\to F}{A\to\forall F}\tag{R2$'$}
\end{gather*}


\section{Derivability in a Sound and Complete Frege-Hilbert Calculus}
\label{sec:der}

For $A\in\sen$ let $\fap A$ be the universal closure of the result of
consistently and injectively replacing the parameters in $A$ with
variables not occuring in $A$ (replacing each parameter $p$ with
$\iota(p)$ where $\iota$ is injective). For $S\subset\sen$ let $\fap
S:=\{\fap A\mid A\in S\}$. For a calculus $\ca$ let $S\vdash_\ca B$
mean that $B$ is in the closure of $S$ under the rules of $\ca$. Then
all traditional sound and complete Frege-Hilbert calculi $\ca$ such as
$\ca_0$, $\ca_1$, and $\ca_1'$ are strongly adequate: $S\vdash_\ca B$
if and only if $\fap S\models\fap B$.

This strong soundness and completeness result gives us the set of all
%pairs $\tup{\{A_1,\dots,A_n\},B}$ such that
pairs $\tup{S,B}$ such that for some $A_1,\dots,A_n\in S$ the pair
$\tup{\tup{A_1,\dots,A_n},B}$ is an instance of a $\ca$-composable
rule. It is the set $\{\tup{S,B}\mid\fap S\models\fap B$\}. The result
is, however, too coarse-grained to precisely determine the set of
$\ca$-composable rules.


\section{A Variant of the Deduction Theorem}
\label{sec:dt}

A parameter $p$ is an \emph{eigenparameter} of an instance $I$ of a
rule $R$ if there is a constant $a$ such that the result of replacing
every occurrence of $p$ in $I$ with $a$ is not an instance of
$R$. The instance $I$
is \emph{compatible} with a formula $D$ if the eigenparameters of $I$
do not occur in $D$.  For a rule $R$ let $\vec R$ be the rule whose
instances are the pairs $\tup{\tup{D\to A_1,\dots,D\to A_n},D\to B}$
such that $\tup{\tup{A_1,\dots,A_n},B}$ is compatible with $D$. A rule
$R$ is \emph{good} for a calculus $\ca$, or \emph{$\ca$-good}, if
$\vec R$ is $\ca$-composable. A calculus $\ca$ is \emph{good} if its
rules are $\ca$-good and invariant under permutations of parameters.

If (A1) and (A2) are $\ca$-composable then (R1) and all
eigenparameter-free axiom schemes of $\ca$ are $\ca$-good. The calculi
$\ca_0$, $\ca_1$, and $\ca_1'$ are good. Compositions of $\ca$-good
rules are $\ca$-good. Thus rules composable in a good calculus $\ca$
are $\ca$-good.

\begin{prop}
  Let $\ca$ be a good calculus in which (A1), (A2), and (R1) are
  composable. Let $\phi\colon\{1,\dots,m\}\to\{0,\dots,n\}$. Let $R$
  be a $\ca$-composable rule. Then there is an $m$-ary
  $\ca$-composable rule $\hat R$ whose set of instances is the set of
  pairs $\tup{\tup{A_1,\dots,A_n},A_0\to B}$ such that
  $\tup{\tup{A_{\phi(1)},\dots,A_{\phi(n)}},B}$ is an instance of $R$
  which is compatible with $A_0$.
\end{prop}


\section{Frege-Hilbert Calculi for Propositional Logic}
\label{sec:pro}

A Frege-Hilbert calculus $\ca$ for propositional logic uses
propositional connectives as well as metavariables for formulas. For
example, calculus $\ca_0$ uses the connectives $\lnot$ and $\to$ and
the metavariables `$A$', `$B$', and `$C$'. Let $\fta$ be the free term
algebra based on the propositional connectives of $\ca$ as its
function symbols and on some infinite superset of the set of
metavariables of $\ca$ as its variables. A \emph{simple rule} is a
rule of the form $\frac{\Phi_1\dots\Phi_n}{\Psi}$ where
$\Phi_1,\dots,\Phi_n,\Psi$ are terms of $\fta$. The rules of
traditional propositional Frege-Hilbert calculi are simple rules. Note that
consistently and injectively replacing the metavariables in
$\Phi_1,\dots,\Phi_n,\Psi$ with proposition symbols results in
formulas $A_1,\dots,A_n,B$. We write $A_1,\dots,A_n\sr B$ for
$\frac{\Phi_1\dots\Phi_n}{\Psi}$.

A composition of two simple rules can be computed using unification on
the term algebra $\fta$, much the same way as two first order Horn
clauses are resolved using unification. It is again a simple rule. And
a composition of two sound rules is again sound. Thus if $\ca$ is a
Frege-Hilbert calculus whose rules are sound and simple then every
$\ca$-composable rule is sound and simple. Unfortunately, it is not
true in general that a sound simple rule is $\ca$-composable, even if
$\ca$ is complete (as well as sound). A counterexample is the calculus
obtained from $\ca_0$ by replacing (R1) with $\frac{A\quad A\quad A\to
  B}{B}$.  In it the rule (R1) is not composable.

\begin{prop}\label{prop:complete-prop}
  Let $\ca$ be a complete propositional Frege-Hilbert calculus such
  that (A1), (A2), and (R1) are $\ca$-composable. Let
  $A_1,\dots,A_n\models B$. Then $A_1,\dots,A_n\sr B$ is
  $\ca$-composable.
\end{prop}

It is easy to show that $A_1,\dots,A_n\sr B$ is subsumed by a
$\ca$-composable rule $R$. 
The harder part of the proof is to show that $A_1,\dots,A_n\sr B$
subsumes $R$.


\section{Frege-Hilbert Calculi for First Order Logic}
\label{sec:fir}

Given a first order language $\lan$, let $\mathcal{L'}$ be the
propositional language whose proposition symbols are the predicate
symbols of $\lan$ and whose propositional connectives are the
propositional connectives and quantifiers of $\lan$.  Quantifiers
$\forall$ or $\exists$ of $\lan$ denote the identity connective in
$\lan'$. For a first order formula $F$ let $F'$ be the formula of
$\lan'$ obtained from $F$ by omitting arguments of predicate symbols
and variables in quantifier prefixes. For example, if $F=\forall
x(P(x)\to\lnot\forall yQ(x,f(x,y)))$ then $F'=\forall(P\to\lnot\forall
Q)$. The operator $'$ is extended in the natural way to rules, to
calculi (see the calculus $\ca_1'$), and to derivations.

%\begin{rem}
%  Let $A$ be a sentence of $\lan$. Then $A'$ is valid if and only if
%  $A$ is valid in a single-element domain.
%\end{rem}

%\begin{rem}
%  Let $B$ be a sentence of $\lan'$. Then $B$ is valid if and only if
%  there is a valid sentence $A$ of $\lan$ such that $B=A'$.
%\end{rem}

%\begin{proof}
%  Simply use some constant $a$ as arguments of predicate symbols.
%\end{proof}

\begin{prop}
  Let $\ca$ be a first order Frege-Hilbert calculus. Then $'$ maps the
  set of derivations in $\ca$ surjectively to the set of derivations
  in $\ca'$. As a consequence, the set of instances of a composition
  of rules of $\ca$ is nonempty if and only if the set of instances of
  the corresponding composition of rules of $\ca'$ is nonempty.
\end{prop}

The significance of this proposition is that the propositional part of
determining the composition of two rules and the part concerning the
terms within the predicate symbols can be seperated from each other to
a great extent. First the composition of the corresponding
propositional rules of $\ca'$ is computed which can be done by simple
unification. If this succeeds then it is guaranteed that the
composition of first order rules also represents a nonempty class of
derivations. Then the terms and the constraints are computed which
have to be imposed on rules in first order logic (see
\cite{eder:backw}). Constraints are eigenparameter conditions
($p\notin F$, $p\notin t$, $p\neq q$) or equations
$F[s_1,\dots,s_m]=G[t_1,\dots,t_n]$ where
$s_1,\dots,s_m,t_1,\dots,t_n$ are metavariables for ground terms or
for parameters. For example, the axiom scheme $\forall
xF[x]\to\lnot\forall y\lnot G[y]\quad (F[s]=G[t])$ is
$\ca_1$-composable.
%It is, however, open which finite sets of eigenparameter conditions
%and equations may actually occur in $\ca_1$-composable rules. Whereas
%in propositional logic Proposition~\ref{prop:complete-prop} guarantees
%that every sound simple rule is composable in a complete Frege-Hilbert
%calculus, it is still open whether a similar result holds for first
%order logic.




%I generated the following bibliography with BibTeX as a file
%macis_Eder.bbl using the two commands
%
%\bibliographystyle{plain}
%\bibliography{macis_Eder.bib}
%
%Then I manually edited and modified it and copied it verbatim
%into this file macis_Eder.tex.


\begin{thebibliography}{1}

\bibitem{Beth55}
Evert~W. Beth.
\newblock Semantic entailment and formal derivability.
\newblock {\em Mededlingen der Koninklijke Nederlandse Akademie van
  Wetenschappen}, 18(13):309--342, 1955.

\bibitem{Bibel87}
Wolfgang Bibel.
\newblock {\em Automated Theorem Proving}.
\newblock Artificial Intelligence. Vieweg, Braunschweig/Wiesbaden, second
  edition, 1987.

\bibitem{eder:backw}
Elmar Eder.
\newblock Backward reasoning in systems with cut.
\newblock In J. Calmet, J.~A. Campbell, and J. Pfalzgraf, eds.,
  {\em Artificial Intelligence and Symbolic Computation, Int.\ Conf.,\
    AISMC-3}, vol.\ 1138 of {\em Lecture Notes in Computer Science},
  339--353. Springer, 1996.

\bibitem{27}
Elmar Eder.
\newblock Algebraic properties of rules of Frege-Hilbert calculi.
\newblock In H. Efinger and A. Uhl, eds., {\em Scientific Computing
  in Salzburg, Festschrift P.\ Zinterhofs 60th
  Birthday},
  189 of {\em books@ocg}, 87--96. \"Osterreichische Computer
  Gesellschaft, Wien, Austria, 2005.

\bibitem{Statm79}
R.~Statman.
\newblock Lower bounds on {H}erbrand's theorem.
\newblock {\em Proc.\ AMS}, 75, 1979.

\end{thebibliography}

\end{document}






***************************************************************************
***************************************************************************
***************************************************************************
***************************************************************************
***************************************************************************
***************************************************************************
***************************************************************************
***************************************************************************





\begin{lem}\label{lem:1}
  Let $\ca$ be a complete Frege-Hilbert calculus whose rules are
  simple. Assume that (R1) is $\ca$-composable. Then every sound
  simple rule is subsumed by a $\ca$-composable rule.
\end{lem}

\begin{proof}
  Let $A_1,\dots,A_n\sr B$ be a sound simple rule. Then
  $A_1,\dots,A_n\models B$. Thus $A_n\to\dots\to A_1\to B$ is valid.
  By the completeness of $\ca$ there is a proof of $A_n\to\dots\to
  A_1\to B$ in $\ca$. Thus there is a $\ca$-composable rule $R_0$ such
  that $\tup{\tup{},A_n\to\dots\to A_1\to B}$ is an instance of $R_0$.
  For $k=1,\dots,n$ let $R_n$ be the second composition of $R_{n-1}$
  and (R1). Then $R_n$ is $\ca$-composable, and
  $\tup{\tup{A_1,\dots,A_n},B}$ is an instance $R_n$. Thus $R_n$
  subsumes $A_1,\dots,A_n\sr B$.
\end{proof}

This result can be extended to calculi for languages which do not have
$\to$ as a propositional conncective by expressing $\to$ in terms of
other connectives. While this lemma guarantees in a sense that every
sound simple rule can be obtained from rules of the calculus, it would
be nice to be able to construct the rule just by composition without
subsumption. For example, we want to find a composition of rules which
proves $(A\to B)\to(A\to B)$ but does not prove $A\to A$. Call a
formula $A$ \emph{obtainable} in a calculus $\ca$ if the simple rule
$\sr A$ is $\ca$-composable. If $\ca$ is a complete calculus and $B$
is a valid formula then there is a formula $A$ obtainable in $\ca$
which is more general than $B$ in the sense that $B$ is obtained from
$A$ by consistently replacing proposition symbols with formulas.

\begin{lem}\label{lem:2}
  Let $U,V,\tilde U,\tilde V$ be proposition symbols. Then the
  following formulas are obtainable in $\ca$. $U\to U$, $(\tilde U\to
  U)\to\lnot U\to\lnot\tilde U$, $(\tilde U\to U)\to(V\to\tilde
  V)\to(U\to V)\to\tilde U\to\tilde V$, $(U\to U)\to(U\to U)$, $U\to
  U\to U$, and $U\to V\to V$.
\end{lem}

\begin{lem}
  Let $\ca$ be a calculus in which (A1), (A2), and (R1) are
  composable.  Let $\phi$ be a surjection from $\{1,\dots,m\}$ to
  $\{1,\dots,n\}$ and let $A_1,\dots,A_n,B$ be formulas. Then
  $A_{\phi(1)},\dots,A_{\phi(m)}\sr B$ is $\ca$-composable if and only
  if $A_1,\dots,A_n\sr B$ are $\ca$-composable.
\end{lem}

Here is a variant of the deduction theorem.
\begin{prop}
  Let $\ca$ be a Frege-Hilbert calculus in which (A1), (A2) and (R1)
  are composable such that $\ca$ has no proper rules except (R1). Let
  $A_1,\dots,A_n,D,E$ be formulas. Then the rule $A_1,\dots,A_n,D\sr
  E$ is $\ca$-composable if and only if the rule $A_1,\dots,A_n\sr
  D\to E$ is $\ca$-composable.
\end{prop}

\begin{lem}\label{lem:3}
  Let $\ca$ be a complete Frege-Hilbert calculus in which (A1), (A2),
  and (R1) are composable. Then every valid formula is obtainable in
  $\ca$.
\end{lem}

\begin{proof}
  The idea is first to replace all occurrences of proposition symbols
  with pairwise distinct proposition symbols $U_1,\dots,U_n$ obtaining
  a new formula $B$. Prove by induction on the length of $B$ that
  $U_1\to U_1,\dots,U_n\to U_n\sr B\to B$ is $\ca$-composable.

  **************************************************************************
  **************************************************************************
  *************** Beweis leider falsch **************
  **************************************************************************
  **************************************************************************
  Let $A$ have $k$ occurrences of proposition symbols $U_1,\dots,U_k$.
  Let $P_1,\dots,P_k$ be pairwise distinct proposition symbols. Let
  $B$ be the result of replacing the $k$ occurrences of proposition
  symbols in $A$ with $P_1,\dots,P_k$, respectively. Let
  $E_1,\dots,E_n$ be all the formulas $P_i\to P_j$ with $U_i=U_j$.
  Then $E_1\to\dots\to E_n\to B$ is valid. By the completeness of
  $\ca$, there is a proof of $E_1\to\dots\to E_n\to B$ in $\ca$. Thus
  there is a $\ca$-composable rule $R_0$ such that
  $\tup{\tup{},E_1\to\dots\to E_n\to B}$ is an instance of $R_0$. Note
  that $P\sr P$ equals
  $(\text{(A2)1}(\text{(A1)1(R1)}))1(\text{(A1)1(R1)})$ and is
  therefore $\ca$-composable. Now let $R_k:=R_{k-1}1((P\sr
  P)1\text{(R1)})$ for $k=1,\dots,n$. Then $R_n$ is the rule $\sr A$.
\end{proof}



% Hier noch der Beweis für den folgenden Satz, der oben im Text
% vorkommt:

\begin{prop}
  Let $\ca$ be a complete Frege-Hilbert calculus such that (A1), (A2),
  and (R1) are $\ca$-composable. Let $A_1,\dots,A_n\models B$. Then
  $A_1,\dots,A_n\sr B$ is $\ca$-composable.
\end{prop}

\begin{proof}
  By Lemma~\ref{lem:3}, $\sr A_1\to\dots\to A_n\to B$ is
  $\ca$-composable. A construction similar as in the proof of
  Lemma~\ref{lem:1} yields the assertion.
\end{proof}



Thus, some of the results for propositional logic can be lifted to
first order logic. Unfortunately however, in first order logic the
composition of two simple rules is in general not a simple rule.
Therefore constraints in the form of equations between formulas and in
the form of eigenparameter conditions have to be added. Certainly,
eigenparamter conditions do not always just state that the
eigenparameter must not occur in the conclusion. For example, each of
the two rules $\frac{A\quad A\to F[p]}{\forall xF[x]}\ \scriptstyle
(p\notin A,F)$ and $\frac{A\quad A\to F[p]}{\forall xF[x]}\
\scriptstyle (p\notin F)$ is $\ca_1$-composable.  Equation constraints
have always the form




%%% Local Variables: 
%%% mode: latex
%%% TeX-master: t
%%% End: