The paper presents a propositional version of the μ-calculus, which is strictly more expressive than PDL. It defines an exponential-time decision procedure, a small model property, and a complete deductive system. The system, denoted Lμ, encodes PDL with tests and looping but without reverse. It is shown that Lμ is strictly more expressive than PDL, and that filtration techniques fail for Lμ. The paper also provides an algebraic semantics and proves a representation theorem. The system Lμ is defined with a least fixpoint formulation, and it is shown that it can encode PDL with tests and looping but not the reverse operator. The paper also presents a deductive system for Lμ, including the fixed point induction rule of Park, and proves completeness. The paper also describes an algorithm for refuting formulas in Lμ, which uses a tableau method and alternating Turing machines. The algorithm is shown to have exponential time complexity and uses O(|W|³) space. The paper also proves that the algorithm is equivalent to the existence of a finite tree-like model of a certain size. The paper concludes with an algebraic semantics and a representation theorem for the μ-calculus.The paper presents a propositional version of the μ-calculus, which is strictly more expressive than PDL. It defines an exponential-time decision procedure, a small model property, and a complete deductive system. The system, denoted Lμ, encodes PDL with tests and looping but without reverse. It is shown that Lμ is strictly more expressive than PDL, and that filtration techniques fail for Lμ. The paper also provides an algebraic semantics and proves a representation theorem. The system Lμ is defined with a least fixpoint formulation, and it is shown that it can encode PDL with tests and looping but not the reverse operator. The paper also presents a deductive system for Lμ, including the fixed point induction rule of Park, and proves completeness. The paper also describes an algorithm for refuting formulas in Lμ, which uses a tableau method and alternating Turing machines. The algorithm is shown to have exponential time complexity and uses O(|W|³) space. The paper also proves that the algorithm is equivalent to the existence of a finite tree-like model of a certain size. The paper concludes with an algebraic semantics and a representation theorem for the μ-calculus.