Many-one reducibility with realizability

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, Fin, the decision of being eventually zero for sequences, is many-one/Levin complete among Σ^0_2 formulas of the form ∃ n∀ m≥ n.φ(m,x), where φ is decidable. The decision of boundedness for sequences BddSeq and posets PO_ top are many-one/Levin complete among Σ^0_2 formulas of the form ∃ n∀ m≥ n∀ 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 NonDense is truly Σ^0_2-complete.