A Survey on Lawvere's Fixed-Point Theorem

Abstract

Lawvere's fixed-point theorem organizes self-reference around a representation hypothesis and a diagonal calculation. This survey develops its set-theoretic, finite-product, and cartesian closed formulations while distinguishing representation on points from equality of whole morphisms. Detailed applications include Cantor's theorem, arithmetic diagonalization, a truth-schema obstruction, an incompleteness consequence with explicit assumptions, the halting problem, and Kleene's recursion theorem. A powerset dcpo supplies a nontrivial positive representation of continuous maps and illustrates the difference between fixed-point existence, a uniform operator, and a least fixed point. Further sections compare parameterized recursion and trace, substructural and relational generalizations, constructive witness data, and topological variants. Throughout, the relevant maps, equality relations, and additional hypotheses are kept explicit. Worked examples use finite tables, Boolean equations, numerical function codes, factorial approximations, and self-output programs. The survey is intended for readers beginning category theory who wish to understand both the common diagonal mechanism and the work required in its applications.