 This formula \(B\) is called a fixed point of \(A(p)\). Moreover, the fixed point is unique, or more accurately, if there is another formula \(C\) such that \( \GL \vdash C \leftrightarrow A(C)\), then we must have \( \GL \vdash B \leftrightarrow C\). Most proofs in the literature give an algorithm by which one can compute the fixed point (see Smoryński 1985, Boolos 1993, Sambin and Valentini 1982, Lindström 2006). A particularly short and clear proof, as well as a very efficient algorithm to compute fixed points, can be found in Reidhaar-Olson (1990). 