Cyclic Proofs for First-Order Logic with Inductive Definitions
Cyclic Proofs for First-Order Logic with Inductive Definitions
复制标题
具有归纳定义的一阶逻辑的循环证明
DOI：
10.1007/11554554_8
复制
发表时间：
2005
期刊：
影响因子：
--
通讯作者：
J. Brotherston
中科院分区：
文献类型：
--
作者：
J. Brotherston
在具有归纳定义的一阶逻辑的背景下，我们考虑了一种循环的归纳推理方法。我们给出了这种语言的一个证明系统，其中证明被表示为有限的、局部合理的派生树，该树具有标识循环证明部分的“重复函数”。健全是由一个良好的基础条件制定的全球范围内的痕迹证明树，遵循一个想法，由于斯普林格和大坝。然而，与他们的工作相反，我们的证明系统不需要通过序数变量扩展逻辑语法。
我们设置的一个基本问题是，与使用显式归纳规则的非循环证明系统相比，循环证明系统的强度如何。我们证明了循环证明系统包含显式归纳规则的使用。此外，我们提供了处理和分析循环证明的结构的机制，主要是基于它们生成正则无限树，并且还给出了一个充分的(但不是必要的)可靠的有限迹条件，它在计算和组合上比一般的迹条件更简单。
We consider a cyclic approach to inductive reasoning in the setting of first-order logic with inductive definitions. We present a proof system for this language in which proofs are represented as finite, locally sound derivation trees with a “repeat function” identifying cyclic proof sections. Soundness is guaranteed by a well-foundedness condition formulated globally in terms of traces over the proof tree, following an idea due to Sprenger and Dam. However, in contrast to their work, our proof system does not require an extension of logical syntax by ordinal variables.
A fundamental question in our setting is the strength of the cyclic proof system compared to the more familiar use of a non-cyclic proof system using explicit induction rules. We show that the cyclic proof system subsumes the use of explicit induction rules. In addition, we provide machinery for manipulating and analysing the structure of cyclic proofs, based primarily on viewing them as generating regular infinite trees, and also formulate a finitary trace condition sufficient (but not necessary) for soundness, that is computationally and combinatorially simpler than the general trace condition.