Schematic cut elimination and the ordered pigeonhole principle

Abstract

Schematic cut-elimination is a method of cut-elimination which can handle certain types of inductive proofs. In previous work, an attempt was made to apply the schematic CERES method to a formal proof with an arbitrary number of Π2 cuts (a recursive proof encapsulating the infinitary pigeonhole principle). However the derived schematic refutation for the characteristic clause set of the proof could not be expressed in the schematic resolution calculus developed so far. Without this formalization a Herbrand system cannot be algorithmically extracted. In this work, we provide a restriction of infinitary pigeonhole principle, the ECA-schema (Eventually Constant Assertion), or ordered infinitary pigeonhole principle, whose analysis can be completely carried out in the existing framework of schematic CERES. This is the first time the framework is used for proof analysis. From the refutation of the clause set and a substitution schema we construct a Herbrand system.