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

一般化Kreisel-Putnam規則の構成的妥当性

基本情報

論文ID: 2311.15376
タイトル: Constructive validity of a generalized Kreisel-Putnam rule
著者: Ivo Pezlar（チェコ科学アカデミー哲学研究所）
分類: cs.LO（コンピュータサイエンス - コンピュータ科学における論理）、math.LO（数学 - 論理）
発表日時: 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