Recursive Jump Operators and Optimal Proof Systems

It is an easy fact that all sets in $\mathrm{NP}$ have optimal proof systems. Messner [39] shows that there are sets without optimal proof systems. He proved that for any non-polynomial time-constructible function $t$ there are sets in $\mathrm{coNTIME}(t)$ that do not have optimal proof systems and that all ${\le }_{\mathrm{m}}^{\mathrm{p}}$-hard sets for $\mathrm{coNE}$ do not have optimal proof systems. Surprisingly, this already covers all that we unconditionally know about the existence of optimal proof systems. Messner [40] also shows that if $\mathrm{NP}=\mathrm{coNP}$, then arbitrary complex sets with optimal proof systems exist. In contrast, Egidy and Glaßer [19] construct two oracles: relative to the first all sets outside non-deterministic quasi-polynomial time do not have optimal proof systems and relative to the second the polynomial-time hierarchy is infinite and all sets in $\mathrm{PSPACE}\setminus \mathrm{NP}$ do not have optimal proof systems. Hence, for most sets we do not know whether they have optimal proof systems and proving their existence would require to overcome at least the relativization barrier.

The most interesting and best-studied proof systems are proof systems for $\mathrm{TAUT}$. Krajíček and Pudlák [36] showed that $\mathrm{NE}=\mathrm{coNE}$ implies the existence of optimal proof systems for $\mathrm{TAUT}$, which was improved to $\mathrm{NEE}=\mathrm{coNEE}$ by Köbler, Messner, and Torán [37]. Razborov [45] discovered the first connection between optimal proof systems and promise classes by showing that the existence of optimal proof systems for $\mathrm{TAUT}$ implies the existence of ${\le }_{\mathrm{m}}^{\mathrm{pp}}$-complete sets for $\mathrm{DisjNP}$, i.e., the class of disjoint $\mathrm{NP}$-pairs defined by Selman [48] and Selman and Grollman [25]. Initiated by this result, many further connections between proof systems for $\mathrm{TAUT}$ and disjoint $\mathrm{NP}$-pairs were obtained [42, 3, 23, 4, 5, 21, 22, 7, 6, 9, 24]. As already mentioned above, the relationship between proof systems and promise classes has turned out to be quite fruitful. These connections in addition to various connections of optimal proof systems to bounded arithmetic (cf. [32, 44, 35]) lead into a research program initiated by Pudlák [43]. Pudlák surveys on several conjectures concerning the existence of optimal proof systems for sets (including conjecture C1) and the existence of complete sets for promise classes (like $\mathrm{UP}$, $\mathrm{NP}\cap \mathrm{coNP}$, $\mathrm{TFNP}$) and asks for a systematic investigation of their relationships. In particular, Pudlák is interested in either proving further implications between conjectures or disproving them relative to an oracle. Since then several implications have been disproved relative to an oracle [15, 18, 16, 17, 20, 23, 27].

One approach to rule out the existence of optimal proof systems for $\mathrm{TAUT}$ is to provide a computable procedure that takes an arbitrary proof system $f$ and produces an improved system that efficiently proves tautologies for which $f$ admits only long proofs. Khaniki [28] calls such procedures efficient jump operators. Several candidate efficient jump operators have been proposed [36, 10, 34, 28] in the hope that they are useful to prove that even strong proof systems like extended Frege are not optimal. A similar concept are hard tautology generators, that informally compute families of tautologies that a given proof system requires super-polynomial size proofs on (cf. [28, Def. 3.2] for a precise definition).

The existence of non-recursive jump operators for $\mathrm{TAUT}$ is equivalent to the non-existence of optimal proof systems for $\mathrm{TAUT}$ which is equivalent to the existence of hard tautology generators [36, 28]. Khaniki [28] extends this relationship to the “efficient” setting, i.e., Khaniki shows that the existence of all of the following concepts are equivalent: partial recursive jump operators, recursive jump operators, polynomial time computable jump operators, partial recursive hard tautology generators, recursive hard tautology generators, polynomial time computable hard tautology generators. Khaniki [28] explicitly asks whether the existence of recursive jump operators is also equivalent to the non-existence of optimal proof systems for $\mathrm{TAUT}$, to which our main result contributes to.

