发表机构
KU Leuven; Vrije Universiteit Brussel（荷语鲁汶大学; 布鲁塞尔自由大学）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
本文为 FO(ID) 逻辑中的非单调归纳定义形式化了无限下降原理，通过扩展 LKID{\omega} 和 CLKID{\omega} 得到相继式演算 SCFO(ID)-inf 和 SCFO(ID)-cyc，并证明了可靠性、完备性、消割及与 SCFO(ID) 的关系。
AI 中文摘要
归纳定义是数学和计算机科学中一种重要的知识形式。关于归纳定义证明定理的两种常见技术是数学归纳法原理和无限下降原理。为了形式化这些原理，Brotherston 和 Simpson 引入了相继式演算证明系统 LKID（用于数学归纳法）以及 LKID{\omega} 和 CLKID{\omega}（用于无限下降）。LKID{\omega} 是一个无穷系统，其中证明是无限树，而 CLKID{\omega} 是一个循环系统，其中证明是有限图。然而，这些演算仅限于单调定义，而归纳定义通常是非单调的。逻辑 FO(ID) 用非单调归纳定义扩展了经典一阶逻辑。在早期工作中，我们通过将 LKID 扩展为 FO(ID) 的相继式演算 SCFO(ID)，提供了非单调定义下数学归纳法原理的形式化。在本文中，我们通过将 LKID{\omega} 和 CLKID{\omega} 分别扩展为 FO(ID) 的相继式演算 SCFO(ID)-inf 和 SCFO(ID)-cyc，提供了非单调定义下无限下降原理的形式化。此外，我们将 LKID{\omega} 和 CLKID{\omega} 的若干证明论结果（关于可靠性、完备性、消割以及与 SCFO(ID) 的关系）扩展到 SCFO(ID)-inf 和 SCFO(ID)-cyc。
英文摘要
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ω and CLKIDω , for infinite descent. LKIDω is an infinitary system, in which proofs are infinite trees, and CLKIDω 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ω and CLKIDω to sequent calculi SCFO(ID)-inf resp. SCFO(ID)-cyc for FO(ID). Furthermore, we extend several proof-theoretic results for LKIDω and CLKIDω to SCFO(ID)-inf and SCFO(ID)-cyc regarding soundness, completeness, cut-elimination and the relation with SCFO(ID).
Comments44 pages, 4 figures
