In this article, we propose a new classification of $\Sigma^0_2$ formulas under the realizability interpretation of many-one reducibility (i.e., Levin reducibility). For example, ${\sf Fin}$, the decision of being eventually zero for sequences, is many-one/Levin complete among $\Sigma^0_2$ formulas of the form $\exists n\forall m\geq n.\varphi(m,x)$, where $\varphi$ is decidable. The decision of boundedness for sequences ${\sf BddSeq}$ and posets ${\sf PO}_{\sf top}$ are many-one/Levin complete among $\Sigma^0_2$ formulas of the form $\exists n\forall m\geq n\forall k.\varphi(m,k,x)$, where $\varphi$ is decidable. However, unlike the classical many-one reducibility, none of the above is $\Sigma^0_2$-complete. The decision of non-density of linear order ${\sf NonDense}$ is truly $\Sigma^0_2$-complete.

翻译：本文提出了一种在可实现性解释下，对$\Sigma^0_2$公式进行多一归约（即莱文归约）的新分类。例如，序列最终是否为零的判定问题${\sf Fin}$，在形如$\exists n\forall m\geq n.\varphi(m,x)$（其中$\varphi$可判定）的$\Sigma^0_2$公式中是多一/莱文完备的。序列有界性判定问题${\sf BddSeq}$和偏序集顶点有界性判定问题${\sf PO}_{\sf top}$，在形如$\exists n\forall m\geq n\forall k.\varphi(m,k,x)$（其中$\varphi$可判定）的$\Sigma^0_2$公式中是多一/莱文完备的。然而，与经典多一归约不同，上述问题均非$\Sigma^0_2$完备的。线性序的非稠密性判定问题${\sf NonDense}$才是真正的$\Sigma^0_2$完备的。