Introduction
Cut-elimination was originally introduced by G. Gentzen as a theoretical tool from which results like decidability and consistency could be proven. Cut-free proofs are computationally explicit objects from which interesting information such as Herbrand disjunctions and interpolants can be easily extracted. When viewing formal proofs as a model for mathematical proofs, cut-elimination corresponds to the removal of lemmas, which leads to interesting applications (such as one described below).
For such applications to mathematical proofs, the cut-elimination method CERES (cut-elimination by resolution) was developed (for first- and higher-order classical logic) [1, 2, 3, 6]. It essentially reduces cut-elimination for a proof \pi to a theorem proving problem: the refutation of the characteristic clause set CL(\pi). Given a resolution refutation \gamma of CL(\pi), an essentially cut-free proof can be constructed by a proof-theoretic transformation.
The present work is motivated by an application of CERES to (a formalization of) a mathematical proof: Fuerstenberg's proof of the infinity of primes [9, 10]. Since cut-elimination in the presence of induction is problematic, the proof was formalized as a sequence of proofs (\pi_k)_{k \in \mathbf{N}} showing that the assumption that there exist exactly k primes is contradictory. The application was performed in a semi-automated way: CL(\pi_k) was computed for some small values of k and from this, a general scheme CL(\pi_n) was constructed and subsequently analyzed by hand. The analysis finally showed that from Fuerstenberg's proof, which makes use of topological concepts, Euclid's elementary proof could be obtained by cut-elimination. It was unsatisfactory that the fact that CL(\pi_n) is really the correct schema for all n \in \mathbf{N} could not be verified, and that the analysis of CL(\pi_n) could not be performed in a computer-aided way.
Hence the present work is concerned with the investigation of a formal concept of proof schema. The aim is to define a CERES method for proof schemata that will yield the schematic CL(\pi_n) directly. Not only will this close the gap in the application described above (and in future ones) by automatically computing the correct schema CL(\pi_n), but it will also allow (semi-)automated application of the method using theorem provers and proof assistants based on the formal definitions.
Schemata play a central role in modern mathematical logic. It is used in a meta level only and the first steps of formalizing schematic language for so called iteration schemata were done in [4, 7]. The subclass of regular schemata was identified and shown decidable, and a tableau calculus STAB was defined and implemented in [5]. We start our investigation into proof schemata with the case of propositional logic and continue with the extension to first-order schemata in the near future.
To achieve the goal of this project, we need to:
- Develop a schematic version of sequent calculus with a notion of proof schema based on primitive recursive definitions.
- Develop a method to extract schematic characteristic clause sets and schematic projections from these proof schemata.
- Develop a schematic resolution calculus for refutation of schemata of clause sets, which can be applied to refute the schematic characteristic clause sets.
- Develop a method that plugs together all these objects and gives a schematic representation of the atomic cut normal forms.
- Implement the method (as a part of the GAPT framework).