Generalized fixed point theorem:
Suppose that are modal sentences such that is modalized in (possibly containing sentence letters other than ).
Then there exists in which no appears such that .
We will prove it by induction.
For the base step, we know by the fixed point theorem that there is such that
Now suppose that for we have such that .
By the second substitution theorem, . Therefore we have that .
If we iterate the replacements, we finally end up with .
Again by the fixed point theorem, there is such that .
But as before, by the second substitution theorem, .
Let stand for , and by combining the previous lines we find that .
By Goldfarb’s lemma, we do not need to check the other direction, so and the proof is finished
An immediate consequence of the theorem is that for those fixed points and every , .
Indeed, since is closed under substitution, we can make the change for in the theorem to get that .
Since the righthand side is trivially a theorem of , 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 to compute fixed points.
Uniqueness of arithmetic fixed points:
Notation: ⊡A=□A∧A
Let H be a fixed point on p of ϕ(p); that is, GL⊢⊡(p↔ϕ(p))↔(p↔H).
Suppose I is such that GL⊢H↔I. Then by the first substitution theorem, GL⊢F(I)↔F(H) for every formula F(q). If F(q)=⊡(p↔q), then GL⊢⊡(p↔H)↔⊡(p↔I), from which it follows that GL⊢⊡(p↔ϕ(p))↔(p↔I).
Conversely, if H and I are fixed points, then GL⊢⊡(p↔H)↔⊡(p↔I), so since GL is closed under substitution, GL⊢⊡(H↔H)↔⊡(H↔I). Since GL⊢⊡(H↔H), it follows that GL⊢(H↔I).
(Taken from The Logic of Provability, by G. Boolos.)