Generalized fixed point theorem:

Suppose that $A_i(p_1,...,p_n)$ are $n$ modal sentences such that $A_i$ is modalized in $p_n$ (possibly containing sentence letters other than $p_{j}s$).

Then there exists $H_1,...,H_n$ in which no $p_j$ appears such that $GL⊢{\wedge }_{i\le n}\{⊡(p_i\leftrightarrow A_i(p_1,...,p_n)\}\leftrightarrow {\wedge }_{i\le n}\{⊡(p_i\leftrightarrow H_i)\}$.

We will prove it by induction.

For the base step, we know by the fixed point theorem that there is $H$ such that $GL⊢⊡(p_1\leftrightarrow A_i(p_1,...,p_n\left)\right)\leftrightarrow ⊡(p_1\leftrightarrow H(p_2,...,p_n\left)\right)$

Now suppose that for $j$ we have $H_1,...,H_j$ such that $GL⊢{\wedge }_{i\le j}\{⊡(p_i\leftrightarrow A_i(p_1,...,p_n)\}\leftrightarrow {\wedge }_{i\le j}\{⊡(p_i\leftrightarrow H_i(p_{j+1},...,p_n\left)\right)\}$.

By the second substitution theorem, $GL⊢⊡(A\leftrightarrow B)\to \left[F\right(A)\leftrightarrow F(B\left)\right]$. Therefore we have that $GL⊢⊡(p_i\leftrightarrow H_i(p_{j+1},...,p_n)\to [⊡(p_{j+1}\leftrightarrow A_{j+1}(p_1,...,p_n\left)\right)\leftrightarrow ⊡(p_{j+1}\leftrightarrow A_{j+1}(p_1,...,p_{i-1},H_i(p_{j+1},...,p_n),p_{i+1},...,p_n\left)\right)]$.

If we iterate the replacements, we finally end up with $GL⊢{\wedge }_{i\le j}\{⊡(p_i\leftrightarrow A_i(p_1,...,p_n)\}\to ⊡(p_{j+1}\leftrightarrow A_{j+1}(H_1,...,H_j,p_{j+1},...,p_n))$.

Again by the fixed point theorem, there is $H_{j+1}^{\prime }$ such that $GL⊢⊡(p_{j+1}\leftrightarrow A_{j+1}(H_1,...,H_j,p_{j+1},...,p_n\left)\right)\leftrightarrow ⊡[p_{j+1}\leftrightarrow H_{j+1}^{\prime }(p_{j+2},...,p_n\left)\right]$.

But as before, by the second substitution theorem, $GL⊢⊡[p_{j+1}\leftrightarrow H_{j+1}^{\prime }(p_{j+2},...,p_n\left)\right]\to [⊡(p_i\leftrightarrow H_i(p_{j+1},...,p_n))\leftrightarrow ⊡(p_i\leftrightarrow H_i(H_{j+1}^{\prime },...,p_n))$.

Let $H_i^{\prime }$ stand for $H_i(H_{j+1}^{\prime },...,p_n)$, and by combining the previous lines we find that $GL⊢{\wedge }_{i\le j+1}\{⊡(p_i\leftrightarrow A_i(p_1,...,p_n)\}\to {\wedge }_{i\le j+1}\{⊡(p_i\leftrightarrow H_i^{\prime }(p_{j+2},...,p_n\left)\right)\}$.

By Goldfarb's lemma, we do not need to check the other direction, so $GL⊢{\wedge }_{i\le j+1}\{⊡(p_i\leftrightarrow A_i(p_1,...,p_n)\}\leftrightarrow {\wedge }_{i\le j+1}\{⊡(p_i\leftrightarrow H_i^{\prime }(p_{j+2},...,p_n\left)\right)\}$ and the proof is finished $\square$

An immediate consequence of the theorem is that for those fixed points $H_i$ and every $A_i$, $GL⊢H_i\leftrightarrow A_i(H_1,...,H_n)$.

Indeed, since $GL$ is closed under substitution, we can make the change $p_i$ for $H_i$ in the theorem to get that $GL⊢{\wedge }_{i\le n}\{⊡(H_i\leftrightarrow A_i(H_1,...,H_n)\}\leftrightarrow {\wedge }_{i\le n}\{⊡(H_i\leftrightarrow H_i)\}$.

Since the righthand side is trivially a theorem of $GL$, we get the desired result.

One remark: the proof is wholly constructive. You can iterate the construction of fixed point following the procedure implied by the construction of the $H_i^{\prime }$ to compute fixed points.

Uniqueness of arithmetic fixed points:

Notation: $⊡A=\square A\wedge A$

Let $H$ be a fixed point on $p$ of $\varphi \left(p\right)$; that is, $GL⊢⊡(p\leftrightarrow \varphi (p\left)\right)\leftrightarrow (p\leftrightarrow H)$.

Suppose $I$ is such that $GL⊢H\leftrightarrow I$. Then by the first substitution theorem, $GL⊢F\left(I\right)\leftrightarrow F\left(H\right)$ for every formula $F\left(q\right)$. If $F\left(q\right)=⊡(p\leftrightarrow q)$, then $GL⊢⊡(p\leftrightarrow H)\leftrightarrow ⊡(p\leftrightarrow I)$, from which it follows that $GL⊢⊡(p\leftrightarrow \varphi (p\left)\right)\leftrightarrow (p\leftrightarrow I)$.

Conversely, if $H$ and $I$ are fixed points, then $GL⊢⊡(p\leftrightarrow H)\leftrightarrow ⊡(p\leftrightarrow I)$, so since $GL$ is closed under substitution, $GL⊢⊡(H\leftrightarrow H)\leftrightarrow ⊡(H\leftrightarrow I)$. Since $GL⊢⊡(H\leftrightarrow H)$, it follows that $GL⊢(H\leftrightarrow I)$.

(Taken from The Logic of Provability, by G. Boolos.)