Schematic Cut elimination and the Ordered Pigeonhole Principle [Extended Version]

TL;DR

This paper applies the schematic CERES method to the ordered infinitary pigeonhole principle, successfully extracting a Herbrand system from a restricted proof, marking the first such analysis within this framework.

Contribution

It introduces a restriction of the proof to enable formal analysis using the schematic CERES method, facilitating the extraction of Herbrand systems from complex proofs.

Findings

Successful formalization of the ECA-schema within the CERES framework

Construction of a Herbrand system from the refutation and substitution schema

First application of the schematic CERES method to the ordered pigeonhole principle

Abstract

In previous work, an attempt was made to apply the schematic CERES method [8] to a formal proof with an arbitrary number of {\Pi} 2 cuts (a recursive proof encapsulating the infinitary pigeonhole principle) [5]. However the derived schematic refutation for the characteristic clause set of the proof could not be expressed in the formal language provided in [8]. Without this formalization a Herbrand system cannot be algorithmically extracted. In this work, we provide a restriction of the proof found in [5], the ECA-schema (Eventually Constant Assertion), or ordered infinitary pigeonhole principle, whose analysis can be completely carried out in the framework of [8], 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.