Our main contribution to Q1 is the construction of the following oracle (cf. Corollary 33), which shows that proving a positive answer for Q1 is provably hard and answers an open question by Khaniki [28].

The oracle $O$ answers the question posed by Khaniki [28, Problem 10] in the sense that no relativizable proof can show the implication Q1. Even more, the hardness of Q1 remains true even if one assumes that the polynomial-time hierarchy is infinite. Note that from the point of view of answering Q1 in the negative, results like ours are the best we can hope for, because actually proving Q1 in the negative implies a proof of conjecture C1 and thus $\mathrm{NP}\ne \mathrm{coNP}$, which currently seems completely out of reach. Hence, a separation via oracles is a standard approach to separate two such longstanding complexity theoretic conjectures from each other, e.g., as reflected by Pudlák’s [43] approach to separate conjectures in his research program.

In contrast to Q1, we obtain partial positive results regarding Q2, namely for sets currently known to lack optimal proof systems. Messner [39] shows the existence of sets that do not have optimal proof systems. Together with the closure under ${\le }_{\mathrm{m}}^{\mathrm{p}}$-reducibility for the class of all sets with optimal proof systems proved by Köbler and Messner [31], Messner obtains that all ${\le }_{\mathrm{m}}^{\mathrm{p}}$-hard sets for $\mathrm{coNE}$ do not have optimal proof systems.

First, we show that the existence of recursive jump operators is upward closed under ${\le }_{\mathrm{m}}^{\mathrm{p}}$-reducibility, i.e., the existence of recursive jump operators for $L$ implies the existence of recursive jump operators for any set $L^{\prime }$ such that $L{\le }_{\mathrm{m}}^{\mathrm{p}}{L}^{\prime }$ (cf. Theorem 1). This is a dual result to the ${\le }_{\mathrm{m}}^{\mathrm{p}}$-closure result of Köbler and Messner. Second, we analyze Messner’s proof against the existence of optimal proof systems for sets. By doing so, we derive a recursive jump operator for these sets (cf. Theorem 7). In total, our results show that any set shown to not have optimal proof systems by Messner [39] in fact has recursive jump operators. This covers essentially all sets currently known to have no optimal proof systems.

Let $J_1,J_2,\mathrm{\dots }$ and $P_1,P_2,\mathrm{\dots }$ notations for the same standard enumeration of Turing transducers. For clarity, we use the enumeration $J_i$ when referring to candidate recursive jump operators and $P_i$ when referring to candidate proof systems. We treat all $J_i$ as candidate recursive jump operators for $\mathrm{TAUT}$ and diagonalize against them. Let $J_i$ be an arbitrary such candidate.

The key idea is to construct a witness proof system $W_i$ that evaluates $J_i$ on its own program code and neutralizes $J_i$’s jump. We achieve this by using an effective version of Kleene’s [29, 30, 49] fixed-point theorem. Informally, the Turing transducer $W_i$ works as follows:

• $\mathrm{■}$

  $W_i$ computes $J_i(W_i)=b$, which is possible by an invocation of the fixed-point theorem.

• $\mathrm{■}$

  Depending on carefully encoded information in the oracle, $W_i$ may either:

  • –

    simulate the allegedly stronger proof system $P_b$, or

  • –

    fall back to a fixed, baseline proof system for $\mathrm{TAUT}$.

There are three ways in which $J_i$ can fail to be a recursive jump operator. Namely, if there is some $a\in {\mathbb{N}}^{+}$ such that

1. F1

   $J_i(a)$ does not halt.

2. F2

   $J_i(a)=b$ and $P_a$ is a proof system for $\mathrm{TAUT}$ and $P_b$ is no proof system for $\mathrm{TAUT}$.

3. F3

   $J_i(a)=b$ and $P_a$, $P_b$ are proof systems for $\mathrm{TAUT}$, but $P_a$ simulates $P_b$.

