Positive introspection
= Positive introspection
{title2=$\Box A\to\Box\Box A$}
Positive introspection says that a boxed assertion can itself be boxed. For an <arithmetical provability predicate> it is the third of the <Hilbert-Bernays-Löb derivability conditions>: provability of $A$ implies provability of the assertion that $A$ is provable. It follows from formalized <Sigma-1 completeness> when provability assertions are Sigma-1. It is not the reflection principle $\Box A\to A$.