Return to Answer

Yes, in fact every such finite system has a fixed-point, 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 in fact, to find your sentence $A$ that is provably equivalent to $\neg\text{Prov}(\text{Prov}(A))$ requires merely the ordinary fixed-point result.)

Meanwhile, you can also find a brief account in my expository article, A review of the Gödel fixed-point lemma with generalizations and applications. Lemma 3 there is the 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.

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.

Yes, every such finite system has a fixed-point, 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.

Meanwhile, you can also find a brief account in my expository article, A review of the Gödel fixed-point lemma with generalizations and applications. Lemma 3 there is the 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.

Yes, in fact every such finite system has a fixed-point, 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 in fact, to find your sentence $A$ that is provably equivalent to $\neg\text{Prov}(\text{Prov}(A))$ requires merely the ordinary fixed-point result.)

Meanwhile, you can also find a brief account in my expository article, A review of the Gödel fixed-point lemma with generalizations and applications. Lemma 3 there is the 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.

Yes, every such finite system has a fixed-point, 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.

Meanwhile, you can also find a brief account in my expository article, A review of the Godel fixed-point lemma with generalizations and applications.

Yes, every such finite system has a fixed-point, 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.

Meanwhile, you can also find a brief account in my expository article, A review of the Gödel fixed-point lemma with generalizations and applications. Lemma 3 there is the 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.