论文标题
一阶逻辑与自我参考
First-order logic with self-reference
论文作者
论文摘要
我们考虑使用递归运算符的一阶逻辑扩展，该递归操作员对应于允许公式引用自己。我们研究了在两个不同语义系统下获得的语言，从而获得了两种密切相关但不同的逻辑。我们为这两种逻辑提供了一个自然扣除系统，该系统既适合有效性，又可以调查一系列相关的基本决策问题。例如，逻辑的两变量片段的有效性问题显示为conexime-Complete，这与固定点最少的两种可变量逻辑的高度不可证明的性质形成鲜明对比。我们还主张研究了递归和自我参考方法的自然性和利益，例如将新逻辑与Lindstrom的第二个定理联系起来。
We consider an extension of first-order logic with a recursion operator that corresponds to allowing formulas to refer to themselves. We investigate the obtained language under two different systems of semantics, thereby obtaining two closely related but different logics. We provide a natural deduction system that is complete for validities for both of these logics, and we also investigate a range of related basic decision problems. For example, the validity problems of the two-variable fragments of the logics are shown coNexpTime-complete, which is in stark contrast with the high undecidability of two-variable logic extended with least fixed points. We also argue for the naturalness and benefits of the investigated approach to recursion and self-reference by, for example, relating the new logics to Lindstrom's Second Theorem.
