Many-one reducibility with realizability

TL;DR

The paper develops a Levin-style many-one reducibility for witnessed subsets within represented spaces, linking computable Levin reducibility to the internal logic of categories with pullbacks. It analyzes the arithmetical/Borel hierarchy in this setting, focusing on Σ^0_2 subobjects and introducing notions like regular vs non-regular subobjects and demi-reducibility (Weihrauch-type). The main results classify several natural Σ^0_2 sets (e.g., ${\sf Fin}$, ${\sf BddSeq}$, ${\sf FinWidth}$, ${\sf NonDense}$) by witnessing properties (unique, increasing, half-hard) and establish a strict hierarchy of completeness/hardness among them, while showing that some classical complete sets avoid this order-theoretic alignment in the witnessed setting. The work illuminates how intuitionistic and constructive frameworks affect classical completeness, revealing refined structurings of definable sets and offering tools for deeper hierarchy analyses beyond the classical scope. The findings have potential implications for understanding finitary decision problems with certificates under constructive semantics and for bridging computability theory with category-theoretic representations.

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.\varphi(m,x)$, where $\varphi$ 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.\varphi(m,k,x)$, where $\varphi$ 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.

Figures (5)

• Figure 1: The fine analysis of classical $\Sigma^0_2$-complete sets
• Figure 2: (left) A reduction pair for ${\sf DisConn}_{\sf fun}\leq_{\sf m}{\sf HalfTruth}_{\Sigma^0_2}$ if it exists; (right) An example of our action if $r_+$ moves a pair $\{z^\ell_{mn},z^p_{qr}\}$ out of the triangle $\{u_0,u_1,u_2\}$.
• Figure 3: Some examples of our actions.
• Figure 4: If $\{a^{01}_{00},a^{01}_{11}\}\subseteq\{1\}$, our action forces $\{u^0_0,u^1_0\}$, $\{u^1_0,u^1_1\}$ and $\{u^1_1,u^0_1\}$ to be connected.
• Figure 5: If $a^{01}_{00}=a^{01}_{01}=0$, our action forces $\{u^0_0,u^1_0\}$, $\{u^0_0,u^1_1\}$ and $\{u^1_1,u^0_1\}$ to be connected.

Theorems & Definitions (134)

• Definition 1.1: Levin Lev73
• Definition 2.1
• Example 2.2
• Example 2.3
• Example 2.4
• Example 2.5
• Definition 2.6
• Definition 2.7
• Definition 3.1
• Definition 3.2