CERES in higher-order logic

We define a generalization CERESω of the first-order cut-elimination method CERES to higher-order logic. At the core of CERESω lies the computation of an (unsatisfiable) set of sequents CS(π) (the characteristic sequent set) from a proof π of a sequent S. A refutation of CS(π) in a higher-order resolution calculus can be used to transform cut-free parts of π (the proof projections) into a cut-free proof of S. An example illustrates the method and shows that CERESω can produce meaningful cut-free proofs in mathematics that traditional cut-elimination methods cannot reach.

► We give a method of cut-elimination for higher-order logic based on resolution. ► We prove soundness of a sequent calculus based on Skolem terms. ► The method is applied to a concrete mathematical proof. ► We find that it can obtain cut-free proofs not reachable by reductive methods.