Many-one reducibility with realizability

In this article, we propose a new classification of Σ⁰₂ 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 Σ⁰₂ formulas of the form ∃ n∀ m≥ n.φ(m,x), where φ is decidable. The decision of boundedness for sequences BddSeq and posets POₜₒₚ are many-one/Levin complete among Σ⁰₂ 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 Σ⁰₂-complete. The decision of non-density of linear order NonDense is truly Σ⁰₂-complete.