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.)
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.)