Constructive Validity of a Generalized Kreisel-Putnam Rule

Basic Information

• Paper ID: 2311.15376
• Title: Constructive validity of a generalized Kreisel-Putnam rule
• Author: Ivo Pezlar (Czech Academy of Sciences, Institute of Philosophy)
• Classification: cs.LO (Computer Science - Logic in Computer Science), math.LO (Mathematics - Logic)
• Publication Date: November 28, 2023 (arXiv v2)
• Paper Link: https://arxiv.org/abs/2311.15376

Abstract

This paper proposes a computational interpretation of the generalized Kreisel-Putnam rule (also known as the generalized Harrop rule or Split rule) in the style of BHK semantics. This is achieved by leveraging the Curry-Howard correspondence between formulas and types. The paper first examines the inferential behavior of the Split rule in a natural deduction system for intuitionistic propositional logic, which guides the formulation of appropriate programs to capture the corresponding computational content of the typed Split rule. In other words, the authors seek to find appropriate selector functions for the Split rule by considering its typed variants. The research can be reformulated as answering the following question: Does the Split rule possess constructive validity in the sense of BHK semantics? The authors provide an affirmative answer for both the Split rule and its newly proposed generalized version, called the S rule.

Research Background and Motivation

Core Problem

The core problem addressed in this paper is: Does the Split rule possess constructive validity in the sense of BHK semantics? Specifically, it seeks to find a constructive function that can transform arbitrary proofs of the premises of the Split rule into proofs of its conclusion.

Problem Significance

1. Theoretical Significance: The Kreisel-Putnam rule is an admissible but underivable rule in intuitionistic logic, though it is proof-theoretically valid in variants of Dummett-Prawitz style semantics.
2. Logical System Properties: When the Split rule is added to intuitionistic logic, the resulting system (such as inquisitive intuitionistic logic) maintains the disjunction property while possessing structural completeness, a characteristic of classical logic.
3. Broad Applications: The Split rule appears in multiple domains such as domain logic, demonstrating its foundational importance.

Limitations of Existing Approaches

1. Lack of Computational Interpretation: Despite the significance of the Split rule, its proof-theoretic meaning and computational content remain largely unexplored.
2. Unclear Constructive Validity: There is no explicit constructive function to interpret the computational content of the Split rule.

Research Motivation

Through the Curry-Howard correspondence, treating formulas as types, the authors seek appropriate selector functions to capture the computational content of the Split rule, thereby establishing its constructive validity.

Core Contributions

1. Proposed the S Rule: Reformulated the Split rule as a generalized form of the disjunction elimination rule, termed the S rule.
2. Established Constructive Validity: Found valid selector functions S for the S rule, proving its constructive validity.
3. Provided Computational Interpretation: Gave a complete computational interpretation of the Split rule through typed variants and computational rules.
4. Proved Normalization Property: Demonstrated that normalization is preserved when the typed S rule is added to Martin-Löf constructive type theory.
5. Established Rule Equivalence: Proved the equivalence between the Split rule and the S rule, providing corresponding reduction processes.

Methodology Details

Task Definition

Input: Premises of the Split rule C → (A ∨ B), where C is a Harrop formula Output: Conclusion of the Split rule (C → A) ∨ (C → B)Constraint: Find a constructive function implementing the transformation from premises to conclusion

Core Methodological Architecture

1. Rule Reformulation

Reformulating the original Split rule:

C → (A ∨ B)
─────────────── Split
(C → A) ∨ (C → B)

into the S rule (disjunction elimination form):

[C]
 ⋮
A ∨ B    [C → A]    [C → B]
          ⋮           ⋮
          D           D
─────────────────────────── S
            D

2. Typed S Rule

Under the Martin-Löf constructive type theory framework, the typed form of the S rule is:

[z : C]
  ⋮
c(z) : A ∨ B    [x : C → A]    [y : C → B]
                   ⋮              ⋮
                d(x) : D        e(y) : D
────────────────────────────────────────── S
            S(c, d, e) : D

3. Computational Rules for Selector S

The computation of selector S is based on pattern matching and case analysis:

Left Branch Computational Rule:

S(inl(a(z)), d, e) = d(λz.a(z)) : D

Right Branch Computational Rule:

S(inr(b(z)), d, e) = e(λz.b(z)) : D

Technical Innovations

1. Special Treatment of Harrop Formulas

• Key Insight: Harrop formulas are computationally irrelevant because they have no computational content
• Technical Implementation: Utilizing Smith's (1993) results, allowing computation of open proof objects containing free variables to normal form, provided these variables range over Harrop formulas

2. Specialization of Hypothetical Judgments

Introducing specialized forms of hypothetical judgments:

z : C ⊢ b(z) : B(z)

where C is restricted to Harrop formulas, interpreted as: b(z) is a program that, upon computation, yields a canonical proof object of type B(z).

3. Design of Reduction Processes

Providing corresponding reduction rules for the S rule:

• S-redL: Handling reduction of left disjunction
• S-redR: Handling reduction of right disjunction

These reduction rules ensure the harmony and local completeness of the rule.

Experimental Setup

Theoretical Verification Framework

This paper primarily conducts theoretical analysis rather than experimental verification, employing the following framework:

1. Base System: Natural deduction system for intuitionistic propositional logic (IPC)
2. Type Theory: Martin-Löf constructive type theory
3. Semantic Framework: BHK interpretation and Curry-Howard correspondence