Note that properties such as “$P_b$ is a proof system for $\mathrm{TAUT}$” are generally not robust under extensions of the oracle⁴⁴4Meaning, just because $P_b$ is a proof system for $\mathrm{TAUT}$ relative to some partial oracle $w$ does not mean that this holds relative to extensions of $w$.. We have to account for that in the oracle construction, but for simplicity, we will ignore it in this sketch.

When diagonalizing against $J_i$, the oracle construction first attempts to realize Case F1 or F2 by an appropriate partial extension of the oracle. If this is not possible, we enforce Case F3 with $a≔W_i$. Since Case F1 failed, $J_i(W_i)=b$ is defined. Since Case F2 failed, $P_b$ is a proof system for $\mathrm{TAUT}$. We then add some suitable code word to the oracle that allows $W_i$ to simulate $P_b$. Then $J_i(W_i)=b$, $W_i$ and $P_b$ are proof systems for $\mathrm{TAUT}$ and $W_i$ simulates $P_b$.

We diagonalize against all disjoint $\mathrm{NP}$-pairs for being ${\le }_{\mathrm{m}}^{\mathrm{pp}}$-complete. Given a pair of $\mathrm{NP}$-machines $(N_0,N_1)$, we define a corresponding witness disjoint pair $(A,B)$ whose elements are determined by the oracle on carefully chosen designated lengths. In particular, $0^n\in A$ if $n$ is of designated length and the oracle contains words from $00{\mathrm{\Sigma }}^{n-2}$. Analogous for $B$ and $01{\mathrm{\Sigma }}^{n-2}$.

For each candidate reduction function $f\in \mathrm{FP}$, we ensure that $(A,B){\nleqq }_{\mathrm{m}}^{\mathrm{pp}}(L(N_0),L(N_1))$ via $f$. We immediately diagonalize successfully, if we can add some word from $00{\mathrm{\Sigma }}^{n-2}$ (resp., $01{\mathrm{\Sigma }}^{n-2}$) to the oracle and $N_0(f(0^n))$ (resp., $N_1(f(0^n))$) rejects. If neither is possible, then both machines must accept on an exponential number of distinct oracle extensions obtained by words of length $n$. However, each leftmost accepting path queries only polynomially many oracle words. This allows us to extend the oracle by two words such that neither leftmost accepting path recognizes the second word. Consequently, $L(N_0)$ and $L(N_1)$ are not disjoint, and hence do not form a ${\le }_{\mathrm{m}}^{\mathrm{pp}}$-complete disjoint $\mathrm{NP}$-pair.

We denote the length of a word $w\in {\mathrm{\Sigma }}^{\ast }$ by $|w|$. The empty word has length $0$ and is denoted by $\epsilon$. The $(i+1)$-th letter of a word $w$ for is denoted by $w(i)$, i.e., $w=w(0)w(1)\mathrm{\cdots }w(|w|-1)$. If $v$ is a (strict) prefix of $w$, we write $v⊑w$ ($v⋤w$) or $w⊒v$ ($w⋥v$).

We identify ${\mathrm{\Sigma }}^{\ast }$ with $\mathbb{N}$ through a polynomial-time computable and polynomial-time invertible bijection $\mathrm{enc}:{\mathrm{\Sigma }}^{\ast }\to \mathbb{N}$ defined as . Thus, we can treat words from ${\mathrm{\Sigma }}^{\ast }$ as numbers from $\mathbb{N}$ and vice versa, which allows us to use notations, relations and operations of words for numbers and vice versa (e.g., we can define the length of a number by this). In particular, $\mathrm{ran}(⟨\cdot ⟩)\subseteq 0{\mathrm{\Sigma }}^{\ast }$. Expressions like $0^i$ and $1^i$ are ambiguous, because they can be interpreted as words from ${\mathrm{\Sigma }}^{\ast }$ or numbers. We resolve this ambiguity by the context or explicitly naming the interpretation. A word $w\in {\mathrm{\Sigma }}^{\ast }$ can be interpreted as a set $\{i\in \mathbb{N}\mid w(i)=1\}$ and subsequently as a partial oracle, which is defined for all words up to $|w|-1$. So $|w|$ is the first word that $w$ is not defined for, i.e., $|w|\in w1$ and $|w|\notin w0$. During the oracle construction we often use words from ${\mathrm{\Sigma }}^{\ast }$ to denote partially defined oracles. In particular, oracle queries for undefined words of a partial oracle are answered negatively.

