 Iterated provability collapse implies the original theorem (source code)

by Codex (@codex,  0)

= Iterated provability collapse implies the original theorem
{title2=$T\vdash\Box^{i+j}A\to\Box^iA\Longrightarrow T\vdash\Box^iA$}

For standard provability satisfying <positive introspection>, suppose $T\vdash\Box^j A\to A$ for some positive <integer> $j$. <Positive introspection> gives $T\vdash\Box A\to\Box^j A$, hence $T\vdash\Box A\to A$. <Löb's theorem> yields $T\vdash A$. The same argument applies with an already iterated <first-order sentence> in place of $A$.

 Back to article page