 Logical fixed point

A logical fixed point is a formula or sentence equivalent to the result of applying a specified formula operation to itself. In arithmetic, self-reference is mediated by a Gödel number and the diagonal lemma, yielding a first-order sentence $G$ with a provable equivalence $G\leftrightarrow H(┌G┐)$. In modal logic, a modal formula $A$ satisfies $A\leftrightarrow F(A)$ modulo the chosen logic. A merely true semantic equivalence is weaker than a specified provable or canonical construction, so its hypotheses must be kept distinct.