For a deterministic Turing machine or transducer $F$ and an oracle $O$, we define $Q(F^O(x))$ as the set of words queried to the oracle by the computation $F^O(x)$. For a non-deterministic Turing machine $N$, we define $Q(N^O(x))$ as the set of words queried on the leftmost accepting computation path of $N^O(x)$. If $N^O(x)$ rejects, then $Q(N^O(x))$ is the empty set. Note that in the context of $Q$ we view a chained computation like $N^O(F^O(x))$ as one computation that first computes $F^O(x)=y$ and then $N^O(y)$.

A function $f^{\prime }$ is an extension of a function $f$, denoted by $f⊑f^{\prime }$ or $f^{\prime }⊒f$, if $\mathrm{dom}(f)\subseteq \mathrm{dom}(f^{\prime })$ and $f(x)=f^{\prime }(x)$ for all $x\in \mathrm{dom}(f)$. If $x\notin \mathrm{dom}(f)$, then $f\cup \{x\mapsto y\}$ denotes the extension $f^{\prime }$ of $f$ such that $f^{\prime }(z)=f(z)$ for $z\ne x$ and $f^{\prime }(x)=y$. We define polynomial functions $p_i:\mathbb{N}\to \mathbb{N}$ for $i\in {\mathbb{N}}^{+}$ by $p_i(n)≔n^i+i$.

A computation $F^w(x)$ is called definite, if $w$ is defined for all words of length less than or equal to the runtime bound of $F^w(x)$. A computation definitely accepts (resp., rejects), if it is definite and accepts (resp., rejects). We may combine computations to more complex expressions and call those definite, if every individual computation is definite, e.g., “$N^w(F^w(x))$ is definite” means $F^w(x)$ outputs some $y$ and is definite, and $N^w(y)$ is definite.

For any oracle $O$ let ${\{F_i^O\}}_{i\in {\mathbb{N}}^{+}}$ be a standard enumeration of polynomial time oracle Turing transducers, where $F_i^O$ has running time exactly $p_i$. For any oracle $O$ let ${\{N_i^O\}}_{i\in {\mathbb{N}}^{+}}$ be a standard enumeration of non-deterministic polynomial time oracle Turing machines, where $N_i^O$ has running time exactly $p_i$. For any oracle $O$, let ${\{J_i^O\}}_{i\in {\mathbb{N}}^{+}}$ be a standard enumeration of oracle Turing transducers and let ${\{P_i^O\}}_{i\in {\mathbb{N}}^{+}}$ be a different notation for the same enumeration. For readability, we will use the machines $J_i$ when referring to candidate jump operators and the machines $P_i$ when referring to candidate proof systems, although $J_i$ is the same machine as $P_i$.

For each candidate disjoint $\mathrm{NP}$-pair $(C,D)$ we define a witness pair $(A_m,B_m)\in \mathrm{DisjNP}$ showing that $(A_m,B_m){\nleqq }_{\mathrm{m}}^{\mathrm{pp}}(C,D)$, i.e., $(A_m,B_m)$ is a witness that $(C,D)$ is no ${\le }_{\mathrm{m}}^{\mathrm{pp}}$-complete pair for $\mathrm{DisjNP}$.

For each candidate recursive jump operator $J_i$ we define many witness proof systems $W_{i,m}$ possibly witnessing that $J_i$ is no recursive jump operator for $\mathrm{TAUT}$, i.e., $J_i(⟨W_{i,m}⟩)=b$ and either $P_b$ is no proof system for $\mathrm{TAUT}$ or $W_{i,m}$ simulates $P_b$.

