Proof-theoretic applications of CERES

Since the time of the ancient Greeks, proofs form the scientific backbone of mathematics. But proofs are not only verifications of theorems but also pieces of evidence and sources of new algorithms and mathematical methods. Proof analysis and proof transformations play a crucial role in this context; in particular the transformation of proofs into elementary ones (logically described as cut-elimination, which can - very roughly - be thought of as an application of Ockham`s razor, as superfluous notions are removed from a proof) can be used to make hidden information explicit. With new theoretical methods and the increasing power of computers the computer-aided analysis of mathematical proofs becomes possible. Towards this aim, the method of cut-elimination by resolution (CERES) - in contrast to other methods of cut- elimination - has been applied successfully: the most prominent application was the analysis of Fürstenberg`s proof of the infinity of primes, from which Euclid`s (elementary) proof could be obtained. The CERES method, and the software system implementing it, have been developed, refined, and experimented with in the previous FWF projects P16264, P17995, and P19875. These past efforts, and the project we now propose, bring us closer to the long-range goal of making computer-aided proof analysis a standard tool for mathematicians. The first main issue tackled in this project is the further improvement of the CERES method: we know that cut- elimination by CERES is, in a certain sense, more powerful than the traditional, so-called reductive methods. Still, in practice the reductive methods may have the advantage that they are more deterministic than CERES. Our aim is therefore to describe the reductive methods as specific resolution refinements. Such refinements will be valuable, since the search of a resolution refutation has turned out to be the major bottleneck in the application of CERES to mathematical proofs, and the refinements will decrease this search space. Apart from increasing the efficiency of CERES, we intend to extend its scope: in its current formulation, CERES is not directly applicable to non-classical logics. We will develop and investigate modifications of CERES which can be used in these logics. The second main issue is the application of the refined CERES method to problems related to proof analysis. Among other aims, we will characterize classes of proofs where fast cut-elimination is possible by means of the resolution refinements, and we will extend the current results on CERES in higher-order logic to full higher-order logic, which will ease practical application of CERES as proofs can be formalized more naturally using higher- order logic.

The aim of this project was the further development and the (primarily theoretical) application of the CERES method. The CERES method, situated in the field of proof theory, is a procedure for the elimination of auxiliary propositions (lemmata) from mathematical proofs (cut-elimination). The lemma-free proofs which are obtained by cut-elimination are computationally interesting: Important information (e.g. bounds on the size of objects) can be extracted from them by means of simple algorithms. In this sense, cut-elimination can be understood as a tool for the extraction of information from proofs. The main result of this project was the generalization of CERES to CERES: The method can now also be applied to the expressive language of higher-order logic. This language is widely used for the formalization of mathematical proofs and is employed by many proof assistants. The generalization therefore allows the application of the CERES method to such proofs directly, avoiding any translation. A corollary of this generalization was the circumvention of so-called proof skolemization, which constitutes a remarkable technical aspect and improves the practical applicability of the CERES method. Another important result was the application of the CERES method to the analysis of the computational complexity of cut-elimination. Roughly speaking, the following question was treated: "Which lemmata are simple, and which are hard to remove from a proof?" The investigations that have been performed by means of the CERES method in this project exhibited a number of classes of lemmata which can be eliminated from proofs (relatively) easily. A practical consequence of this result is that it is possible to check whether a given proof falls into one of the investigated classes and that, if so, fast cut-elimination can be performed on it using CERES. The investigation also contained a methodological component: For one of the investigated classes it was shown that the standard method of cut-elimination, due to G. Gentzen, performs computationally poorly. This proves that an investigation of the complexity of this class with the help of Gentzen`s method cannot be fruitful, while on the other hand the CERES method yields good results. This shows the methodological strength of CERES as a tool for investigations in proof theory.