Infinitary and cyclic proof systems are proof systems for logical formulas with fixed-point operators or inductive definitions. A cyclic proof system is a restriction of the corresponding infinitary proof system. Hence, these proof systems are generally not the same, as in the cyclic system may be weaker than the infinitary system. For several logics, the infinitary proof systems are shown to be cut-free complete. However, cyclic proof systems are characterized with many unknown problems on the (cut-free) completeness or the cut-elimination property. In this study, we show that the provability of infinitary and cyclic proof systems are the same for some propositional logics with fixed-point operators or inductive definitions and that the cyclic proof systems are cut-free complete.
翻译:无穷与循环证明系统是针对带有不动点算子或归纳定义的逻辑公式的证明系统。循环证明系统是对应无穷证明系统的限制形式。因此,这些证明系统通常并不相同,循环系统可能弱于无穷系统。对于多种逻辑,无穷证明系统已被证明具备无切割完备性。然而,循环证明系统的(无切割)完备性或消去定理性质仍存在许多未解问题。本研究证明,对于某些带有不动点算子或归纳定义的命题逻辑,无穷与循环证明系统的可证性相同,且循环证明系统具备无切割完备性。