We develop the theory of illfounded and cyclic proof systems in the context of the modal $\mu$-calculus. A fine analysis of provability and admissibility bridges the finitary, cyclic and illfounded notions of proof for this logic and re-enforces the subtlety of two important normal form theorems: guardedness and disjunctiveness.
翻译:我们针对模态 $\mu$ 演算发展了非良基与循环证明系统的理论。通过对可证明性与可容许性的精细分析,我们在此逻辑的有限性、循环性及非良基性证明概念之间建立了联系,并进一步凸显了两种重要范式定理——守备性与析取性——的微妙之处。