For any monotone function in a complete lattice, one can obtain its least fixed-point by finding the limit of the approximation sequence obtained by starting with the minimal element and iteratively substituting the result of the function to be its input. However if we start with an arbitrary element, or the function is not monotone, then the approximation sequence sometimes oscillates instead of converging. We study the (iterative) substitution over basic modal logic, characterizing its power and applying it to analyze oscillations.
