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.
翻译:无穷与循环证明系统是用于处理含不动点算子或归纳定义的逻辑公式的证明系统。循环证明系统是相应无穷证明系统的一种限制。因此,这些证明系统通常并不等同,循环系统可能弱于无穷系统。对于若干逻辑,无穷证明系统已被证明具有无切割完备性。然而,循环证明系统在(无切割)完备性或切割消去性质方面仍存在许多未解问题。在本研究中,我们证明:对于某些含不动点算子或归纳定义的命题逻辑,无穷证明系统与循环证明系统的可证性相同,且循环证明系统具有无切割完备性。