Generalize the Gödel sentence requires a fixed point theorem I am trying to generalize the Gödel sentence as follows.
Define a pair of sentence $A$ and $B$ such that:
\begin{gather*}
A := \lnot \operatorname{Prov}(\hat B) \\
B :=  \operatorname{Prov}(\hat A)
\end{gather*}
where $\hat A$ and $\hat B$ are the Gödel numbers of $A$ and $B$ respectively.
From the definition above I derive the following equation $\hat A = \text{the Gödel number of $\lnot \operatorname{Prov}(\widehat{\operatorname{Prov}(\hat A)}) $}$. My question is for a minimal system that the incompleteness theorems apply, whether this equation always has a fixed point?
 A: Yes, in fact every such finite self-referential system has a fixed-point solution, and this can be proved using the same methods usually used to prove the unary fixed-point lemma. Such systems were explored at great length by Raymond Smullyan in several of his books. (But your desired example requires only the ordinary fixed-point lemma, which will produce a sentence $A$ that it is provably equivalent to $\neg\text{Prov}(\text{Prov}(A))$.)
You can also find an account in my expository article, A review of the Gödel fixed-point lemma with generalizations and applications, which gives this fixed-point result as well as others — the Gödel fixed-point lemma, the finite-system fixed-point lemma, the Gödel-Carnap fixed-point lemma, the Kleene recursion theorem, with applications to Turing's theory of computable numbers and so on. In particular, Lemma 3 in that paper is double-fixed point lemma:
Lemma. (Double-fixed point). $\newcommand{\gcode}[1]{\ulcorner\!#1\!\urcorner}$ Suppose that $A(x,y)$ and $B(x,y)$ are two formulas in the language of arithmetic, then there are sentences $\phi$ and $\psi$ such that PA proves the equivalences
$$\phi\iff A(\gcode{\phi},\gcode{\psi})$$
and
$$\psi\iff B(\gcode{\phi},\gcode{\psi}).$$
Proof. Let $\text{Sub}$ be the binary substitution operator, the
primitive recursive function such that
$\text{Sub}(\gcode{\eta(x,y)},n,m)=\gcode{\eta(\kern1pt\underline{n},\kern1pt\underline{m}\kern1pt)}$. Let
$\theta_1(x,y)=A(\text{Sub}(x,x,y),\text{Sub}(y,x,y))$ and
$\theta_2(x,y)=B(\text{Sub}(x,x,y),\text{Sub}(y,x,y))$. Let
$n=\gcode{\theta_1(x,y)}$ and $m=\gcode{\theta_2(x,y)}$. Finally, let
$\phi=\theta_1(\kern1pt\underline{n},\underline{m}\kern1pt)$ and $\psi=\theta_2(\kern1pt\underline{n},\underline{m}\kern1pt)$.
Observe that
\begin{eqnarray*}
\phi &\iff& \theta_1(\kern1pt\underline{n},\underline{m}\kern1pt)\\
     &\iff& A(\text{Sub}(\kern1pt\underline{n},\underline{n},\underline{m}\kern1pt),\text{Sub}(\kern1pt\underline{m},\underline{n},\underline{m}\kern1pt))\\
     &\iff& A(\gcode{\theta_1(\kern1pt\underline{n},\underline{m}\kern1pt)},\gcode{\theta_2(\kern1pt\underline{n},\underline{m}\kern1pt)})\\
     &\iff& A(\gcode{\phi},\gcode{\psi}).\\
\end{eqnarray*}
Also observe
\begin{eqnarray*}
\psi &\iff& \theta_2(\kern1pt\underline{n},\underline{m}\kern1pt)\\
     &\iff& B(\text{Sub}(\kern1pt\underline{n},\underline{n},\underline{m}\kern1pt),\text{Sub}(\kern1pt\underline{m},\underline{n},\underline{m}\kern1pt))\\
     &\iff& B(\gcode{\theta_1(\kern1pt\underline{n},\underline{m}\kern1pt)},\gcode{\theta_2(\kern1pt\underline{n},\underline{m}\kern1pt)})\\
     &\iff& B(\gcode{\phi},\gcode{\psi}),
\end{eqnarray*}
as desired.
$\Box$
Note that we can arrange that $\phi$ and $\psi$ are distinct simply by ensuring that $\theta_1(n,m)$ and $\theta_2(n,m)$ are not syntactically the same sentence,
such as by replacing $\theta_1(x,y)$ with its conjunction, if necessary, while ensuring that $\theta_2(x,y)$ does not have such a
form.
The lemma easily generalizes to any size system and indeed, to infinite systems of fixed points.
