Lawvere's fixed-point theorem

In mathematics, Lawvere's fixed-point theorem is an important result in category theory.^[1] It is a broad abstract generalization of many diagonal arguments in mathematics and logic, such as Cantor's diagonal argument, Russel's paradox, Gödel's first incompleteness theorem and Turing's solution to the Entscheidungsproblem.^[2]

It was first proven by William Lawvere in 1969.^[3][4]

Statement

Lawvere's theorem states that, for any Cartesian closed category ${\displaystyle \mathbf {C} }$ and given an object ${\displaystyle B}$ in it, if there is a weakly point-surjective morphism ${\displaystyle f}$ from some object ${\displaystyle A}$ to the exponential object ${\displaystyle B^{A}}$, then every endomorphism ${\displaystyle g:B\rightarrow B}$ has a fixed point. That is, there exists a morphism ${\displaystyle b:1\rightarrow B}$ (where ${\displaystyle 1}$ is a terminal object in ${\displaystyle \mathbf {C} }$ ) such that ${\displaystyle g\circ b=b}$.

Applications

The theorem's contrapositive is particularly useful in proving many results. It states that if there is an object ${\displaystyle B}$ in the category such that there is an endomorphism ${\displaystyle g:B\rightarrow B}$ which has no fixed points, then there is no object ${\displaystyle A}$ with a weakly point-surjective map ${\displaystyle f:A\rightarrow B^{A}}$. Some important corollaries of this are:^[2]

• Cantor's theorem
• Cantor's diagonal argument
• Diagonal lemma
• Russell's paradox
• Gödel's first incompleteness theorem
• Tarski's undefinability theorem
• Turing's proof
• Löb's paradox
• Roger's fixed-point theorem
• Rice's theorem

References