arxiv: 2604.23273 · v1 · submitted 2026-04-25 · 💻 cs.LO · math.LO

Recognition: unknown

The Constructive μ-calculus: Game Semantics and Non-Wellfounded Proof Systems

Leonardo Pacheco

Authors on Pith no claims yet

Pith reviewed 2026-05-08 06:55 UTC · model grok-4.3

classification 💻 cs.LO math.LO

keywords constructive mu-calculusgame semanticsnon-wellfounded proof systemsbirelational Kripke semanticssoundness and completenessconstructive modal logicfixed-point operatorsmodal mu-calculus

0 comments

The pith

Game semantics for the constructive mu-calculus is equivalent to birelational Kripke semantics and supports a sound, complete fully-labeled non-wellfounded proof system.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper defines game semantics for the constructive mu-calculus, a fixed-point extension of constructive modal logic CK, and proves that these games match the birelational Kripke semantics. It then applies the game semantics to establish that a fully-labeled non-wellfounded proof system is sound and complete for the logic. The work closes by sketching how the same techniques adapt to mu-calculi over other non-classical modal bases. A reader would care because the result supplies both an intuitive operational account of the logic and a usable proof system for reasoning with recursive modalities in constructive settings.

Core claim

We define game semantics for the constructive μ-calculus and prove its equivalence to the birelational Kripke semantics. We then use the game semantics to prove the soundness and completeness of a fully-labeled non-wellfounded proof system for it.

What carries the argument

The game semantics, consisting of two-player games played on formulas and models whose winning strategies correspond exactly to satisfaction in birelational Kripke structures.

If this is right

The fully-labeled non-wellfounded proof system is sound and complete for validity in the constructive mu-calculus.
Proofs in the system can be read as strategies in the corresponding games.
The same game-based argument can be reused to obtain soundness and completeness results for mu-calculi over other non-classical modal logics.
Infinite branches in proofs correspond to infinite plays in the games.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

The equivalence makes it possible to transfer decidability or complexity results between the game and proof-system presentations.
Non-wellfounded proofs may serve as a basis for automated theorem-proving tools that search for cyclic derivations in constructive modal settings.
The games supply an operational reading of fixed points that could be used to define model-checking algorithms directly on constructive models.

Load-bearing premise

The birelational Kripke semantics is the intended meaning of the constructive mu-calculus and the games are defined so that their equivalence to it holds without extra constraints on models or formulas.

What would settle it

A concrete formula of the constructive mu-calculus together with a model in which one player has a winning strategy in the associated game yet the formula fails to hold under the birelational Kripke satisfaction relation, or vice versa.

read the original abstract

We study a variant of the modal $\mu$-calculus based on the constructive modal logic $\mathsf{CK}$. We define game semantics for the constructive $\mu$-calculus and prove its equivalence to the birelational Kripke semantics. We then use the game semantics to prove the soundness and completeness of a fully-labeled non-wellfounded proof system for it. At last, we briefly describe how to adapt the game semantics and proof system to the $\mu$-calculus over other non-classical modal logics.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

The paper works out game semantics for the constructive μ-calculus over CK, proves equivalence to birelational Kripke models, and derives soundness plus completeness for a fully-labeled non-wellfounded proof system from that equivalence.

read the letter

The core contribution is the adaptation of game semantics to the constructive setting and the use of those games to justify the proof system. Pacheco defines the games so that infinite plays respect parity conditions for the fixed points while the modal moves respect the constructive rules of CK. The equivalence to the birelational Kripke semantics then lets him transfer the usual strategy-composition arguments to obtain soundness and completeness for the non-wellfounded system without having to reason directly on the models for every rule. That is the part that is new relative to the classical μ-calculus literature. The fully-labeled format of the proof system is also a deliberate choice that makes the correspondence with game positions straightforward. The paper does this cleanly and follows the standard pattern for these results without introducing hidden constraints on the models or on how fixed points unfold. The brief closing section on other non-classical modal logics is only sketched, so it remains to be seen how much extra work the adaptation requires in each case, but that is a minor point rather than a load-bearing gap. The central claims rest on explicit definitions and the equivalence proof, so there is no circularity or fitting presented as prediction. This is for people already working on constructive modal logics, fixed-point proof systems, or verification tools that need constructive soundness. A reader in those areas will get a usable bridge between semantics and proof rules. The work is grounded enough to deserve a serious referee even if some details of the other-logics adaptation need expansion.

Referee Report

0 major / 3 minor

Summary. The paper defines game semantics for the constructive μ-calculus (based on the constructive modal logic CK) and proves its equivalence to the standard birelational Kripke semantics. It then leverages the game semantics to establish soundness and completeness of a fully-labeled non-wellfounded proof system, and sketches how the approach adapts to the μ-calculus over other non-classical modal logics.

