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(\ulcorner G\urcorner)$. 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.


 Logical fixed point (source code)