Adapting from Anil Gupta and & Nuel Belnap, *Revision theory of truth*, MIT 1993, p. 194, in the context of a second order logic, where $A(x.G)$ is a formula where $G$ only occurs positively, a fixed point


$$\forall x(Gx\leftrightarrow A(x,G))$$


may be isolated. One may also show


$$\forall x(Gx\leftrightarrow\forall H[\forall x(Hx\leftrightarrow A(x,H))\rightarrow Hx])$$


I understand how these together define a least fixed point of $A(x,G)$.


How may one define a largest fixed point of $A(x,G)$ in the context?



How may a largest fixed-point be defined in second order logic?
Just as the least fixed point is the intersection of all the sets $H$ such that $\forall x\,(A(x,H)\to H(x))$, so (dually) the greatest fixed point is the union of all the sets $K$ such that $\forall x\,(K(x)\to A(x,K))$.


Alternatively, one can use duality to obtain the greatest fixed point of $A(x,G)$ as the complement of the least fixed point of $\neg A(x,\neg G)$.