Verification Methods

1. Constructivity: Proving constructive validity through explicit construction of selector functions
2. Normalization: Verifying system consistency through extension of Smith's (1993) normalization proof
3. Equivalence: Proving equivalence between Split rule and S rule through mutual derivation

Experimental Results

Main Theoretical Results

1. Proof of Constructive Validity

Theorem: The S rule is constructively valid. Proof: Through explicit construction of selector S, which transforms the premises of the S rule into its conclusion.

2. Normalization Theorem

Theorem: Normalization is preserved when the typed S rule is added to Martin-Löf constructive type theory. Proof: Extending Smith's (1993) type-theoretic translation of Kleene-Aczel slash realizability, demonstrating that the system containing the S rule satisfies the normalization property.

3. Equivalence Results

Theorem: The Split rule and S rule are logically equivalent. Proof:

• The Split rule can be derived from the S rule
• The S rule can be derived from the Split rule

Concrete Case Analysis

Case 1: Atomic Formula Case

For the formula (p → (q ∨ r)) → ((p → q) ∨ (p → r)), where p is an atomic formula (hence a Harrop formula), the S rule can successfully prove it.

Case 2: Non-Harrop Formula Case

For the formula ((s ∨ t) → (q ∨ r)) → (((s ∨ t) → q) ∨ ((s ∨ t) → r)), since (s ∨ t) is not a Harrop formula, the S rule cannot be applied, demonstrating the limitations of the rule.

Related Work

Main Related Research

1. Kreisel-Putnam Logic: Originally proposed by Kreisel and Putnam (1957), a logical system stronger than intuitionistic logic while maintaining the disjunction property.
2. Inquisitive Intuitionistic Logic: Work by Punčochář (2016) and Ciardelli et al. (2020), systems obtained by adding the Split rule to intuitionistic logic.
3. Proof-Theoretic Semantics: Dummett-Prawitz style semantics by Prawitz (1971, 1973) and its variants.

Relationship to Related Work

1. Comparison with Condoluci and Manighetti (2018): They investigated the computational perspective of the related Harrop rule using a top-down approach, while this paper employs a bottom-up approach.
2. Relationship to Smith (1993): This paper extends Smith's work on type-theoretic interpretation of Kleene-Aczel slash realizability, particularly regarding computation of open proof objects.

Conclusions and Discussion

Main Conclusions

1. Split Rule Possesses Constructive Validity: Through the mediation of the S rule, the Split rule is constructively valid in the sense of BHK semantics.
2. S Rule Provides Natural Generalization: The S rule, as a disjunction elimination rule, provides a more natural formulation of the Split rule.
3. System Maintains Good Properties: The type system with the added S rule preserves important properties such as normalization.

Limitations

1. Restriction to Harrop Formulas: The S rule can only be applied when C in the premises is a Harrop formula; the system is not closed under uniform substitution.
2. Complexity: The computation of selector S involves handling open proof objects, increasing theoretical complexity.
3. Practicality: The practical applicability of theoretical results requires further exploration.

Future Directions

1. Alternative Generalizations: Exploring another generalization of the Split rule as an implication elimination rule.
2. Extended Applications: Investigating applications of the S rule in other logical systems and computational frameworks.
3. Implementation Verification: Implementing and verifying these theoretical results in concrete proof assistants.

In-Depth Evaluation

Strengths

1. Theoretical Depth: Provides deep proof-theoretic analysis and constructive interpretation of the Split rule.
2. Methodological Innovation: Offers new theoretical perspectives by reformulating the Split rule as the S rule.
3. Technical Rigor: Conducts rigorous formalization within the Martin-Löf type theory framework.
4. Completeness: Not only proves constructive validity but also verifies important properties such as normalization.

Weaknesses

1. Limited Application Scope: The restriction to Harrop formulas may limit practical applications.
2. High Complexity: The computation involving open proof objects increases difficulty in understanding and implementation.
3. Absence of Experimental Verification: Lacks implementation and verification in concrete systems.

Impact

1. Theoretical Contribution: Makes important contributions to the intersection of proof-theoretic semantics and constructive type theory.
2. Methodological Value: Provides a methodological template for studying constructive validity of other logical rules.
3. Foundational Research: Offers new insights into understanding the computational content of intuitionistic logic.

Applicable Scenarios

1. Proof-Theoretic Research: Applicable to studying proof-theoretic properties and computational interpretations of logical rules.
2. Type Theory Development: Can be used to extend and enrich the theoretical foundations of constructive type theory.
3. Logic Programming: May provide new theoretical support for logic programming languages.

References

This paper cites abundant relevant literature, primarily including:

• Kreisel and Putnam's (1957) pioneering work on Kreisel-Putnam logic
• Smith's (1993) type-theoretic interpretation of Kleene-Aczel slash realizability
• Martin-Löf's (1984) foundations of constructive type theory
• Prawitz's (1965, 1971, 1973) work on proof theory and semantics
• Recent research on inquisitive logic (Punčochář 2016, Ciardelli et al. 2020)

This is a high-quality theoretical research paper at the intersection of logic and type theory, providing important theoretical contributions to understanding the constructive content of the Split rule. While possessing certain technical complexity and application limitations, its rigorous theoretical analysis and innovative methodology have significant value for the development of related fields.