非単調な帰納的定義のための無限・循環シーケント計算
An Infinitary and a Cyclic Sequent Calculus for Non-Monotone Inductive Definitions
この論文をやさしく読む
ひとことで言うと
非単調な帰納的定義について、無限に続く証明と循環する有限の証明を扱う形式体系を拡張した研究。
何に役立つ？
プログラム検証や形式論理で、非単調な定義を含む主張の証明規則を分析するための理論的な基盤になる。
この研究の面白いところ
既存の単調な定義向けの無限・循環シーケント計算をFO(ID)へ広げ、健全性や完全性などの証明論的性質も扱っている。
どこまで分かった？
要旨が述べるのは形式体系とその証明論的結果である。実際の検証ツールでの速度や適用事例は示されていない。
v1のアブストラクトに基づくAI解説。日本語訳とは別に、用途の解釈を含みます。
アブストラクトの日本語訳
帰納的定義は数学と計算機科学で重要な知識の形式である。これについて定理を証明する一般的な二つの方法が、数学的帰納法と無限降下法である。これらを形式化するため、BrotherstonとSimpsonは、数学的帰納法のためのシーケント計算LKIDと、無限降下法のためのLKIDωおよびCLKIDωを導入した。LKIDωは証明が無限の木となる無限的な体系であり、CLKIDωは証明が有限のグラフとなる循環的な体系である。ただし、これらの計算は単調な定義に限定されるのに対し、帰納的定義は一般には非単調である。論理FO(ID)は、古典的な一階論理を非単調な帰納的定義で拡張する。 著者らは以前、LKIDをFO(ID)のためのシーケント計算SCFO(ID)へ拡張することで、非単調な定義に対する数学的帰納法の原理を形式化した。本論文ではLKIDωとCLKIDωをそれぞれFO(ID)のためのSCFO(ID)-infとSCFO(ID)-cycへ拡張し、非単調な定義に対する無限降下法の原理を形式化する。さらに、健全性、完全性、カット除去、およびSCFO(ID)との関係について、LKIDωとCLKIDωの複数の証明論的結果をSCFO(ID)-infとSCFO(ID)-cycへ拡張する。
v1の要旨から自動生成。本文の精読・人による確認は未実施。
- 初稿
- 2026-09-22（UTC）
- 最新改訂
- 2026-09-22 · v1
- 査読・掲載
- 査読状況未確認
更新履歴
- v1 2026-09-22 この版を読む
取得できた版を表示。版の更新は査読済みを意味しません。過去版の本文差分は未解析です。
原文の要旨
Inductive definitions are an important form of knowledge in mathematics and computer science. Two common techniques to prove theorems about inductive definitions are the principle of mathematical induction and the principle of infinite descent. To formalize these principles, Brotherston and Simpson introduced the sequent calculus proof systems LKID, for mathematical induction, and LKID{\omega} and CLKID{\omega} , for infinite descent. LKID{\omega} is an infinitary system, in which proofs are infinite trees, and CLKID{\omega} a cyclic system, in which proofs are finite graphs. However, these calculi restrict to monotone definitions, while inductive definitions are generally non-monotone. The logic FO(ID) extends classical first-order logic with non-monotone inductive definitions. In earlier work, we provided a formalization of the principle of mathematical induction for non-monotone definitions by extending LKID to a sequent calculus SCFO(ID) for FO(ID). In this paper, we provide a formalization of the principle of infinite descent for non-monotone definitions by extending LKID{\omega} and CLKID{\omega} to sequent calculi SCFO(ID)-inf resp. SCFO(ID)-cyc for FO(ID). Furthermore, we extend several proof-theoretic results for LKID{\omega} and CLKID{\omega} to SCFO(ID)-inf and SCFO(ID)-cyc regarding soundness, completeness, cut-elimination and the relation with SCFO(ID).
著者のコメント
44 pages, 4 figures
arXiv ID: 2609.26337 ／ 要約の誤りについて