Completeness of Cut-Free Kozen Modal Calculus

Definitions and mathematical statement

Let $K$ denote the particular presentation of Kozen's axiomatization of the modal $\mu$-calculus intended by the supplied source, and let $K^{-}$ denote that presentation with its cut rule deleted and its other axioms and inference rules retained. Write $\vdash_{K^{-}}\varphi$ when $\varphi$ has a finite derivation without premises in $K^{-}$.

Under the conventional Kripke interpretation, a model has a nonempty set $S$ of states, a binary accessibility relation $R_a\subseteq S\times S$ for each modal index $a$ in the intended language, and a valuation assigning subsets of $S$ to proposition letters. Fixed-point variables also range over subsets of $S$. The expressions $\mu X.\psi$ and $\nu X.\psi$ denote, respectively, the least and greatest fixed points of the operator on $\mathcal P(S)$ induced by $\psi$; the usual positivity restriction on occurrences of $X$ ensures monotonicity. A formula closed with respect to fixed-point variables is valid if it holds at every state of every such model, for every valuation of its proposition letters.

With completeness understood as completeness for validity under this interpretation, the question is whether \[ \forall\varphi\;\left(\models\varphi\ \Longrightarrow\ \vdash_{K^{-}}\varphi\right), \] where $\varphi$ ranges over all well-formed formulas of the intended language that are closed with respect to fixed-point variables. Equivalently, must every valid formula have a proof in the original presentation using none of its cut rule?

Unresolved qualification. The supplied record does not reproduce the axioms, inference rules, cut rule, or precise language of the intended presentation. It also does not explicitly specify the semantics or whether completeness concerns validity or consequence from assumptions. The displayed formulation expresses the conventional validity reading; these choices require confirmation against the cited source before the statement specifies a unique formal proof-system problem. Completeness of a different cut-free formalism would not by itself answer this question.

Short English statement

Does deleting cut from the particular intended presentation of Kozen's modal $\mu$-calculus axiomatization leave every valid formula provable? The exact presentation and intended meaning of completeness require source confirmation.

Sources

• Supplied local UnsolvedMath registry record, permanent ID $30003659$, title Completeness of Cut-Free Kozen Modal Calculus, source problem code catalogue entry. The record gives proposed year 2017 and supplies no individual proposer attribution.
• Supplied report citation: Mathematical Logic: Proof Theory, Constructive Mathematics (2018), Oberwolfach Reports, pp. 3121--3183, DOI 10.4171/owr/2017/53. https://doi.org/10.4171/owr/2017/53. Also listed in the supplied literature sources as "Oberwolfach Report 53, cut elimination."
• Supplied literature source: Afshari--Leigh, Finitary proof systems for Kozen's mu. https://oa.tib.eu/renate/bitstreams/50824d0c-d5f5-4a10-8518-36ade258b3e3/download.
• Literature assessment dated exactly 2026-08-21: the supplied curation labels the problem open and states that Kozen's original system is complete with cut, that complete cut-free systems exist in other formalisms, and that completeness of the original system after removing cut remains open. This is supplied dated curation derived from the Oberwolfach Reports material, not an independently verified literature assessment; its time-sensitive status and cited claims require independent verification.
• The registry labels the statement corrected_verified, explaining that mathematical content was preserved while notation, typography, and sentence structure were repaired. This supplied editorial label is not independent mathematical verification of this draft.