Show there are a pair of sentences where the first says the second is provable and the second says the first is unprovable Given $B_1(y)$ and $B_2(y)$ in the language of arithmetic, show there are sentences $G_1$ and $G_2$ such that:
$$\vdash_Q G_1 \leftrightarrow B_2(\ulcorner G_2 \urcorner)$$
$$\vdash_Q G_2 \leftrightarrow B_1(\ulcorner G_1 \urcorner)$$
 A: I'm not sure about it, but I think we must start with Gödel's sentence $G$ :

For each consistent formal theory $Q$ having the required small amount of number theory, the corresponding Gödel sentence $G$ asserts : "$G$ cannot be proved within the theory $Q$".

Let $G_1 := \lnot G$.
$G_1$ asserts : "$G$ is provable in $Q$".
Thus :

$G_1$ iff $\exists x Pf(x, \ulcorner G \urcorner)$, where $Pf$ is the predicate formalizing the fact that $x$ is the Gödel's number of a proof in $Q$ of the formula with Gödel's number $\ulcorner G \urcorner$ [see Elliott Mendelson, Introduction to Mathematical Logic (4th ed - 1997), page 198]. 

The above fact is provable in $Q$; thus :

$\vdash_Q G_1 \leftrightarrow \exists x Pf(x, \ulcorner G \urcorner)$.

Now, let $G_2 := \lnot G_1$. Thus, $G_2$ is the original Gödel's sentence $G$. So, we may replace $\ulcorner G \urcorner$ with $\ulcorner G_2 \urcorner$ to get :

$\vdash_Q G_1 \leftrightarrow \exists x Pf(x, \ulcorner G_2 \urcorner)$.

Up to now, we have found $B_2(x)$ such that :


$\vdash_Q G_1 \leftrightarrow B_2(\ulcorner G_2 \urcorner)$.


Gödel's Theorem "formalized" in Q amount to :

$\vdash_Q G \leftrightarrow \lnot \exists x Pf(x, \ulcorner G \urcorner)$.

Using $Neg$, the negation function [see Mendelson, page 196], we have that $\ulcorner G \urcorner = Neg(\ulcorner G_1 \urcorner)$; thus, being $G_2$ and $G$ the "same formula" :

$\vdash_Q G_2 \leftrightarrow \lnot \exists x Pf(x, Neg(\ulcorner G_1 \urcorner))$.

Thus, we have $B_1$ such that :


$\vdash_Q G_2 \leftrightarrow B_1(\ulcorner G_1 \urcorner)$.



Added : April, 8
As per comment of Peter Smith above, this answer does not address the original question, which ask for $B_1$ and $B_2$ arbitrary wffs with one free variable.
A: See George Boolos & John Burgess & Richard Jeffrey, Computability and Logic (5th ed - 2007), Problem 17.3, page 229.
We have to follow the hints in the website of the book :

Imitate the proof of the Diagonal Lemma [see BBJ, page 221], beginning as follows:
For formulas $E_1(x, y)$ and $E_2(x, y)$ with code numbers $e_1$ and $e_2$, let the first and second double diagonals be :
$\exists x \exists y (x = e_1 \land y = e_2 \land E_1(x, y))$, logically equivalent to $E_1(e_1, e_2)$
and
$\exists x \exists y (x = e_1 \land y = e_2 \land E_2(x, y))$, logically equivalent to $E_2(e_1, e_2)$.

Added - April, 18
I'm still not sure, but I think we need a "trick" in order to use the formulas of the Hint.
Starting from $B_1(x)$ and $B_2(x)$ whatever, let :

$E_1(x,y) := B_2(y) \land x = x$
$E_2(x,y) := B_1(x) \land y = y$.

Clearly : $\forall y(E_1(x,y) \leftrightarrow B_2(x))$ and $\forall x(E_2(x,y) \leftrightarrow B_1(y))$.
Now we consider $E_1(x,y)$ and $E_2(x,y)$ formulas.
Let $su (w, x_1, x_2)$ the function subst whose value at $\overline a, \overline b_1, \overline b_2$ is the G-number of the result of substituting respectively the numerals $\overline b_1, \overline b_2$ for the variables $x_1, x_2$ in the formula with G-number $\overline a$ [see the generalized diagnal lemma in George Boolos, The Logic of Provability (1993), page 53].
Let $\overline k_i$, be the G-number of :
$E_i(su(x_1, x_1, x_2), su(x_2, x_1, x_2))$
and let $G_i$ be the formula
$E_i(su(\overline k_1, \overline k_1, \overline k_2), su(\overline k_2, \overline k_1, \overline k_2))$.
The result of respectively substituting the numerals $\overline k_1, \overline k_2$ for the variables $x_1, x_2$ in the formula with G-number $\overline k_i$, i.e., in the formula
$E_i(su (x_1, x_1, x_2), su(x_2, x_1, x_2))$
is the formula $G_i$ and therefore subst($\overline k_i, \overline k_1, \overline k_2$) = the G-number of $G_i$.
Therefore, in $Q$ we can prove $su(\overline k_i, \overline k_1, \overline k_2) = \ulcorner G_i \urcorner$.
But by "construction", we have :

$\vdash_Q G_1 \leftrightarrow E_1 (\ulcorner G_1 \urcorner,\ulcorner G_2 \urcorner)$,

and $\vdash \forall y(E_1(x,y) \leftrightarrow B_2(y))$;
thus :


$\vdash_Q G_1 \leftrightarrow B_2(\ulcorner G_2 \urcorner)$.


In the same way :

$\vdash_Q G_2 \leftrightarrow E_2 (\ulcorner G_1 \urcorner,\ulcorner G_2 \urcorner) \leftrightarrow B_1(\ulcorner G_1 \urcorner)$.

