Dexter Kozen's paper "Results on the Propositional μ-Calculus" introduces a propositional version of the μ-calculus, a programming logic that includes a least fixpoint operator. The paper provides an exponential-time decision procedure, demonstrates the small model property, and presents a complete deductive system. It also shows that this propositional μ-calculus is strictly more expressive than Propositional Dynamic Logic (PDL). Additionally, the paper offers an algebraic semantics and proves a representation theorem, characterizing countable standard models up to isomorphism. The μ-calculus is defined with primitive propositions, programs, and formulas, including μQ.X, where Q is a variable bound by σ. The syntax and semantics are detailed, and the deductive system is equational, with logical axioms and rules for Boolean algebra, μQ.pQ, and fix-point induction. The paper also discusses the expressive power of the μ-calculus, proving that μQ.[a]Q is not equivalent to any PDL formula, and provides a decision procedure based on a tableau or semantic tree method. Finally, it establishes completeness and a small model property, showing that a consistent formula has a finite tree-like model.Dexter Kozen's paper "Results on the Propositional μ-Calculus" introduces a propositional version of the μ-calculus, a programming logic that includes a least fixpoint operator. The paper provides an exponential-time decision procedure, demonstrates the small model property, and presents a complete deductive system. It also shows that this propositional μ-calculus is strictly more expressive than Propositional Dynamic Logic (PDL). Additionally, the paper offers an algebraic semantics and proves a representation theorem, characterizing countable standard models up to isomorphism. The μ-calculus is defined with primitive propositions, programs, and formulas, including μQ.X, where Q is a variable bound by σ. The syntax and semantics are detailed, and the deductive system is equational, with logical axioms and rules for Boolean algebra, μQ.pQ, and fix-point induction. The paper also discusses the expressive power of the μ-calculus, proving that μQ.[a]Q is not equivalent to any PDL formula, and provides a decision procedure based on a tableau or semantic tree method. Finally, it establishes completeness and a small model property, showing that a consistent formula has a finite tree-like model.