We use this fixed-point theorem to define our witness proof systems $W_{i,m}$ such that they evaluate $J_i$ on their own program code. For this, let $i,m\in {\mathbb{N}}^{+}$ and let $s_{i,m}:{\mathbb{N}}^{+}\to {\mathbb{N}}^{+}$ be a function that returns the code of the oracle-program defined in Algorithm 2 when given $z\in {\mathbb{N}}^{+}$ as input. Note that $O$ is a placeholder for an arbitrary oracle, let $F$ be a proof system for $\mathrm{TAUT}$ relative to all oracles, and recall that $p_t$ is the polynomial bounding the number of steps to non-deterministically decide $\overline{\mathrm{TAUT}}$ relative to any oracle. We provide some intuition of Algorithm 2 after Observation 17.

For all $i,m\in {\mathbb{N}}^{+}$, let $⟨s_{i,m}⟩$ denote the program code of a polynomial-time Turing transducer computing $s_{i,m}$. The following observation shows that such a Turing transducer exists.

Let $i,m\in {\mathbb{N}}^{+}$ be arbitrary. It is clear that (i) holds. Property (ii) follows by the totality of $s_{i,m}$ and Theorem 14 invoked with $⟨s_{i,m}⟩$ for $i$. $◂$

With this, for every candidate recursive jump operator $J_i$, we have infinitely many witness proof systems $W_{i,m}$ behaving like Algorithm 2 where $z=⟨W_{i,m}⟩$. So $W_{i,m}$ first evaluates $J_i$ on its own program code and obtains the code of a supposedly stronger proof system $P_b$. Depending on information in the oracle, $W_{i,m}$ is allowed to simulate $P_b$. Here, the oracle should only allow the simulation of $P_b$ if $\mathrm{ran}(P_b)\subseteq \mathrm{TAUT}$. Lastly, $W_{i,m}$ only simulates $P_b$ if the simulation can be done in a polynomial number of steps, ensuring that $W_{i,m}$ remains polynomial-time computable.

The following results show that if $P_b$ is a proof system and the oracle has the right conditions, $W_{i,m}$ is a proof system for $\mathrm{TAUT}$ that simulates $P_b$.

Consider $W_{i,m}^O$. Line 2 does not depend on the size of the input and halts by assumption, thus requiring only constant time. Lines 3 and 4 are about at most polynomially many polysize oracle queries. Lines 5 and 6 are about simulating computations for a polynomially bounded number of steps. Finally, lines 8 and 12 simulate a proof system for ${\mathrm{TAUT}}^O$. Hence, $W_{i,m}^O$ runs in polynomial time.

Line 2 computes the number $b$ from the assumption. Any output is either computed by $P_b^O$ or $F^O$, whose ranges are subsets of ${\mathrm{TAUT}}^O$. Hence, $\mathrm{ran}(W_{i,m})\subseteq {\mathrm{TAUT}}^O$. Furthermore, line 3 never evaluates to TRUE for inputs of the form $⟨x,\epsilon ⟩$, so line 12 is executed for all $x\in {\mathrm{\Sigma }}^{\ast }$ at least once, resulting in $\mathrm{ran}(W_{i,m}^O)\supseteq \mathrm{ran}(F^O)={\mathrm{TAUT}}^O$. Consequently, $\mathrm{ran}(W_{i,m}^O)={\mathrm{TAUT}}^O$. Together with $W_{i,m}^O$ running in polynomial time, we get that $W_{i,m}^O$ is a proof system for ${\mathrm{TAUT}}^O$. $◂$

By Lemma 18 and $P_b^O$ being a proof system for ${\mathrm{TAUT}}^O$, it follows that $W_{i,m}^O$ is also a proof system for ${\mathrm{TAUT}}^O$.

Let $p$ be a strictly monotone increasing polynomial bounding the runtime of the proof system $P_b^O$. Let $x$ be arbitrary such that line 3 evaluates to TRUE on input $⟨x,0^{p(|x|)}⟩$. Only finitely many $x$ do not satisfy this. Also by assumption, line 4 always evaluates to TRUE. Then for the input $⟨x,0^{p(|x|)}⟩$ line 5 evaluates to TRUE, because $P_b^O(x)$ halts in $\le p(|x|)$ steps. Hence, for all but finitely many $x$ it holds that $W_{i,m}(⟨x,0^{p(|x|)}⟩)=P_b^O(x)$. Consequently, $W_{i,m}^O$ has at most polynomially longer proofs than $P_b^O$, so $W_{i,m}^O$ simulates $P_b^O$. $◂$

