Many-one reducibility with realizability

Abstract

In this article, we propose a new classification of $Σ^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 $Σ^0_2$ formulas of the form $\exists n\forall m\geq n.φ(m,x)$, where $φ$ is decidable. The decision of boundedness for sequences ${\sf BddSeq}$ and for width of posets ${\sf FinWidth}$ are many-one/Levin complete among $Σ^0_2$ formulas of the form $\exists n\forall m\geq n\forall k.φ(m,k,x)$, where $φ$ is decidable. However, unlike the classical many-one reducibility, none of the above is $Σ^0_2$-complete. The decision of non-density of linear order ${\sf NonDense}$ is truly $Σ^0_2$-complete.