2025-11-17T09:43:13.266953

Constructive validity of a generalized Kreisel-Putnam rule

Pezlar

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.

academic

Constructive validity of a generalized Kreisel-Putnam rule

基本信息

论文ID: 2311.15376
标题: Constructive validity of a generalized Kreisel-Putnam rule
作者: Ivo Pezlar (Czech Academy of Sciences, Institute of Philosophy)
分类: cs.LO (Computer Science - Logic in Computer Science), math.LO (Mathematics - Logic)
发表时间: 2023年11月28日 (arXiv v2)
论文链接: https://arxiv.org/abs/2311.15376

摘要

本文提出了广义Kreisel-Putnam规则（也称为广义Harrop规则或Split规则）的计算解释，采用BHK语义学风格。通过利用公式与类型之间的Curry-Howard对应关系来实现这一目标。首先检查Split规则在直觉主义命题逻辑自然演绎系统中的推理行为，这将指导我们制定适当的程序来捕获类型化Split规则的相应计算内容。换句话说，我们希望通过考虑其类型化变体来找到Split规则的适当选择子函数。我们的研究也可以重新表述为回答以下问题：Split规则在BHK语义学意义下是否具有构造性有效性？我们对Split规则及其新提出的广义版本（称为S规则）给出了肯定的答案。

研究背景与动机

核心问题

本文要解决的核心问题是：Split规则是否在BHK语义学意义下具有构造性有效性？ 具体来说，就是寻找一个构造性函数，能够将Split规则前提的任意证明转换为其结论的证明。

问题重要性

理论意义: Kreisel-Putnam规则是一个在直觉主义逻辑中可容许但不可推导的规则，尽管在Dummett-Prawitz风格语义学的变体中是证明论有效的。
逻辑系统特性: 当将Split规则添加到直觉主义逻辑时，得到的系统（如询问直觉主义逻辑）既保持析取性质又具有结构完全性，这是经典逻辑的特性。
广泛应用: Split规则出现在领域逻辑等多个领域中，显示了其基础重要性。

现有方法局限性

缺乏计算解释: 尽管Split规则具有重要意义，但其证明论意义和计算内容大多未被探索。
构造性有效性未明: 没有明确的构造性函数来解释Split规则的计算内容。

研究动机

通过Curry-Howard对应关系，将公式视为类型，寻找适当的选择子函数来捕获Split规则的计算内容，从而确立其构造性有效性。

核心贡献

提出了S规则: 将Split规则重新表述为析取消除式规则的广义形式，称为S规则。
建立了构造性有效性: 为S规则找到了有效的选择子函数S，证明了其构造性有效性。
提供了计算解释: 通过类型化变体和计算规则，给出了Split规则的完整计算解释。
证明了规范化性质: 证明了在Martin-Löf构造类型论中添加类型化S规则后仍保持规范化。
建立了规则等价性: 证明了Split规则与S规则的等价性，并提供了相应的约简过程。

方法详解

任务定义

输入: Split规则的前提 C → (A ∨ B)，其中C是Harrop公式输出: Split规则的结论 (C → A) ∨ (C → B)约束: 寻找构造性函数实现从前提到结论的转换

核心方法架构

1. 规则重新表述

将原始Split规则：

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

重新表述为S规则（析取消除式）：

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

2. 类型化S规则

在Martin-Löf构造类型论框架下，S规则的类型化形式为：

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