 Finally we mention still alternative logics to reason about programs, viz. fixpoint logics, with as typical example the so-called \(\mu\)-calculus, dating back to Scott and de Bakker (1969), and further developed in Hitchcock and Park 1972, Park 1976, de Bakker 1980, and Meyer 1985. The basic operator is the least fixed point operator \(\mu\), capturing iteration and recursion: if \(\phi(X)\) is a logical expression with a free relation variable \(X\), then the expression \(\mu X\phi(X)\) represents the least \(X\) such that \(\phi(X) = X\), if such an \(X\) exists. A propositional version of the \(\mu\)-calculus, called propositional or modal \(\mu\)-calculus comprising the propositional constructs \(\rightarrow\) and false, together with the atomic (action) modality [\(a\)] and \(\mu\) operator is completely axiomatized by propositional modal logic plus the axiom \(\phi[X/\mu X\phi] \rightarrow \mu X\phi\), where \(\phi[X/Y\)] stands for the expression \(\phi\) in which \(X\) is substituted by \(Y\), and rule