Many-one reducibility with realizability

Abstract

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