I'm trying to understand the proof sketch of Gödel's Incompleteness Theorem 1 on Wikipedia (https://en.wikipedia.org/wiki/Proof_sketch_for_G%C3%B6del%27s_first_incompleteness_theorem)
In particular, this proof involves the construction of a formula $PF(x,y)$ which holds in case $x$ is the Gödel number of the proof of the statement which has Gödel number $y$. The author says that $PF(x,y)$ is in fact an arithmetical relation, just as $x + y = 6$ is, though a (much) more complicated one" and that the "detailed construction of the formula $PF$ makes essential use of the assumption that the theory is effective."
What would the detailed construction of the formula $PF$ look like?
I understand that one can translate $x$ into its representation as a sequence of arithmetic sentences, and $y$ into its representation as an arithmetic sentence. I assume that assumption that the theory is recursively enumerable implies an effective procedure for checking whether $F(x)$ proves $F(y)$, but how does this imply a formula for $PF(x,y)$? In particular, my understanding is that $PF(x,y)$ must be a finite-length sentence in the language, with $x$ and $y$ as free variables, however, I do not see the way to construct it.
I can imagine (roughly) trying to construct $PF(x,y)$ as the disjunction of all finite sequences of inference rules applied to $F(x)$ but this is not itself finite, even if the set of inference rules is finite.