GL fixed point for a provability implication
= GL fixed point for a provability implication
{c}
{title2=$F=(\Box q\to q),\quad\mathrm{GL}\vdash F\leftrightarrow(\Box F\to q)$}
The Löb axiom gives $\Box F\to\Box q$. The tautology $q\to F$, necessitated and distributed, gives $\Box q\to\Box F$. Thus $\Box F\leftrightarrow\Box q$, and replacing the antecedent in $\Box F\to q$ gives exactly $F$. Setting $q=\bot$ produces a negative-provability fixed point, provably equivalent to $\neg\Box\bot$.