Significance. If the equivalence and derived proof-theoretic results hold, the work is significant for extending game semantics and non-wellfounded proof systems to constructive fixed-point modal logics, an area with limited prior treatment. The use of game semantics as an intermediary to obtain soundness/completeness is a standard but effective technique here, and the adaptation section indicates potential generality beyond CK.

minor comments (3)

The abstract uses the phrasing 'At last' which is slightly informal; consider 'Finally' for consistency with the rest of the manuscript.
Ensure that all notation for game positions, parity conditions, and fixed-point unfoldings is introduced with explicit definitions before first use in the main body.
If the paper includes any diagrams of game arenas or proof trees, verify that labels and arrows are legible and that the caption fully explains the correspondence to the formal definitions.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for the positive evaluation of our manuscript and the recommendation for minor revision. The referee correctly summarizes the main contributions: the definition of game semantics for the constructive μ-calculus, its equivalence to birelational Kripke semantics, the use of this to establish soundness and completeness for the non-wellfounded proof system, and the sketch of adaptations to other logics. We will make minor revisions to the manuscript to improve its quality.

Circularity Check

0 steps flagged

No significant circularity detected

full rationale

The paper defines game semantics for the constructive μ-calculus independently of the target results, proves equivalence to birelational Kripke semantics via explicit constructions and standard strategy-based arguments for fixed points, and then derives soundness/completeness of the non-wellfounded proof system from that equivalence. No step reduces by construction to its inputs, no parameters are fitted and relabeled as predictions, and no load-bearing self-citations or uniqueness theorems imported from the authors' prior work are present. The derivation chain is self-contained with independent mathematical content at each stage.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The work rests on the standard background of constructive modal logic CK and the usual definitions of game semantics and non-wellfounded proofs; no free parameters or invented entities are introduced in the abstract.

axioms (1)

domain assumption Birelational Kripke semantics correctly interprets the constructive modal logic CK
Invoked as the target semantics to which game semantics is shown equivalent.

pith-pipeline@v0.9.0 · 5373 in / 1251 out tokens · 52897 ms · 2026-05-08T06:55:04.571185+00:00 · methodology

discussion (0)

Reference graph

Works this paper leans on

14 extracted references · 12 canonical work pages

[1]

[AGLZ24] Bahareh Afshari, Lide Grotenhuis, Graham E

URL: https://doi.org/10.1007/978-3-031-43513-3_13, doi:10.1007/978-3-031-43513-3\_13. [AGLZ24] Bahareh Afshari, Lide Grotenhuis, Graham E. Leigh, and Lukas Zenger. Intuitionistic master modality. InAdvances in modal logic. Vol. 15, pages 19–39. Coll. Publ.,

work page doi:10.1007/978-3-031-43513-3_13
[2]

Leigh, and Guillermo Men ´endez Tu- rata

[ALM24] Bahareh Afshari, Graham E. Leigh, and Guillermo Men ´endez Tu- rata. Demystifyingµ. Preprint, 2024.arXiv:2401.01096. [AN01] Andr ´e Arnold and Damian Niwi ´nski.Rudiments ofµ-Calculus. Number v. 146 in Studies in Logic and the Foundations of Mathe- matics. Elsevier, 1st edition,

work page arXiv 2024
[3]

Intuitionistic linear temporal logics

[BBDFD19] Philippe Balbiani, Joseph Boudou, Mart ´ın Di´eguez, and David Fern´andez-Duque. Intuitionistic linear temporal logics. 21(2), De- cember 2019.doi:10.1145/3365833. [BDFD21] Philippe Balbiani, Martin Dieguez, and David Fern ´andez-Duque. Some constructive variants of S4 with the finite model property. In 2021 36th Annual ACM/IEEE Symposium on Log...

work page doi:10.1145/3365833 2019
[4]

[BzDs84] Milan Boˇ zi ´c and Kosta Doˇ sen

Springer International Publishing, 2018.doi:10.1007/ 978-3-319-10575-8\_26. [BzDs84] Milan Boˇ zi ´c and Kosta Doˇ sen. Models for normal intuitionistic modal logics.Studia Logica, 43(3):217–245, 1984.doi:10.1007/ BF02429840. [CMRR13] Xavier Caicedo, George Metcalfe, Ricardo Rodr ´ıguez, and Jonas Rogger. A finite model property for G ¨odel modal logics. ...

work page doi:10.1007/978-3-642-39992-3 2018
[5]

Methods Comput

