Knaster–Tarski theorem

In the mathematical areas of order and lattice theory, the Knaster–Tarski theorem, named after Bronisław Knaster and Alfred Tarski, states the following:

Let (L, ≤) be a complete lattice and let f : L → L be an order-preserving (monotonic) function with respect to ≤. Then the set of fixed points of f in L forms a complete lattice under ≤.

It was Tarski who stated the result in its most general form, and so the theorem is often known as Tarski's fixed-point theorem. Some time earlier, Knaster and Tarski established the result for the special case where L is the lattice of subsets of a set, the power set lattice.

The theorem has important applications in formal semantics of programming languages and abstract interpretation, as well as in game theory. It is the logical bedrock for defining the meaning of recursive or repetitive processes in computer science and for proving the existence of equilibrium states in fields like game theory. It essentially proves that when a system follows simple, non-decreasing rules, a stable, self-consistent outcome is always guaranteed to exist.

A kind of converse of this theorem was proved by Anne C. Davis: If every order-preserving function f : L → L on a lattice L has a fixed point, then L is a complete lattice.