By knowing Solovay's proof for the arithmetical completeness of provability logic, isn't the celebrated fixed point lemma of provability logic just equivalent to the Gödel's diagonal lemma? Or does fixed point lemma shed some extra light to Peano arithmetics (shortly PA) compared to diagonalization lemma?
Diagonal lemma for PA : For any formula $B(x)$, with exactly one free variable $x$ there is a formula $G$ such that $PA\vdash G \leftrightarrow B([G]^{*})$.
*($[x]=_{def}$ Gödel-number of $x$)
Fixed point lemma of GL: Suppose that all occurrences of the propositional variable p in a given formula B(p) are under the scope of the provability operator, for example $B(p)=¬◻p$, or $B(p)=◻(p→q)$. Then there is a formula G in which p does not appear, such that all propositional variables that occur in D already appear in B(p), and such that $GL\vdash G \leftrightarrow B(G)$.
My attempt to answer:
When fixed point lemma of GL is translated to PA I have found it to be stronger than diagonal lemma. The difference and advantage I have found is that:
i.) Most of the diagonal lemma constructions (the proof) contain an algorithm to compute the fixed points. I am not aware of similar constructions in PA. (This of course doesn't have anything to do with the lemma per se, rather with the proof of the lemma.)
ii.) Diagonal lemma tells us that there is such a formula $G$ s.t. $PA\vdash G \leftrightarrow B([G]^{*})$, this is typically made with self-reference, like in the case with Gödel-sentence. Fixed point lemma tells us more, it tells us that every self-referential sentence can be expressed 'non-self-referentially'. And this last point seems to be quite deep philosophically speaking since it tells us that self-referential sentences (paradoxes) have genuine meanings determinable without resort to selfreference.