CERES in higher-order logic

Abstract

A well-studied logical model of mathematical proofs is the sequent calculus introduced by Gerhard Gentzen. In the sequent calculus, the use of lemmas corresponds to the application of the cut rule. Already Gentzen proved that if a theorem can be proved using the cut rule, it can also be proved without using it. This metamathematical result is called cut-elimination theorem. The original motivation for obtaining it was to establish the consistency of the sequent calculus: It is easy to observe that a contradiction can only be derived by use of the cut rule. But if such a derivation of a contradiction would exist, by Gentzen's result there would also be a derivation of it without the use of cut, which is impossible. Hence the original application of the cut-elimination theorem was to a hypothetical proof.<br />Since then, the formalization of mathematics in the form of proofs in logical systems has been made possible by the computer. Hence it has become possible to apply (implementations of) cut-elimination theorems to (formalizations of) mathematical proofs. The result is a new, cut-free proof, from which interesting information can be extracted.<br />Informally, the proof will be direct: it will not contain detours in the form of lemmas.<br />The subject of this thesis is to extend a well-known method of cut-elimination, CERES (cut-elimination by resolution), from first-order logic to higher-order logic. In first-order logic, both theoretical and practical results have established the value of the method. But first-order logic has some limitations which restrict its usefulness for the formalization of mathematics: often, the intuitive description of mathematical objects cannot be formalized in a straightforward way, but rather needs to be encoded.<br />In higher-order logic, some of the basic syntactical properties of proofs in first-order logic on which CERES depends fail to hold. Hence a more flexible sequent calculus, suitable for CERES, is defined in the thesis, and its properties investigated. Furthermore, a resolution calculus is defined and formally linked to the standard higher-order resolution calculus of Peter B. Andrews. Building on the defined systems, the cut-elimination by resolution method for higher-order logic, CERESomega, is defined.