一句话：为模态 μ-演算给出两个有限无割矢列演算，并由此构造性地证明 Kozen 公理系统的完备性。
本文研究模态 μ-演算的证明论，目标是给出无割且有限的矢列演算，并重新建立 Kozen 公理系统的完备性。作者提出两个演算：其一将 Kozen 公理系统中的 cut 替换为对最大不动点归纳规则的强化；其二采用 Stirling 带名字的表列证明系统风格，推导带标注的矢列，并推广 ν-再生规则以允许释放开放假设。完备性与可靠性通过一系列证明系统之间的嵌入来证明：从 Stirling 的表列证明出发，逐步嵌入到 Kozen 的原始公理系统。作为推论，得到 Kozen 公理化完备性的新构造性证明，避免通常经由自动机与博弈的绕道。
We present two finitary cut-free sequent calculi for the modal μ-calculus. One is a variant of Kozen's axiomatisation in which cut is replaced by a strengthening of the induction rule for greatest fixed point. The second calculus derives annotated sequents in the style of Stirling's `tableau proof system with names' (2014) and features a generalisation of the ν-regeneration rule that allows discharging open assumptions. Soundness and completeness for the two calculi is proved by establishing a sequence of embeddings between proof systems, starting at Stirling's tableau-proofs and ending at the original axiomatisation of the μ-calculus due to Kozen. As a corollary we obtain a new, constructive, proof of completeness for Kozen's axiomatisation which avoids the usual detour through automata and games.