Lawvere's fixed-point theorem

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}$.

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}$ that 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