Schematic Cut elimination and the Ordered Pigeonhole Principle [Extended Version]
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.
Cite
@article{arxiv.1601.06548,
title = {Schematic Cut elimination and the Ordered Pigeonhole Principle [Extended Version]},
author = {David Cerna and Alexander Leitsch},
journal= {arXiv preprint arXiv:1601.06548},
year = {2023}
}
Comments
Submitted to IJCAR 2016. Will be a reference for Appendix material in that paper. arXiv admin note: substantial text overlap with arXiv:1503.08551