Methods of cut-elimination (Q609451)

The book summarizes work by the authors and their collaborators on a new method of normalization of proofs called cut elimination by resolution (CERES). A clause \(p\vee q\vee\neg r\vee\neg s\) looks in their notation as \(r,s\vdash p,q\). CERES is applicable to prrofs of \textit{Skolemized} sequents in the classical first-order logic containing no weakening rules (so that even redundant formulas are carried out to the axioms). Each axiom \(S=X,A\vdash A,Y\) in a given derivation \(\phi\) is assigned a clause \(X',A'\vdash A'',Y'\) consisting of all formulas in \(S\) traceable to cut formulas. The whole derivation \(\phi\) is assigned a characteristic clause term \(\Theta(\phi)\) which is a \((\&,\vee)\)-combination of the clauses assigned to the axioms. \(\Theta(\phi)\) is polynomial in the size of \(\phi\), but the result \(Cl(\phi)\) of transforming \(\Theta(\phi)\) into a conjunction of clauses may be exponential. Three results at the background of CERES are: {\parindent5mm \begin{itemize}\item[1.] The (universal closure) of \(Cl(\phi)\) is unsatisfiable. \item[2.] For each clause \(C\in Cl(\phi)\) the result of ``adding'' (i.e. forming a disjunction) a substitution instance of \(C\) to each sequent in \(\phi\) is a cut-free derivation. \item[3.] Any resolution derivation of a contradiction from \(Cl(\phi)\) results (via 1 and 2) in a derivation (of the same endsequent as in \(\phi\)) containing cuts only over atomic formulas. \end{itemize}} The remaining cuts can be eliminated in a standard way with at most exponential blow-up, but their presence is not an obstacle to most applications of cut elimination including interpolation. The speed-up by CERES over the standard methods of cut elimination is possible for example when \(Cl(\phi)\) belongs to one of the classes efficiently decided by resolution. Several such useful classes are described. Other potential applications concern proof-mining, i.e., analysis of mathematical proofs by extracting additional information and generalization. Extensions of CERES to non-classical logics is restricted by the necessity of Skolemization. One positive example in this book concerns many-valued logics with (what the authors call) distributive quantifiers.