= GL fixed point by truth substitution
{c}
{title2=$\mathrm{GL}\vdash\Box Y(\top)\leftrightarrow\Box Y(\Box Y(\top))$}
Let $U=\Box Y(\top)$ and $V=\Box Y(U)$. Boxed replacement gives $\Box U\to(U\leftrightarrow V)$, and <positive introspection> gives $U\to V$. For the reverse implication rewrite it as $V\to(\Box U\to U)$, necessitate, use $V\to\Box V$, and apply the Löb <axiom> to obtain $V\to\Box U\to U$. This explicit one-variable construction needs no <full local reflection in a one-sentence extension is inconsistent>[reflection] <axiom>.
Back to article page
