Constructive validity of a generalized Kreisel-Putnam rule

TL;DR

This paper provides a computational interpretation of the generalized Kreisel-Putnam rule within BHK semantics, demonstrating its constructive validity and proposing a typed selector function for the rule.

Contribution

It introduces a typed computational interpretation of the generalized Kreisel-Putnam rule, establishing its constructive validity and formulating a selector function within the Curry-Howard framework.

Findings

The generalized Kreisel-Putnam rule is constructively valid in BHK semantics.

A typed selector function for the rule is formulated.

The validity extends to the newly proposed S rule.

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.