Computer-Aided Analysis of Inductive and Second Order Proofs

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) allows the extraction of bounds and programs from proofs. With new theoretical methods and the increasing power of computers the computer-aided analysis of mathematical proofs becomes possible. In the previous FWF projects P16264 and P17995 a software system has been developed that is capable of performing cut-elimination based on the CERES-method (cut-elimination by resolution) on realistic mathematical proofs formalized in first-order logic. The system has been used to carry out a successful analysis of Fürstenberg`s proof of the infinity of primes by topological methods. This project aims at extending the CERES-method and the system to cover also induction (which is of fundamental importance for mathematical proofs) and parts of second-order logic. This will result not only in a much broader scope of proofs that can be analyzed but also in a simpler formulation of proofs that could already be analyzed by the present system. To realize this aim, on the one hand the theoretical analysis of the CERES-method has to be deepened and extended to stronger systems. In particular, we plan to treat the system ACA0 which is arithmetic whose only second-order part is the formalization of the induction axiom. On the other hand we will develop and implement a resolution calculus without the need for skolemization and other shortcomings of present theorem provers which will be crucial in the extension of CERES. Furthermore we will apply the new system to the analysis of several mathematical proofs, an interesting candidate being the theorem on the representability of numbers as sum of two squares.

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) allows the extraction of bounds and programs from proofs. With new theoretical methods and the increasing power of computers the computer-aided analysis of mathematical proofs becomes possible. In the previous FWF projects P16264 and P17995 a software system has been developed that is capable of performing cut-elimination based on the CERES-method (cut-elimination by resolution) on realistic mathematical proofs formalized in first-order logic. The system has been used to carry out a successful analysis of Fürstenberg`s proof of the infinity of primes by topological methods. This project aims at extending the CERES-method and the system to cover also induction (which is of fundamental importance for mathematical proofs) and parts of second-order logic. This will result not only in a much broader scope of proofs that can be analyzed but also in a simpler formulation of proofs that could already be analyzed by the present system. To realize this aim, on the one hand the theoretical analysis of the CERES-method has to be deepened and extended to stronger systems. In particular, we plan to treat the system ACA0 which is arithmetic whose only second-order part is the formalization of the induction axiom. On the other hand we will develop and implement a resolution calculus without the need for skolemization and other shortcomings of present theorem provers which will be crucial in the extension of CERES. Furthermore we will apply the new system to the analysis of several mathematical proofs, an interesting candidate being the theorem on the representability of numbers as sum of two squares.