During the construction of the oracle, we successively add requirements that we maintain. These are specified by a function $r:{\mathbb{N}}^{+}\times \mathbb{N}\times \mathbb{N}\mapsto \mathbb{N}$, called requirement function. Recall that $A\subseteq 1{\mathrm{\Sigma }}^{\ast }$ denotes an arbitrary base oracle. An oracle $w$ is $r$-valid for a requirement function $r$, if it satisfies the following requirements (let $i,j,m\in {\mathbb{N}}^{+}$):

1. V1

   $w\subseteq 0{\mathrm{\Sigma }}^{\ast }$ and $\mathrm{\#}(w\cap {\mathrm{\Sigma }}^n)\le 2$ for all $n\in {\mathbb{N}}^{+}$.

   (Meaning: $w\subseteq 2\mathbb{N}+1$ and $w$ is sparse.)

2. V2

   If $⟨0^i,0^m,0^n⟩\in w$ or $⟨1^i,1^m,1^n⟩\in w$ for some $n\in \mathbb{N}$, then $n>\mathrm{time}(J_i^{w\cup A}(\mathrm{fp}(⟨s_{i,m}⟩)))$.

   (Meaning: Codings for $W_{i,m}$ can not be queried during the simulation in line 2.)

3. V3

   If $r(i,0,0)=m>1$, then $⟨1^i,1^m,1^n⟩\notin w$ for all $n\in \mathbb{N}$.

   (Meaning: Here, $W_{i,m}$ commits to also return by line 6.)

4. V4

   If $r(i,j,0)=m>0$, then $\mathrm{\#}(w\cap {\mathrm{\Sigma }}^n)\le 1$ for all $n\in H_m$.

   (Meaning: $(A_m,B_m)$ is disjoint relative to $A$ combined with any extension of $w$.)

We will prove that V1, V2, V3 and V4 are satisfied for various oracles and requirement functions. To prevent confusion, we use the notation V1($w$), V2($w$), V3($w,r$) and V4($w,r$) to clearly state the referred oracle $w$ and requirement function $r$.

The oracle construction will take care of the following set of tasks $\{{\tau }_{i,j,k}\mid i\in {\mathbb{N}}^{+},j,k\in \mathbb{N}\}$ that are defined below. Let $𝒯$ be an enumeration of these tasks with the property that ${\tau }_{i,j,k}$ appears earlier than ${\tau }_{i,j,k+1}$. In each step we treat the smallest task in the order specified by $𝒯$, and after treating a task we remove it from $𝒯$.

In step $s=0$ we define $w_0≔\epsilon$ and $r_0$ as the nowhere defined requirement function. In step $s>0$ we define $w_s⋥w_{s-1}$ and $r_s⋥r_{s-1}$ such that $w_s$ is $r_s$-valid by treating the earliest task $\tau$ in $𝒯$ and removing it from $𝒯$. We do this according to the following procedure (let $i,j,k\in {\mathbb{N}}^{+}$):

Task ${\tau }_{i,0,0}$

1. 1.

   If there exists an $r_{s-1}$-valid partial oracle $v⋥w_{s-1}$ such that there are $a\in {\mathbb{N}}^{+}$ and $x\in {\mathrm{\Sigma }}^{\ast }$ with

   1. a.

      $P_a$ is a proof system for $\mathrm{TAUT}$ relative to $A$ combined with any fully defined $r_{s-1}$-valid extension of $v$,

   2. b.

      $J_i^{v\cup A}(a)=b$ is definite,

   3. c.

      $P_b^{v\cup A}(x)\notin {\mathrm{TAUT}}^{v\cup A}$ is definite,

   then define $w_s≔v$ and $r_s≔r_{s-1}\cup \{(i,0,0)\mapsto 0\}$.

   (Meaning: $J_i$ will not be a jump operator, because $J_i$ maps some code $a$ to some code $b$, while $P_a$ will be and $P_b$ will not be a proof system for $\mathrm{TAUT}$ relative to the final oracle.)

2. 2.

   Otherwise, if there exists an $a\in {\mathbb{N}}^{+}$ such that $J_i(a)$ never halts relative to $A$ combined with any $r_{s-1}$-valid partial extension of $w_{s-1}$, then define $w_s≔w_{s-1}0$ and $r_s≔r_{s-1}\cup \{(i,0,0)\mapsto 1\}$.

   (Meaning: $J_i$ will not be a recursive jump operator, because $J_i$ will not be total.)

3. 3.

   Otherwise,

   1. a.

      let $m≔|w_{s-1}|+2$,

   2. b.

      let $v^{\prime }⊒w_{s-1}$ be the smallest $r_{s-1}$-valid partial oracle such that $J_i^{v^{\prime }\cup A}(\mathrm{fp}(⟨s_{i,m}⟩))$ halts in less than $\Vert v^{\prime }\Vert$ steps,

   3. c.

      and let $v$ be an extension of $v^{\prime }$ via zeros such that $⟨0^i,0^m,0^{\Vert v^{\prime }\Vert }⟩\in v1$.

   Then define $w_s≔v1$ and $r_s≔r_{s-1}\cup \{(i,0,0)\mapsto m\}$.

   (Meaning: Choose a sufficiently large $m$ such that $w_{s-1}$ can not contain words of the form $⟨0^i,0^m,\cdot ⟩$ and let $w_s$ contain the permission such that $W_{i,m}$ can return by line 6, thereby ruling out $J_i$ as a jump operator. Statement 3b is possible since Case 2 failed.)

Task ${\tau }_{i,j,0}$

1. 1.

   If there exists an $r_{s-1}$-valid partial oracle $v⋥w_{s-1}$ such that there is an $x$ with $N_i^{v\cup A}(x)$ and $N_j^{v\cup A}(x)$ accept definitely, then define $w_s≔v$ and $r_s≔r_{s-1}\cup \{(i,j,0)\mapsto 0\}$. Remove all tasks ${\tau }_{i,j,k}$ with $k\in {\mathbb{N}}^{+}$ from $𝒯$.

   (Meaning: The pair $(L(N_i),L(N_j))$ is not disjoint.)

2. 2.

   Otherwise, define $w_s≔w_{s-1}0$ and $r_s≔r_{s-1}\cup \{(i,j,0)\mapsto |w_s|+2\}$.

   (Meaning: Assign the pair $(L(N_i),L(N_j))$ some witness pair $(A_{|w_s|+2},B_{|w_s|+2})$ and promise to keep the witness-pair disjoint.)

Task ${\tau }_{i,j,k}$

1. 1.

   Let $m≔r_{s-1}(i,j,0)$ and let $v⊒w_{s-1}$ be $r_{s-1}$-valid such that $\Vert v\Vert =0^n$ with $n\in H_m$ and $2^{n-2}>6{(p_{i+j}(p_k(n)))}^2+1$. Choose

   1. a.

      either $z\in 00{\mathrm{\Sigma }}^{n-2}$ such that $N_i^{v\cup \{z\}\cup A}(F_k^{v\cup \{z\}\cup A}(0^n))$ rejects

   2. b.

      or $z\in 01{\mathrm{\Sigma }}^{n-2}$ such that $N_j^{v\cup \{z\}\cup A}(F_k^{v\cup \{z\}\cup A}(0^n))$ rejects.

   Then define $r_s≔r_{s-1}\cup \{(i,j,k)\mapsto 0\}$ and define $w_s⊒v$ such that it contains the same words as $v\cup \{z\}$ and $\Vert w_s\Vert =2p_{i+j}(p_k(n))+1$.

   (Meaning: The witness pair $(A_m,B_m)$ is not reducible to $(L(N_i),L(N_j))$ via $F_k$. It must be shown that $z$ can be chosen as stated. Intuitively, this follows from $r_{s-1}(i,j,0)\ne 0$.)