 The proof of this fact relies explicitly on the representability of the relation \(\mathsf{Proof}_{\mathsf{P}}(x,y)\) in \(\mathsf{P}\) which in turn derives from its primitive recursiveness. But the techniques on which Gödel’s proof relies also contributed to the subsequent development of computability theory in several additional ways. First, it follows from the possibility of Gödel numbering the formulas of \(\mathsf{P}\) that we may also effectively enumerate them as \(\varphi_0(x), \varphi_1(x), \varphi_2(x), \ldots\)—e.g., in increasing order of \(\ulcorner \varphi_i \urcorner\). This provides a mechanism for referring to formulas via their indices which in turn served as an important precedent for Kleene’s (1936a) use of a similar indexation of general recursive definitions in his proof of the Normal Form Theorem (see  Section 2.2.2).  Second, the proof of the Diagonal Lemma also demonstrates how it is possible to formalize the substitution of terms for free variables in a manner which may be understood to yield an effective form of Cantor’s diagonal argument  (see the entry on self-reference).  This technique served as an important precedent for the use of diagonalization in results such as the undecidability of the Halting Problem (Turing 1937, see  Section 3.2),  the Recursion Theorem (Kleene 1938, see  Section 3.4),  and the Hierarchy Theorem (Kleene 1943, see  Section 3.6). 