Constructive validity of a generalized Kreisel-Putnam rule

TL;DR

This paper investigates the constructive validity of the Split rule, a generalized Kreisel-Putnam principle, within the BHK framework and via Curry-Howard. It introduces a typed generalization, the S rule, along with a selector $\mathsf{S}$ that computes the content of $[z: C]\; c(z): A \vee B$ under Harrop hypotheses, and proves that Split and S are interderivable through reduction rules. The results show that the typed S rule is computable and normalizes, providing a constructive interpretation of the Split rule and its content in Martin-Löf's constructive type theory. The work also frames future directions, including a comparison with an implication-elimination-like generalization and connections to prior results on Harrop-rule admissibility and normalization.

Abstract

In this paper, we propose a computational interpretation of the generalized Kreisel-Putnam rule, also known as the generalized Harrop rule or simply the Split rule, in the style of BHK semantics. We will achieve this by exploiting the Curry-Howard correspondence between formulas and types. First, we inspect the inferential behavior of the Split rule in the setting of a natural deduction system for the intuitionistic propositional logic. This will guide our process of formulating an appropriate program that would capture the corresponding computational content of the typed Split rule. In other words, we want to find an appropriate selector function for the Split rule by considering its typed variant. Our investigation can also be reframed as an effort to answer the following questions: is the Split rule constructively valid in the sense of BHK semantics? Our answer is positive for the Split rule as well as for its newly proposed generalized version called the S rule.