understanding one step of Gödel's theorem

Question

I'm trying to understand this proof of Gödel's theorem: https://mat.iitm.ac.in/home/asingh/public_html/papers/goedel.pdf

At page 3 it says:

Let $B_1(n), B_2(n), ...$ be an enumeration of all formulas having exactly one free variable. Consider the formula $¬P(B_n(n))$. This is one in the above list, say $B_k(n)$.

This is a self-contained statement, where $P(X)$ can be any way of transforming a predicate $X$ into a new predicate $P(X)$. I understand that for all natural number $k$ we can consider the formula $¬P(B_k(n))$ depending on the free variable $n$. So there exists $j$ such that $B_j(n) = ¬P(B_k(n))$. But I don't see why we can suppose $j=k$.

Can you help me explaining that passage?

Answer 1

We don't consider formula $\neg P(B_k(n))$ for all $k$, we consider single formula $\neg P(B_n(n))$ - $n$ is variable in this formula, not just a parameter (it's one of the most important parts in the proof - that we can use a variable as number of formula).

As enumeration was total, there is some $k$ s.t. $\vdash B_k(n) \leftrightarrow \neg P(B_n(n))$ for any $n$. The important part is that $k$ is some constant, the same for all $n$. Then, as $\vdash B_k(n) \leftrightarrow \neg P(B_n(n))$ is true for any $n$, we can substitute $n = k$ and get $\vdash B_k(k) \leftrightarrow \neg P(B_k(k))$.

Answer 2

One thing that looks a bit fishy in the formulation is that $B_n(n)$ apparently uses the letter $n$ both as a variable at the metalevel (so we can speak about formula number $n$) and as an object variable.

What it probably means, given how Gödel's construction generally goes, is $ \neg P( B_n(\bar n))$ where $\bar n$ means the numeral for $n$ -- or in other words $$ \neg P( B_n(\underbrace{SS\cdots S}_n 0)) $$ Then it is hopefully clearer that "$B_n(\underbrace{S\cdots S}_n0)$" is a recipe for constructing a particular sentence once a given $n$ is given. So at the metalevel $\neg P(B_n(\bar n))$ asks whether the sentence we construct is provable. This can be written as an arithmetic formula with $n$ as a free variable, and therefore it appears somewhere in the $B_1, B_2, \ldots, B_k, \ldots$ enumeration. Then we let $k$ be its number