Inflationary µ-Calculus via an Infinitary Proof-System: Foundations, Soundness, and Completeness

Abstract

Inflationary fixed-point logic (IFPL) extends modal logic with non-monotonic, in- flationary fixed-point operators, achieving greater expressiveness than the standard µ-calculus. While IFPL can define properties beyond regular languages and classical fixed-point systems, its lack of desirable properties (no finite model property, undecid- ability) and poor algorithmic tractability have relegated it to theoretical obscurity. This thesis bridges a foundational gap by proposing two novel infinitary proof systems: Kω (µ∗) with an ω-rule, and Kω1 (µ∗) with an ω1-rule, to derive deflationary fixed points. We adapt techniques from ω-rule-based µ-calculus systems to handle inflationary semantics, introducing dual approximation rules for fixed points. By restricting to the alternation-free fragment AF-Kω1 (µ∗), we sidestep nested fixed-point complexities while preserving core challenges. We present: (1) Soundness of Kω (µ∗) for finite models and soundness of Kω1 (µ∗) for all models. (2) Completeness of AF-Kω1 (µ∗) through a novel canonical model construction building on saturated sets and relying on truth-set signatures for the model con- struction. Beyond technical contributions, this work serves as an accessible introduction to (inflationary) fixed-point logics, explicitly detailing often-overlooked proofs and intu- itions. While completeness remains partial, the framework lays groundwork for future exploration of tractable IFPL-fragments or circular proof systems. The results suggest that inflationary operators, long dismissed as impractical, may yet find application in, for example, epistemic reasoning when carefully constrained.