Cut-elimination and redundancy-elimination by resolution (Q5927981)

The authors propose a new cut-elimination procedure for classical predicate calculus LK. The basic formulation treats a particular case: \[ \text{if }A,\Gamma\vdash\Delta\text{ is derivable and }A\text{ is valid, then }\Gamma\vdash\Delta\text{ is derivable}.\tag{\(*\)} \] In general a cut like \(\Gamma\vdash B\); \(B,\Gamma\vdash\Delta/\Gamma \vdash\Delta\) is replaced by \(\rightarrow\)-antecedent, introducing a (valid) formula \(B\to B\), into \(B\to B\), \(\Gamma\vdash \Delta\). A simple induction on a derivation \(\psi: A,\Gamma\vdash \Delta\) produces a set of clauses (disjunctions of literals) \(\text{Cl}(\psi,A)\) that can ``replace'' \(A\) in \(\psi\). First, there is a cut-free derivation of the sequent \(A\vdash\) from the universal closure \(\forall\text{Cl}(\psi,A)\), hence \(\forall\text{Cl}(\psi, A)\vdash\neg A\) is derivable and \(\forall\text{Cl}(\psi, A)\) is inconsistent. Second, for every clause \(C\in \text{Cl}(\psi,A)\), written as an implication \(\overline P\vdash\overline Q\) of finite sets of atoms, there is a derivation of \(\overline P,\Gamma\vdash \Delta\), \(\overline Q\) (called projection \(\psi[C]\)). This and the following statements are proved only for skolemized sequents \(\Gamma\vdash \Delta\). Since \(\forall\text{Cl}(\psi, A)\) is inconsistent, there exists a resolution refutation \(R\) of it. Treating the resolution rule as a cut on an atomic formula and replacing each initial clause \(C\in \text{Cl}(\psi,A)\) by the projection \(\psi[C]\). The authors obtain a cut-free proof of \(\Gamma\vdash\Delta\) from \(\psi\) and \(R\). They investigate in detail dependence of this cut-free proof from parameters of \(\psi\). Since nothing except validity of \(A\) is assumed, there is no control over the complexity of \(R\). The authors hope that finding \(R\) may be feasible in some interesting cases. This is supported by an example of a sequence of proofs where the speed-up is hyperexponential. It would be interesting to investigate the relation of the proposed approach to the connection method, to P. Novikov's proof of Herbrand's theorem [\textit{P. Novikov}, Elements of mathematical logic, Oliver \& Boyd, Edinburgh (1964; Zbl 0113.00301)], Kreisel's notion of disjunctive interpretation [\textit{G. Kreisel}, ``Mathematical logic'', Lect. Modern Math. 3, 95-195 (1965; Zbl 0147.24703)], Statman-Orevkov's cut-elimination (providing bounds depending only on the size of the origial proof, not the cut-rank) and to the reviewer's proofs of strengthening of \((*)\) providing normalization for arithmetic [\textit{G. Mints}, ``A normal form theorem for logical derivations implying one for arithmetical derivations'', Ann. Pure Appl. Logic 62, 65-79 (1993; Zbl 0786.03040)]. It is natural to expect easy extensions to non-classical systems having equivalent resolution formulations.