Strong-Induction Admissibility in Cut-Free Modal Calculus

Definitions and mathematical statement

The modal $\mu$-calculus extends modal logic with least and greatest fixed-point formulas $\mu X.\varphi$ and $\nu X.\varphi$, where the bound variable $X$ occurs positively in $\varphi$, ensuring monotonicity of the associated operator.

Let $K_{\mathrm{cf}}$ denote the system called "Kozen's cut-free system" in the supplied record, and write $K_{\mathrm{cf}}\vdash S$ when the sequent $S$ has a derivation in that system. For an inference rule $R$, admissibility in $K_{\mathrm{cf}}$ means that, for every instance of $R$ with premises $(S_i)_{i\in I}$ and conclusion $S$, including every side condition of that instance, \[ \left(\forall i\in I,\ K_{\mathrm{cf}}\vdash S_i\right) \quad\Longrightarrow\quad K_{\mathrm{cf}}\vdash S. \] Here admissibility concerns derivability of the conclusion from the existence of derivations of all premises; it does not assert that the rule is a primitive inference of the system.

Problem. Is the strong-induction rule referred to in the supplied source admissible in $K_{\mathrm{cf}}$? The record presents admissibility of a corresponding quantifier-contraction inference as an equivalent formulation.

Unresolved specification. The supplied record does not give the axioms and inference rules of $K_{\mathrm{cf}}$, the strong-induction rule, or the corresponding quantifier-contraction inference. In particular, their premises, conclusions, substitution conventions, and side conditions are absent. Consequently, the displayed condition gives the precise meaning of admissibility, but the intended rule instances cannot be specified from this record alone. The asserted equivalence of the two formulations is retained as a source claim requiring verification.

Short English statement

Does every instance of the source's strong-induction rule whose premises are derivable in Kozen's cut-free modal $\mu$-calculus also have a derivable conclusion? The source states an equivalent question about quantifier contraction, but supplies neither inference explicitly. This statement-only draft therefore requires source consultation and human mathematical review.

Sources

• Supplied local problem-registry record: permanent UnsolvedMath ID $30003660$; exact source problem code catalogue entry; collection: Oberwolfach Reports Open Problems. No individual proposer is recorded; the proposed year is $2017$.
• Supplied report citation: Mathematical Logic: Proof Theory, Constructive Mathematics (2018), Oberwolfach Reports, pp. 3121--3183, DOI 10.4171/owr/2017/53. Source URL: https://doi.org/10.4171/owr/2017/53. The supplied literature-source label for this same link is "Oberwolfach Report 53, cut elimination."
• Supplied literature reference: 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, identifies strong-induction admissibility with an unresolved completeness question for Kozen's cut-free system, and states that current cut-free results use strengthened or alternative systems. These are supplied dated curation claims, not independently verified findings. The background expressly requests independent verification of time-sensitive status and cited claims.
• The registry labels the statement corrected_verified and explains that notation, typography, and sentence structure were repaired while mathematical content was preserved. This records the supplied editorial assessment; it does not establish mathematical verification of this draft or of the asserted equivalences.