URL:https://lmcs.episciences.org/ 3280,doi:10.23638/LMCS-14(3:3)2018. [Fit48] Frederic B. Fitch. Intuitionistic modal logic with quantifiers.Por- tugaliae Mathematicae, 7:113–118, 1948.doi:10.2307/2269276. [FS78] Gis `ele Fischer Servi. The finite model property for MIPQ and some consequences.Notre Dame Journal of Formal Logic, XIX(4):687–692, 1978.doi:10...

work page doi:10.23638/lmcs-14(3:3)2018 2018
[6]

URL:https:// doi.org/10.1007/978-3-031-62687-6_4,doi:10.1007/ 978-3-031-62687-6\_4

©2024. URL:https:// doi.org/10.1007/978-3-031-62687-6_4,doi:10.1007/ 978-3-031-62687-6\_4. [GO26] Han Gao and Nicola Olivetti. Constructive modal logics: bi- nested calculi and bi-relational countermodels. InLogic, language, information, and computation, volume 15942 ofLecture Notes in Comput. Sci., pages 211–227. Springer, Cham,

work page doi:10.1007/978-3-031-62687-6_4 2024
[7]

URL: https://doi.org/10.1007/978-3-031-99536-1_13, doi:10.1007/978-3-031-99536-1\_13

©2026. URL: https://doi.org/10.1007/978-3-031-99536-1_13, doi:10.1007/978-3-031-99536-1\_13. [GTW03] Erich Gr ¨adel, Wolfgang Thomas, and Thomas Wilke.Automata, logics, and infinite games: a guide to current research, volume

work page doi:10.1007/978-3-031-99536-1_13 2026
[8]

Aggarwal, Y

[JM16] Gerhard J ¨ager and Michel Marti. Intuitionistic common knowl- edge or belief.J. Appl. Log., 18:150–163, 2016.doi:10.1016/j. jal.2016.04.004. [KM16] Leszek Aleksander Kołodziejczyk and Henryk Michalewski. How unprovable is Rabin’s decidability theorem? InProceedings of the 31st Annual ACM-IEEE Symposium on Logic in Computer Sci- ence (LICS 2016), page

work page doi:10.1016/j 2016
[9]

Filiot, O

ACM, New York, 2016.doi:10.1145/ 2933575.2934543. [Koz83] Dexter Kozen. Results on the propositionalµ-calculus.The- oretical Computer Science, 27(3):333–354, 1983.doi:10.1016/ 0304-3975(82)90125-6. [Len10] Giacomo Lenzi. Recent results on the modalµ-calculus: A sur- vey.Rendiconti dell’Istituto di Matematica dell’Universit` a di Trieste, 42:235–255,

work page arXiv 2016
[10]

Constructive CK for con- texts.Context Representation and Reasoning (CRR-2005), 13,

[MdP05] Michael Mendler and Valeria de Paiva. Constructive CK for con- texts.Context Representation and Reasoning (CRR-2005), 13,

2005
[11]

A fully labelled proof system for intuitionistic modal logics.J

[MMSb21] Sonia Marin, Marianela Morales, and Lutz Straß burger. A fully labelled proof system for intuitionistic modal logics.J. Logic Com- put., 31(3):998–1022, 2021.doi:10.1093/logcom/exab020. [Nis82] Hirokazu Nishimura. Semantical analysis of constructive PDL. Publications of the Research Institute for Mathematical Sciences, 18(2):847–858,

work page doi:10.1093/logcom/exab020 2021
[12]

Games for theµ- calculus.Theoret

[NW96] Damian Niwi ´nski and Igor Walukiewicz. Games for theµ- calculus.Theoret. Comput. Sci., 163(1-2):99–116, 1996.doi:10. 1016/0304-3975(95)00136-0. [Ono77] Hiroakira Ono. On some intuitionistic modal logics.Publications of the Research Institute for Mathematical Sciences, 13(3):687–722,

1996
[13]

[Pac24] Leonardo Pacheco

doi:10.2977/prims/1195189604. [Pac24] Leonardo Pacheco. Collapsing constructive and intuitionistic modal logics. Preprint, 2024.arXiv:2408.16428. 17 [Pra65] Dag Prawitz.Natural Deduction: A Proof-Theoretical Study

work page doi:10.2977/prims/1195189604 2024
[14]

[Stu08] Thomas Studer

URL: https://era.ed.ac.uk/handle/1842/407. [Stu08] Thomas Studer. On the proof theory of the modal mu- calculus.Studia Logica, 89(3):343–363, 2008.doi:10.1007/ s11225-008-9133-6. [Wal95] Igor Walukiewicz. Completeness of Kozen’s axiomatisation of the propositionalµ-calculus. InProceedings of Tenth Annual IEEE Symposium on Logic in Computer Science, pages ...

work page doi:10.1109/lics.1995.523240 2008