Let $\mathfrak{P}$ be the preorder of $\Delta^0_0$ (= only bounded quantifiers) formulas with one free variable in the language of arithmetic with a symbol for each primitive recursive function, under the relation $\alpha(x)\le\beta(x)$ iff there is a primitive recursive function $p$ such that $$\mathsf{PA}\vdash \forall x[\neg\alpha(x)\rightarrow\neg\beta(p(x))].$$

As top element $\mathfrak{P}$ has the class of all formulas $\varphi$ such that $\forall x\varphi(x)$ is not true; the bottom element is the class of $x=x$, and the formula "$x$ is not a $\mathsf{PA}$-proof of $\perp$" is maximal amongst formulas whose universal closure is "schematically verifiable in $\mathsf{PA}$" in a particular sense (see this answer of mine.)

I suspect this preorder is well-known in proof theory, but I haven't seen it before; my question is, what is it?

Let $\mathfrak{P}$ be the preorder of $\Delta^0_0$ (= only bounded quantifiers) formulas with one free variable in the language of arithmetic, under the relation $\alpha(x)\le\beta(x)$ iff there is a primitive recursive function $p$ such that $$\mathsf{PA}\vdash \forall x[\neg\alpha(x)\rightarrow\neg\beta(p(x))].$$

As top element $\mathfrak{P}$ has the class of all formulas $\varphi$ such that $\forall x\varphi(x)$ is not true; the bottom element is the class of $x=x$, and the formula "$x$ is not a $\mathsf{PA}$-proof of $\perp$" is maximal amongst formulas whose universal closure is "schematically verifiable in $\mathsf{PA}$" in a particular sense (see this answer of mine.)

I suspect this preorder is well-known in proof theory, but I haven't seen it before; my question is, what is it?