On a Hierarchy of Reflection Principles in Peano Arithmetic

We study reflection principles of Peano Arithmetic PA which are based on both proof and provability. Any such reflection principle in PA is equivalent to either $\Box P\!\rightarrow\! P$ ($\Box P$ stands for `$P$ is provable') or $\Box^k u\!\!:\!\!P\!\rightarrow\! P$ for some $k\geq 0$ ($t:P$ states `$t$ is a proof of $P$'). Reflection principles constitute a non-collapsing hierarchy with respect to their deductive strength $$u\!\!:\!\!P\!\rightarrow\! P\ \ \prec\ \ \Box u\!\!:\!\!P\!\rightarrow\! P\ \ \prec\ \ \Box^2 u\!\!:\!\!P\!\rightarrow\! P \ \ \prec\ \ldots\ \prec\ \ \Box P\!\rightarrow\! P.$$