Gödel's Incompleteness Theorem - Diagonal Lemma In proving Gödel's incompleteness theorem, why does he needed the Diagonal Lemma or the Fixed Point Theorem for building a formula $\phi$ that spoke about itself? Can't this formula be built this way:
Diagonal Function. Let $D(x, y)$ be the diagonal function, such that $D$ returns the result obtained by replacing the formula with Gödel number $y$ for all free occurrences of $a$ in the formula with Gödel number $x$.
Example. Let $\psi(a)$ be a formula that affirms that some formula with the Gödel number of $a$ is closed (has no free variables) and $k$ be it's Gödel number. Using Diagonal Function to construct a formula, by applying $D(k, k) = j$, the Gödel number $j$ will already be the Gödel number of a formula affirming that the formula itself has no free variables. I mean, $\ulcorner \psi(\ulcorner \psi(a) \urcorner) \urcorner = j$, or $\ulcorner \psi(\overline{k}) \urcorner = j$.
What i am missing here?
 A: If I understand your notation correctly, the formula (whose Gödel number is) $j$ does not assert that $j$ itself has no free variables, merely that $\psi(a)$ (which is different from $j$ itself) has no free variables. Which, incidentally, is false because it has $a$ as a free variable.
A: There are two questions: 


*

*Why does Gödel's proof needs the Diagonalization Lemma"

*Could the diagonal function be defined as suggested? 


My answer to 1 is twofold: Some proofs of Gödel's First Incompleteness Theorem do not use the Diagonalization Lemma (like the one suggested by Turing in his celebrated and seminal article) and a proof by Kripke reported in the following article: 
Hilary Putnam: Nonstandards models and Kripke's proof of the Gödel Theorem, Notre Dame Journal of Formal Logic, Volume 41, Number 1, pages 53-58, 2000
Thew following might help understand Gödel's proof and thus better answer the first question: 
The "diagonal lemma" (also called "diagonalization lemma", "self-referential lemma” and “fixed-point lemma”) is a generalization (see below (Carnap 1934)) of Gödel's argument. Gödel attributed that generalization to Carnap in the references (Gödel 1934) and (Gödel 1986) given below. Gödel proved the special case of that lemma where the unary relation is "not Bew(x)". 
R. Carnap: Logische Syntax der Sprache, Vienna: Julius Springer, 1934
K. Gödel: On Undecidable Propositions of Formal Mathematical Systems, lecture notes taken by S. Kleene and J. Rosser, 1934
K. Gödel: Review of Carnap 1934, in: Gödel: Collected Works I. Publications 1929–1936, S. Feferman et al. editors, Oxford University Press, 1986 p. 389
