Editing Diagonal lemma (section)

==History==
The lemma is called "diagonal" because it bears some resemblance to [[Cantor's diagonal argument]].<ref>See, for example, Gaifman (2006).</ref> The terms "diagonal lemma" or "fixed point" do not appear in [[Kurt Gödel]]'s [[On Formally Undecidable Propositions of Principia Mathematica and Related Systems|1931 article]] or in [[Alfred Tarski]]'s [[The Concept of Truth in Formalized Languages|1936 article]].

In 1934, [[Rudolf Carnap]] was the first to publish the diagonal lemma in some level of generality, which says that for any formula <math>\psi (x)</math> with <math>x</math> as free variable (in a sufficiently expressive language), then there exists a sentence <math>\varphi</math> such that <math>\varphi \leftrightarrow \psi(\ulcorner \varphi \urcorner)</math> is true (in some standard model).<ref>See Carnap, 1934, and Gödel, 1986, p. 363, fn 23.</ref> Carnap's work was phrased in terms of [[Semantic theory of truth|truth]] rather than [[Proof calculus|provability]] (i.e. semantically rather than syntactically).<ref>See Smoryński 2022, Sec. 3.</ref> Remark also that the concept of [[General recursive function|recursive functions]] was not yet developed in 1934.

The diagonal lemma is closely related to [[Kleene's recursion theorem]] in [[computability theory]], and their respective proofs are similar.<ref>See Gaifman, 2006 or Smoryński 2022, Sec. 3.</ref> In 1952, [[Leon Henkin|Léon Henkin]] asked whether sentences that state their own provability are provable. His question led to more general analyses of the diagonal lemma, especially with [[Löb's theorem]] and [[provability logic]].<ref>See Smoryński 2022, Sec. 3.</ref>