A Generalized Resolution Proof Schema and the Pigeonhole Principle

TL;DR

This paper introduces a generalized resolution proof schema to handle complex refutations in proof schemata, specifically applied to a formalized schematic version of the Infinitary Pigeonhole Principle, advancing cut elimination techniques.

Contribution

It formalizes a schematic version of the IPP in the LKS-calculus and develops a new generalized resolution proof schema to refute clause sets that traditional schemas cannot handle.

Findings

Developed a generalized resolution proof schema based on recursion over lists.

Refuted the clause set extracted from the formal IPP proof using the new schema.

Extracted a Herbrand System from the refutation.

Abstract

The schematic CERES method is a method of cut elimination for proof schemata, that is a sequence of proofs with a recursive construction. Proof schemata can be thought of as a way to circumvent the addition of an induction rule to the LK-calculus. In this work, we formalize a schematic version of the Infinitary Pigeonhole Principle (IPP), in the LKS-calculus, and analyse the extracted clause set schema. However, the refutation we find cannot be expressed as a resolution proof schema because there is no clear ordering of the terms indexing the recursion, every ordering is used in the refutation. Interesting enough, the clause set and its refutation is very close to a canonical form found in cut elimination of LK-proofs. Not being able to handle refutations of this form is problematic in that proof schema, when instantiated, are LK-proofs. Based on the structure of our refutation and structural results, we develop a generalized resolution proof schema based on recursion over a special type of list, and provide a refutation, using our generalization, of the clause set extracted from our formal proof of IPP. We also extract a Herbrand System from the refutation.