P-Optimal Proof Systems for Each NP-Complete Set but no Complete Disjoint NP-Pairs Relative to an Oracle
Titus Dose

TL;DR
This paper constructs an oracle demonstrating that certain proof complexity conjectures, including the non-existence of complete disjoint NP-pairs and P-optimal proof systems for NP-complete sets, cannot be proven relativistically.
Contribution
It provides a relativized separation showing that these conjectures are independent of relativizable proof techniques.
Findings
An oracle where disjoint NP-pairs are not complete.
An oracle where NP does not have P-optimal proof systems.
An oracle where NP∩coNP lacks complete problems.
Abstract
Pudl\'ak [Pud17] lists several major conjectures from the field of proof complexity and asks for oracles that separate corresponding relativized conjectures. Among these conjectures are: - : The class of all disjoint NP-pairs does not have many-one complete elements. - : NP does not contain many-one complete sets that have P-optimal proof systems. - : UP does not have many-one complete problems. - : does not have many-one complete problems. As one answer to this question, we construct an oracle relative to which , , , and hold, i.e., there is no relativizable proof for the implication . In particular,…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
P-Optimal Proof Systems for Each NP-Complete Set
but no Complete Disjoint NP-Pairs Relative to an Oracle
Titus Dose
Julius-Maximilians-Universität Würzburg
?abstractname?
Pudlák [Pud17] lists several major conjectures from the field of proof complexity and asks for oracles that separate corresponding relativized conjectures. Among these conjectures are:
- •
: The class of all disjoint NP-pairs does not have many-one complete elements.
- •
: NP does not contain many-one complete sets that have P-optimal proof systems.
- •
: UP does not have many-one complete problems.
- •
: does not have many-one complete problems.
As one answer to this question, we construct an oracle relative to which , , , and hold, i.e., there is no relativizable proof for the implication . In particular, regarding the conjectures by Pudlák this extends a result by Khaniki [Kha19].
1 Introduction
The main motivation for the present paper is an article by Pudlák [Pud17] that is “motivated by the problem of finding finite versions of classical incompleteness theorems”, investigates major conjectures in the field of proof complexity, discusses their relations, and in particular draws new connections between the conjectures. Among others, Pudlák conjectures the following assertions (note that within the present paper all reductions are polynomial-time-bounded):
- •
(resp., ): (resp., ) does not contain many-one complete sets that have P-optimal proof systems
- •
: does not contain many-one complete sets that have optimal proof systems,
(note that is the non-uniform version of )
- •
(resp., ): The class of all disjoint -pairs (resp., -pairs) does not have many-one complete elements,
- •
: The class of all total polynomial search problems does not have complete elements,
- •
(resp., ): (resp., , the class of problems accepted by machines with at most one accepting path for each input) does not have many-one complete elements.
The following figure contains the conjectures by Pudlák and illustrates the state of the art regarding (i) known implications and (ii) separations in terms of oracles that prove the non-existence of relativizable proofs for implications. denotes the oracle constructed in the present paper.
The main conjectures of [Pud17] are and . Let us give some background on these conjectures (for details we refer to [Pud13]) and on the notion of disjoint pairs. The first main conjecture refers to the notion of proof systems introduced by Cook and Reckhow [CR79], who define a proof system for a set to be a polynomial-time computable function whose range is .
The subsequent paragraph is due to [DG19] and explains a logical characterization of and . has an interesting connection to some finite version of an incompleteness statement. Denote by the finite consistency of a finitely axiomatized theory , i.e., is the statement that has no proofs of contradiction of length . Krajíček and Pudlák [KP89] raise the conjectures and and show that the latter is equivalent to the statement that there is no finitely axiomatized theory which proves the finite consistency for every finitely axiomatized theory by a proof of polynomial length in . In other words, expresses that a weak version of Hilbert’s program (to prove the consistency of all mathematical theories) is possible [Pud96]. Correspondingly, is equivalent to the existence of a theory such that, for each fixed finitely axiomatized theory , proofs of in can be constructed in polynomial time in [KP89].
The conjecture , raised by Megiddo and Papadimitriou [MP91], is implied by the non-existence of disjoint coNP-pairs [BKM09, Pud17], and implies that no NP-complete set has P-optimal proof systems [BKM09, Pud17]. It states the non-existence of total polynomial search problems that are complete with respect to polynomial reductions, where a total polynomial search problem (i) is represented by a polynomial and a binary relation satisfying and (ii) is the following computational task: On input compute some with . In other words, total polynomial search problems are represented by nondeterministic multivalued functions with values that are polynomially verifiable and guaranteed to exist [MP91].
The notion of disjoint NP-pairs, i.e., pairs with and , has its origin in public-key cryptography and characterizes promise problems [EY80, ESY84, GS88]. Razborov [Raz94] connects disjoint pairs with the concept of propositional proof systems (pps), i.e., proof systems for the set of propositional tautologies TAUT, defining for each pps a disjoint NP-pair, the so-called canonical pair of , and showing that the canonical pair of a P-optimal pps is complete. Hence, putting it another way, , which Köbler, Messner, and Torán [KMT03] extend to .
In contrast to the many implications only very few oracles were known separating two of the relativized conjectures [Pud17], which is why Pudlák asks for further oracles showing relativized conjectures to be different.
Khaniki [Kha19] partially answers this question: besides showing two of the conjectures to be equivalent he presents two oracles and showing that and (as well as and ) are independent in relativized worlds which means that none of the two possible implications between the two conjectures has a relativizable proof. To be more precise, relative to , there exist P-optimal propositional proof systems but no many-one complete disjoint coNP-pairs, where —as mentioned above— the latter implies and . Relative to , there exist no P-optimal propositional proof systems and each total polynomial search problem has a polynomial-time solution, where the latter implies [KM00].
Dose and Glaßer [DG19] construct an oracle that also separates some of the above relativized conjectures. Relative to there exist no many-one complete disjoint -pairs, has many-one complete problems, and has no many-one complete problems. In particular, relative to , there do not exist P-optimal propositional proof systems. Thus, among others, shows that the conjectures and as well as and cannot be proven equivalent with relativizable proofs.
Our Contribution.
In the present paper we construct an oracle relative to which
The class of all disjoint NP-pairs does not have many-one complete elements. 2. 2.
Each many-one complete set for has P-optimal proof systems. 3. 3.
UP does not contain many-one complete problems. 4. 4.
does not contain many-one complete problems.
Indeed, relative to there even exist no disjoint -pairs that are hard for , which implies both 1 and 4. Figure 1 illustrates that yields one of the strongest oracle results that Pudlák [Pud17] asks for since , , and are the strongest conjectures in their respective branches in Figure 1 whereas is the weakest conjecture that is not relativizably implied by the three other conjectures.
Among others, the oracle shows that there are no relativizable proofs for the implications and . Let us now focus on the properties 1 and 2 of the oracle. Regarding these, our oracle has similar properties as the aforementioned oracle by Khaniki [Kha19]: both oracles show that there is no relativizable proof for the implication . Relative to Khaniki’s oracle it even holds that each total polynomial search problem has a polynomial time solution, which implies not only but also that all optimal proof systems for SAT are P-optimal [KM00]. Regarding Pudlák’s conjectures, however, our oracle extends Khaniki’s result as relative to we have the even stronger result that there is no relativizable proof for the implication . Since due to the oracle by Khaniki [Kha19] none of the implications , , and can be proven relativizably, our oracle shows that is independent of each of the conjectures , , and in relativized worlds, i.e., none of the six possible implications has a relativizable proof.
2 Preliminaries
Throughout this paper let be the alphabet . We denote the length of a word by . Let for . The empty word is denoted by and the -th letter of a word for is denoted by , i.e., . If is a prefix of , i.e., and for all , then we write or . If and , then we write v\mathrel{\sqsubseteq\kern-9.19998pt\raise-1.49994pt\hbox{\rotatebox{313.0}{\scalebox{1.1}[0.75]{\shortmid}}}\scalebox{0.3}[1.0]{\ }}w or w\mathrel{\sqsupseteq\kern-9.19998pt\raise-1.49994pt\hbox{\rotatebox{313.0}{\scalebox{1.1}[0.75]{\shortmid}}}\scalebox{0.3}[1.0]{\ }}v. For each finite set , let \ell(Y)\mathop{=}\limits^{\mbox{\raisebox{-0.45206pt}[0.0pt][0.0pt]{\scriptscriptstyle df}}}\sum_{w\in Y}|w|.
denotes the set of integers, denotes the set of natural numbers, and . The set of primes is denoted by and denotes the set . Moreover, (resp., ) denotes the set of all primes of the form (resp., ) for .
We identify with via the polynomial-time computable, polynomial-time invertible bijection , which is a variant of the dyadic encoding. Hence, notations, relations, and operations for are transferred to and vice versa. In particular, denotes the length of . We eliminate the ambiguity of the expressions and by always interpreting them over .
Let be an injective, polynomial-time computable, polynomial-time invertible pairing function such that .
Given two sets and , denotes the set difference between and , i.e., . The complement of a set relative to the universe is denoted by . The universe will always be apparent from the context. Furthermore, the symmetric difference is denoted by , i.e., for arbitrary sets and .
The domain and range of a function are denoted by and , respectively.
, , and denote standard complexity classes [Pap94]. Define for a class . is the class of all problems accepted by nondeterministic polynomial-time Turing machines that on each input have at most one accepting path. If (resp., ) and , then we call a disjoint -pair (resp., a disjoint -pair). The set of all disjoint -pairs (resp., -pairs) is denoted by (resp., ).
We also consider all these complexity classes in the presence of an oracle and denote the corresponding classes by , , , and so on.
Let be a Turing machine. denotes the computation of on input with as an oracle. For an arbitrary oracle we let , where as usual in case is nondeterministic, the computation accepts if and only if it has at least one accepting path.
For a deterministic polynomial-time Turing transducer (i.e., a Turing machine computing a function), depending on the context, either denotes the computation of on input with as an oracle or the output of this computation.
Definition 2.1
A sequence is called standard enumeration of nondeterministic, polynomial-time oracle Turing machines, if it has the following properties:
All are nondeterministic, polynomial-time oracle Turing machines. 2. 2.
For all oracles and all inputs the computation stops within steps. 3. 3.
For every nondeterministic, polynomial-time oracle Turing machine there exist infinitely many such that for all oracles it holds that . 4. 4.
*There exists a nondeterministic, polynomial-time oracle Turing machine such that for all oracles and all inputs it holds that nondeterministically simulates the computation . *
Analogously we define standard enumerations of deterministic, polynomial-time oracle Turing transducers.
Throughout this paper, we fix some standard enumerations. Let be a standard enumeration of nondeterministic polynomial-time oracle Turing machines. Then for every oracle , the sequence represents an enumeration of the languages in , i.e., . Let be a standard enumeration of polynomial time oracle Turing transducers.
By the properties of standard enumerations, for each oracle the problem
[TABLE]
is -complete (in particular it is in ).
In the present article we only use polynomial-time-bounded many-one reductions. Let be an oracle. For problems we write (resp., ) if there exists (resp., ) with . In this case we say that is polynomially many-one reducible to . Now let such that . In this paper we always use the following reducibility for disjoint pairs [Raz94]. is polynomially many-one reducible to , denoted by , if there exists with and . If , then we also write instead of .
We say that is -hard (-complete) for if for all (and ). Moreover, a pair is -hard for if for every .
Definition 2.2** ([CR79])**
A function is called proof system for the set . For we say that is simulated by (resp., is -simulated by ) denoted by (resp., ), if there exists a function (resp., a function ) and a polynomial such that and for all . A function is optimal (resp., -optimal), if (resp., ) for all with . Corresponding relativized notions are obtained by using , , and in the definitions above.
The following proposition states the relativized version of a result by Köbler, Messner, and Torán [KMT03], which they show with a relativizable proof.
Proposition 2.3** ([KMT03])**
For every oracle , if has a -optimal (resp., optimal) proof system and , then has a -optimal (resp., optimal) proof system.
Corollary 2.4
For every oracle , if there exists a -complete that has a -optimal (resp., optimal) proof system, then all sets in have -optimal (resp., optimal) proof systems.
Let us introduce some (partially quite specific) notations that are designed for the construction of oracles [DG19]. The support of a real-valued function is the subset of the domain that consists of all values that does not map to 0. We say that a partial function is injective on its support if for implies . If a partial function is not defined at point , then denotes the extension of that at has value .
If is a set, then denotes the characteristic function at point , i.e., is if , and [math] otherwise. An oracle is identified with its characteristic sequence , which is an -word. In this way, denotes both, the characteristic function at point and the -th letter of the characteristic sequence, which are the same. A finite word describes an oracle that is partially defined, i.e., only defined for natural numbers . We can use instead of the set and write for example , where and are sets. For nondeterministic oracle Turing machines we use the following phrases: a computation definitely accepts, if it contains a path that accepts and all queries on this path are . A computation definitely rejects, if all paths reject and all queries are .
For a nondeterministic Turing machine we say that the computation is defined, if it definitely accepts or definitely rejects. For a polynomial-time oracle transducer , the computation is defined if all queries are .
3 Oracle Construction
The following lemma is a slightly adapted variant of a result from [DG19].
Lemma 3.1
For all and all it holds .
**Proof ** We may assume for suitable and , since otherwise, and . For each that is queried within the first steps of or it holds that and thus, . Hence, these queries are answered the same way relative to and , showing that accepts within steps if and only if accepts within steps.
Theorem 3.2
There exists an oracle such that the following statements hold:
- •
* does not contain pairs that are -hard for .*
- •
Each has -optimal proof systems.
- •
* does not contain -complete problems.*
The following Corollary immediately follows from Theorem 3.2.
Corollary 3.3
There exists an oracle such that the following statements hold:
- •
* does not contain -complete pairs.*
- •
Each has -optimal proof systems.
- •
* does not contain -complete problems.*
- •
* does not contain -complete problems.*
Proof of Theorem 3.2 Let be a (possibly partial) oracle and (resp., ). Recall and . We define
[TABLE]
Note that and if for each . In that case . Moreover, if for each .
For the sake of simplicity, let us call a pair an -machine if . Note that throughout this proof we sometimes omit the oracles in the superscript, e.g., we write or instead of or . However, we do not do that in the “actual” proof but only when explaining ideas in a loose way in order to give the reader the intuition behind the occasionally very technical arguments.
Preview of construction. We sketch some of the very basic ideas our construction uses.
For all positive the construction tries to achieve that is not an -machine. If this is not possible, then inherently is an -machine. Once we know this, we choose some odd prime and diagonalize against all -functions such that and is not -reducible to . 2. 2.
For all the construction intends to make sure that is not a proof system for . If this is not possible, then inherently is a proof system for . Then we start to encode the values of into the oracle. However, it is important to also allow encodings for functions that are not known to be proof systems for yet. Regarding the P-optimal proof systems, our construction is based on ideas by Dose and Glaßer [DG19]. 3. 3.
For all the construction tries to ensure that is not a -machine. In case this is impossible, we know that inherently is a -machine, which enables us to diagonalize against all -functions making sure that for some that we choose is not reducible to .
For and we write . Note that is even and (cf. the properties of the pairing function ).
Claim 3.4
Let be an oracle, , and such that . Then the following holds.
* is defined and .* 2. 2.
* for all .*
**Proof ** As the running time of is bounded by , the computation is defined and its output is less than . Hence, 1 holds. Consider 2. It suffices to show that for all and all . This holds by Lemma 3.1.
During the construction we maintain a growing collection of requirements that is represented by a partial function belonging to the set
[TABLE]
A partial oracle is called -valid for if it satisfies the following properties.
- V1
For all and all , if , then .
(meaning: if the oracle contains the codeword , then outputs and ; hence, is a proof for )
- V2
For all distinct , if , then there exists such that and definitely accept.
(meaning: for every extension of the oracle, is not a disjoint NP-pair.)
- V3
For all distinct with for some and each , it holds (i) and (ii) if is defined for all words of length , then .
(meaning: if , then ensure that (i.e., ) relative to the final oracle.)
- V4
For all with , there exists such that is defined and for all .
(meaning: for every extension of the oracle, is not a proof system for )
- V5
For all and with , it holds .
(meaning: if , then from on, we encode the values of into the oracle.
Note that V5 is not in contradiction with e.g. V3 or V7 as is even.)
- V6
For all with , there exists such that is defined and has two accepting paths.
(meaning: for every extension of the oracle, is not a -machine.)
- V7
For all with and each , it holds .
(meaning: if , ensure that is in .)
The subsequent claim follows directly from the definition of -valid.
Claim 3.5
Let such that is an extension of . For all oracles , if is -valid, then is -valid.
Claim 3.6
Let and be oracles such that and both and are -valid. Then is -valid.
**Proof ** satisfies V2, V4, and V6 since satisfies these conditions. Moreover, satisfies V3 and V7 as satisfies these conditions.
Let and such that . Then and as is -valid, we obtain by V1 that . Claim 3.4 yields that is defined and . This yields that and . Thus, satisfies V1.
Now let and such that . Again, by Claim 3.4, is defined and thus, . As and is -valid, we obtain by V5 that . Since and , we obtain , which shows that satisfies V5.
Oracle construction. Let be an enumeration of having the property that appears earlier than for all (more formally, could be defined as a function ). Each element of stands for a task. We treat the tasks in the order specified by and after treating a task we remove it and possibly other tasks from . We start with the nowhere defined function and the -valid oracle . Then we define functions in such that is an extension of and partial oracles w_{0}\mathrel{\sqsubseteq\kern-9.19998pt\raise-1.49994pt\hbox{\rotatebox{313.0}{\scalebox{1.1}[0.75]{\shortmid}}}\scalebox{0.3}[1.0]{\ }}w_{1}\mathrel{\sqsubseteq\kern-9.19998pt\raise-1.49994pt\hbox{\rotatebox{313.0}{\scalebox{1.1}[0.75]{\shortmid}}}\scalebox{0.3}[1.0]{\ }}w_{2}\mathrel{\sqsubseteq\kern-9.19998pt\raise-1.49994pt\hbox{\rotatebox{313.0}{\scalebox{1.1}[0.75]{\shortmid}}}\scalebox{0.3}[1.0]{\ }}\dots such that each is -valid. Finally, we choose (note that is totally defined since in each step we will strictly extend the oracle). We describe step , which starts with some and a -valid oracle and chooses an extension of and a -valid w_{s}\mathrel{\sqsupseteq\kern-9.19998pt\raise-1.49994pt\hbox{\rotatebox{313.0}{\scalebox{1.1}[0.75]{\shortmid}}}\scalebox{0.3}[1.0]{\ }}w_{s-1} (it will be argued later that all these steps are indeed possible). Let us recall that each task is immediately deleted from after it is treated.
- •
task : Let . If there exists a -valid v\mathrel{\sqsupseteq\kern-9.19998pt\raise-1.49994pt\hbox{\rotatebox{313.0}{\scalebox{1.1}[0.75]{\shortmid}}}\scalebox{0.3}[1.0]{\ }}w_{s-1}, then let and be the least -valid, partial oracle \mathrel{\sqsupseteq\kern-9.19998pt\raise-1.49994pt\hbox{\rotatebox{313.0}{\scalebox{1.1}[0.75]{\shortmid}}}\scalebox{0.3}[1.0]{\ }}w_{s-1}. Otherwise, let and choose with such that is -valid.
(meaning: try to ensure that is not a proof system for . If this is impossible, require that from now on the values of are encoded into the oracle.)
- •
task with : Let . If there exists a -valid v\mathrel{\sqsupseteq\kern-9.19998pt\raise-1.49994pt\hbox{\rotatebox{313.0}{\scalebox{1.1}[0.75]{\shortmid}}}\scalebox{0.3}[1.0]{\ }}w_{s-1}, then let , define to be the least -valid, partial oracle \mathrel{\sqsupseteq\kern-9.19998pt\raise-1.49994pt\hbox{\rotatebox{313.0}{\scalebox{1.1}[0.75]{\shortmid}}}\scalebox{0.3}[1.0]{\ }}w_{s-1}, and delete all tasks from . Otherwise, let , choose some greater than and all with and , let , and choose with such that is -valid.
(meaning: try to ensure that is not a disjoint NP-pair. If this is impossible, choose a sufficiently large prime . It will be made sure later that cannot be reduced to .)
- •
task with : It holds for a prime , since otherwise, this task would have been deleted in the treatment of task . Define and choose a -valid w_{s}\mathrel{\sqsupseteq\kern-9.19998pt\raise-1.49994pt\hbox{\rotatebox{313.0}{\scalebox{1.1}[0.75]{\shortmid}}}\scalebox{0.3}[1.0]{\ }}w_{s-1} such that for some one of the following two statements holds:
- –
for all and definitely rejects.
- –
for all and definitely rejects.
(meaning: make sure that it does not hold via . Due to V3 it will hold relative to the final oracle and hence, it will not hold via .
- •
task : Let . If there exists a -valid v\mathrel{\sqsupseteq\kern-9.19998pt\raise-1.49994pt\hbox{\rotatebox{313.0}{\scalebox{1.1}[0.75]{\shortmid}}}\scalebox{0.3}[1.0]{\ }}w_{s-1}, then let , define to be the least -valid, partial oracle \mathrel{\sqsupseteq\kern-9.19998pt\raise-1.49994pt\hbox{\rotatebox{313.0}{\scalebox{1.1}[0.75]{\shortmid}}}\scalebox{0.3}[1.0]{\ }}w_{s-1}, and delete all tasks from . Otherwise, let , choose some greater than both and all with and , let , and choose with such that is -valid.
(meaning: try to ensure that is not a -machine. If this is impossible, choose a sufficiently large prime . It will be made sure later that cannot be reduced to .)
- •
task : It holds for a prime , since otherwise, this task would have been deleted in the treatment of task . Define and choose a -valid w_{s}\mathrel{\sqsupseteq\kern-9.19998pt\raise-1.49994pt\hbox{\rotatebox{313.0}{\scalebox{1.1}[0.75]{\shortmid}}}\scalebox{0.3}[1.0]{\ }}w_{s-1} such that for some one of the following conditions holds:
- –
for all and definitely rejects.
- –
for all and definitely accepts.
(meaning: make sure that it does not hold via .)
Observe that is always chosen in a way such that it is in . We now show that the construction is possible. For that purpose, we first describe how a valid oracle can be extended by one bit such that it remains valid.
Claim 3.7
Let and be a -valid oracle with . It holds for :
If for and , , and , then is defined and for all . 2. 2.
There exists such that is -valid. In detail, the following statements hold.
- (a)
If is odd and for all and with it holds , then and are -valid. 2. (b)
If there exist and with such that , , and , then and are -valid. 3. (c)
If there exist and with such that and , then is -valid. 4. (d)
If there exist and with such that and , then and are -valid. 5. (e)
If for and , , and , then is -valid and . 6. (f)
If for and , at least one of the three conditions (i) undefined, (ii) , and (iii) holds, and , then and are -valid. 7. (g)
In all other cases (i.e., none of the assumptions in (2a)–(2f) holds) is -valid.
**Proof **
By Claim 3.4, is defined. Assume that for it holds for and , , and . Let be the step where the task is treated (note as is defined). By Claim 3.5, is -valid. Moreover, by Claim 3.4, for all . Thus, is -valid for , which is why the construction would have chosen , in contradiction to . Hence, and by Claim 3.4, it even holds for all . This shows statement 1. 2. 2.
We first show the following assertions.
[TABLE]
(1) and (2): Let and such that . Then, as is -valid, by V1, and by Claim 3.4, is defined and for all . Hence, in particular, for all . This shows (1). For the proof of (2) it remains to consider . In case (ii) satisfies V1 as is odd and each has even length. Consider case (i), i.e., for and with . Then by Claim 3.4, , which shows (2).
(3) and (4): Let and such that . Then by Claim 3.4, is defined and thus, for all . As is -valid, it holds and hence, for all . This shows (4). In order to finish the proof for (3), it remains to consider . Assume for some with (otherwise, clearly satisfies V5). If (ii) or (iii) is wrong, then satisfies V5. If (iv) is wrong, then . By Claim 3.4, this computation is defined and hence, , which is why satisfies V5. This shows (3).
Let us now prove the assertions (2a)–(2g) and note that we do not have to consider V2,V4, and V6 as these conditions are not affected by extending a -valid oracle.
- (a)
By (1) and (2), the oracles and satisfy V1. By (3) and (4), the oracles and satisfy V5 (for the application of (3) recall that each has even length and hence, for all condition (i) does not hold). V3 and V7 are not affected as for all primes with and all . 2. (b)
By (1), (2), (3), and (4), the oracles and satisfy V1 and V5 (for the application of (3) recall that each has even length and hence, for all condition (i) does not hold). As , V7 is satisfied by and . Moreover, satisfies V3 as due to the oracle is not defined for all words of length . Finally, satisfies V3 since . 3. (c)
By (2) and (4), the oracle satisfies V1 and V5. As , V7 is satisfied by . Moreover, as , it holds and hence, satisfies V3. 4. (d)
By (1), (2), (3), and (4), the oracles and satisfy V1 and V5 (for the application of (3) recall that each has even length and hence, for all condition (i) does not hold). As , the oracles and satisfy V3. Finally, trivially satisfies V7 and satisfies V7 as . 5. (e)
By (4), the oracle satisfies V5. By statement 1 of the current claim, is defined and for all . Hence, (2) can be applied, satisfies V1, and . As is even, trivially satisfies V3 and V7. 6. (f)
By (1), satisfies V1. By (2), satisfies V1. By (3), satisfies V5. By (4), satisfies V5. As is even, both and satisfy V3 and V7. 7. (g)
By (1), satisfies V1. Moreover, (3) can be applied since otherwise, there would exist with such that conditions (i)–(iv) of the assertion (3) hold and then we were in case 2(e). Hence, satisfies V5. Trivially, satisfies V7 and finally, satisfies V3 as the only way could hurt V3 is that for some with and as well as , but this case is treated in 2(c).
This finishes the proof of Claim 3.7.
In order to show that the above construction is possible, assume that it is not possible and let be the least number, where it fails.
If step treats a task , then is not defined, since the value of is defined in the unique treatment of the task . If is chosen to be 0, then the construction clearly is possible. Otherwise, due to the (sufficiently large) choice of , the -valid oracle is even -valid and Claim 3.7.2 ensures that there exists a -valid for some . Hence, the construction does not fail in step , a contradiction.
For the remainder of the proof that the construction above is possible we assume that step treats a task . We treat the cases and simultaneously whenever it is possible. Recall that in the case we work for the diagonalization ensuring that is not a complete -set and in the case we work for the diagonalization ensuring that the pair is not hard for .
In both cases, and for some (recall if and if ). Let and choose for some such that
[TABLE]
and is not defined for any words of length . Note that is not less than the running time of each of the computations and for each oracle .
We define to be the minimal -valid oracle that is defined for all words of length . Such an oracle exists by Claim 3.7.2.
Moreover, for , let u_{z}\mathrel{\sqsupseteq\kern-9.19998pt\raise-1.49994pt\hbox{\rotatebox{313.0}{\scalebox{1.1}[0.75]{\shortmid}}}\scalebox{0.3}[1.0]{\ }}u be the minimal -valid oracle with that is defined for all words of length . Such an oracle exists by Claim 3.7.2: first, starting from we extend the current oracle bitwise such that (i) it remains -valid, (ii) it is defined for precisely the words of length , and (iii) its intersection with equals . This is possible by (2b, 2c, and 2g) or (2d and 2g) of Claim 3.7 depending on whether or . Then by Claim 3.7.2, the current oracle can be extended bitwise without losing its -validity until it is defined for all words of length .
Claim 3.8
Let .
For each one of the following statements holds.
- •
* for some with and some .*
- •
* for some and with , , and .* 2. 2.
For all with and all , if , then .
**Proof **
Let . Moreover, let be the prefix of that has length , i.e., is the least word that is not defined for. In particular, it holds and thus, . As and both and are -valid, Claim 3.6 yields that is also -valid.
Let us apply Claim 3.7.2 to the oracle . If one of the cases 2a, 2b, 2d, 2f, and 2g can be applied, then is -valid and can be extended to a -valid oracle with by Claim 3.7.2. As and agree on all words and , we obtain and due to we know that . This is a contradiction to the choice of (recall that is the minimal -valid oracle that is defined for all words of length and that satisfies ).
Hence, none of the cases 2a, 2b, 2d, 2f, and 2g of Claim 3.7 can be applied, i.e., either (i) for some and with or (ii) for , , , and . In the latter case Claim 3.7.1 shows that is defined and for all , which implies . 2. 2.
As , is -valid, and is defined for all words of length , V3 yields that there exists . Let be the minimal element of . It suffices to show . For a contradiction, we assume . Let be the prefix of that is defined for exactly the words of length . Then and both and are -valid. Hence, by Claim 3.6, the oracle is -valid as well.
By Claim 3.7.2, can be extended to a -valid oracle that satisfies and . Then . As the oracles and agree on all words smaller than , we have and , in contradiction to the choice of (again, recall that is the minimal -valid oracle that is defined for all words of length and that satisfies ).
This finishes the proof of Claim 3.8.
Let us study the case that for some odd (resp., even) the computation (resp., if is even) rejects. Then it even definitely rejects since is defined for all words of length . If , then and since , we have for all (resp., for all if is even). Analogously, if , then and as , we have for all . Hence, in all these cases we can choose and obtain a contradiction to the assumption that step of the construction fails in treating the task . Therefore, for the remainder of the proof that the construction is possible we assume the following:
- •
For each odd the computation definitely accepts.
- •
For each even the computation definitely accepts.
Note that in case we could have also formulated the two conditions equivalently in the following simpler way: for each the computation definitely accepts. Recall, however, that as far as possible we consider the cases and simultaneously.
Let for odd (resp., even) be the set of all those oracle queries of the least accepting path of (resp., ) that are of length . Observe . Moreover, define and for ,
[TABLE]
Let . Note that all words in have length . Moreover, note that for for some it does not necessarily hold and therefore, it might be that the computation (in the notation used in the equation above) does not have any accepting paths. In that case the second of the two sets in the equation above is empty.
Claim 3.9
For all , and the length of each word in is .
**Proof ** We show that for all , . Then for all implies . Moreover, from and the second part of the claim follows.
Let and consider an arbitrary element of . If is not of the form for and , then generates no elements in . Assume for and with for and . The computation runs for at most steps, where “” holds by the definition of and the properties of the pairing function . Hence, the set of queries of satisfies .
Moreover, the computation runs for less than steps (for “” we refer again to the definition of and the properties of the pairing function ). Hence, for the set of queries of the least accepting path of the computation (if such a path exists) we have .
Consequently,
[TABLE]
which finishes the proof of Claim 3.9.
For we say that and conflict if there is a word which is in . In that case, we say and conflict in . Note that whenever and conflict in a word , then and .
The next five claims are dedicated to the purpose of proving that for each odd and each even , the sets and conflict in a word of length . Indeed, then and conflict in one of the words and as these are the only words of length in .
Claim 3.10
Let such that is odd and is even. If and conflict, then they conflict in a word of length .
**Proof ** Let be the least word in which and conflict (note that due to and Claim 3.9). Then . By symmetry, it suffices to consider the case . For a contradiction, assume that . Then by Claim 3.8, two situations are possible.
Assume for with and . Then by Claim 3.8.2, , a contradiction. Hence, for all with and . 2. 2.
Here, for and with and . By construction, . Thus, , since otherwise, by the -validity of and V5, it would hold . Consequently, . Hence, there exists a query that is asked by both and and that is in (otherwise, both computations would output the same word). By definition of and , it holds . Hence, and conflict in and , in contradiction to the assumption that is the least word which and conflict in.
In both cases we obtain a contradiction. Thus, the proof is complete.
We want to show next that for all odd and all even the sets and indeed conflict. For the proof of this we need three more claims. We will make use of the next claim several times. In some cases a weaker version of this claim is sufficient. For better readability, we formulate this weaker statement in a separate claim (Claim 3.12).
Claim 3.11
Let for some and such that and do not conflict. For each -valid oracle v\mathrel{\sqsupseteq\kern-9.19998pt\raise-1.49994pt\hbox{\rotatebox{313.0}{\scalebox{1.1}[0.75]{\shortmid}}}\scalebox{0.3}[1.0]{\ }}u that is defined for exactly the words of length and that satisfies for all and for all , there exists a -valid oracle v^{\prime}\mathrel{\sqsupseteq\kern-9.19998pt\raise-1.49994pt\hbox{\rotatebox{313.0}{\scalebox{1.1}[0.75]{\shortmid}}}\scalebox{0.3}[1.0]{\ }}v with , for all , and for all .
The following claim follows immediately from Claim 3.11 when we choose and (trivially, for no the set conflicts with itself).
Claim 3.12
Let . For each -valid oracle v\mathrel{\sqsupseteq\kern-9.19998pt\raise-1.49994pt\hbox{\rotatebox{313.0}{\scalebox{1.1}[0.75]{\shortmid}}}\scalebox{0.3}[1.0]{\ }}u that is defined for exactly the words of length and that satisfies for all , there exists a -valid oracle v^{\prime}\mathrel{\sqsupseteq\kern-9.19998pt\raise-1.49994pt\hbox{\rotatebox{313.0}{\scalebox{1.1}[0.75]{\shortmid}}}\scalebox{0.3}[1.0]{\ }}v with and for all .
Proof of Claim 3.11 Let with , for all , and for all . Moreover, let , i.e., is the least word that is not defined for. It suffices to show the following:
- •
If for some with and , then there exists a -valid w^{\prime}\mathrel{\sqsupseteq\kern-9.19998pt\raise-1.49994pt\hbox{\rotatebox{313.0}{\scalebox{1.1}[0.75]{\shortmid}}}\scalebox{0.3}[1.0]{\ }}w that is defined for the words of length , undefined for all words of greater length, and that satisfies for all and for all .
Note that in this case since is defined for exactly the words of length .
- •
If for all with and all the word is not of length , then there exists such that is -valid, for all and for all .
We study three cases.
Assume for some with and . Then we let w^{\prime}\mathrel{\sqsupseteq\kern-9.19998pt\raise-1.49994pt\hbox{\rotatebox{313.0}{\scalebox{1.1}[0.75]{\shortmid}}}\scalebox{0.3}[1.0]{\ }}w be the minimal oracle that is defined for all words of length and contains , i.e., when interpreting the oracles as sets. As by Claim 3.8.2, we obtain for all and for all . Moreover, if , then is -valid by Claim 3.7.2b and Claim 3.7.2c. If , then is -valid by Claim 3.7.2a. 2. 2.
Now assume that for and with . Let us first assume that . Then there exists such that is -valid (cf. Claim 3.7.2) and clearly for all and for all .
From now on we assume . By symmetry, it suffices to consider the case . We study two cases.
- (a)
If , then by V1, . As all queries of are in and due to satisfy , it holds . Similarly, we obtain : If for and , then by the computation has an accepting path and all queries of the least accepting path of this computation are in and due to satisfy . Hence, accepts and . Let us choose . Note that is not necessarily defined. If is defined, then and we can apply Claim 3.7.2e and obtain that is -valid. If is undefined, then we can apply Claim 3.7.2f and obtain that is -valid. Clearly for all . In order to see that also for all , it is sufficient to show that \big{(}\alpha\in Q(U_{z^{\prime}})\Rightarrow\alpha\in u_{z^{\prime}}\big{)}. But this holds since otherwise, and conflict. 2. (b)
Assume . Then by V5, . As all queries of are in and due to satisfy , it holds . Choose . Then by Claim 3.7.2g, is -valid and clearly for all . In order to see for all , it suffices to argue for . If , then as otherwise, and would conflict. 3. 3.
We now consider the remaining cases, i.e., we may assume
- •
is not of length for all with and all and
- •
for all and with .
In this case, it holds by Claim 3.8.1. We choose and obtain that for all and for all . Moreover, by Claim 3.7.2, is -valid.
This finishes the proof of Claim 3.11.
Claim 3.13
For all it holds .
**Proof ** For a contradiction, assume for some . We study the cases and separately.
First assume . In this case . Let be the oracle that is defined for exactly the words of length and satisfies when the oracles are considered as sets. Then is -valid by Claim 3.7.2d and and agree on all words in as and . Thus, we can apply Claim 3.12 to the oracle . Hence, there exists a -valid oracle satisfying , , and for all . By the latter property and the fact that contains all queries asked by the least accepting path of , this path is also an accepting path of the computation . As is defined for all words of length , the computation is defined. Thus, for all and definitely accepts, in contradiction to the assumption that step of the construction fails.
Now let us consider the case . Here . By symmetry, it suffices to consider the case that is odd. Let be the minimal even element of that is not in . Such exists as it holds by (5), by Claim 3.9, and hence, . Now choose to be the oracle that is defined for exactly the words of length and that satisfies when the oracles are considered as sets. Then is -valid by Claim 3.7.2b and Claim 3.7.2g. Moreover, as , the oracles and agree on all words in . Thus, we can apply Claim 3.12 to the oracle for the parameter and obtain a -valid oracle that is defined for all words of length and satisfies both and for all . The latter property and the fact that contains all queries asked by the least accepting path of yield that this path is also an accepting path of the computation . As is defined for all words of length , the computation definitely accepts. Let us study two cases depending on whether definitely accepts or definitely rejects (note that this computation is defined as is defined for all words of length ):
- •
Assume that definitely accepts. Let be the step that treats the task . Hence, since is defined. By Claim 3.5, the oracle is -valid. Now, as both and definitely accept, is even -valid for . But then the construction would have chosen , in contradiction to .
- •
Assume that definitely rejects. As , it holds for all . This is a contradiction to the assumption that step of the construction fails.
As in both cases we obtain a contradiction, the proof of Claim 3.13 is complete.
Claim 3.14
For all odd and all even , and conflict.
**Proof **Assume there are odd and even such that and do not conflict. Then let u^{\prime}\mathrel{\sqsupseteq\kern-9.19998pt\raise-1.49994pt\hbox{\rotatebox{313.0}{\scalebox{1.1}[0.75]{\shortmid}}}\scalebox{0.3}[1.0]{\ }}u be the minimal oracle that is defined for all words of length and contains and , i.e., interpreting oracles as sets it holds . Let be the step that treats the task . Then as is defined. As is injective on its support and , it holds . Therefore, the oracle is -valid by Claim 3.7.2a. If Claim 3.11 cannot be applied to the oracle for the parameters , , and , then or . As by Claim 3.13, and and moreover, and , in this case and conflict, a contradiction. Hence, it remains to consider the case that Claim 3.11 can be applied to the oracle for the parameters , , and .
Applying Claim 3.11, we obtain a -valid that is defined for all words of length and that satisfies for all and for all . We claim
[TABLE]
Once (6) is proven, we obtain a contradiction as then the construction would have chosen , in contradiction to . Hence, then our assumption is wrong and for all odd and all even , and conflict.
It remains to prove (6). We study two cases.
Case 1: first we assume that , i.e., it suffices to prove that and definitely accept. Recall that and definitely accept. Moreover, for all and for all and in particular, is defined for all words in . This implies that the least accepting paths of and are also accepting paths of the computations and . Thus, is -valid.
Case 2: assume that , i.e., we have to prove that on some input the computation has two accepting paths. By Claim 3.13, and . As and do not conflict, it holds , which implies . Let be minimal such that and for a contradiction, assume .
Let . Without loss of generality, we assume . Then there exist with such that and asks the query . By the choice of , it holds and thus, . Consequently, all queries of are in . However, and therefore, cannot be asked by . This shows that there is a word asked by both and (otherwise, the two computations would ask the same queries). But then , which implies that and conflict, a contradiction. Hence, we obtain and .
Recall that (resp., ) is the set consisting of all oracle queries of the least accepting path (resp., ) of the computation (resp., ). As for all and for all , the paths and are accepting paths of the computation . Finally, and are distinct paths since and are distinct sets. This finishes the proof of (6). Hence, the proof of Claim 3.14 is complete.
The remainder of the proof that the construction is possible is based on an idea by Hartmanis and Hemachandra [HH88]. Consider the set
[TABLE]
Let such that . Then by Claim 3.14 and Claim 3.10, and conflict in a word of length . As observed above, this means that they conflict in or . Hence, or . This shows E=\{\{z,z^{\prime}\}\mid z,z^{\prime}\in{\Sigma}^{n},\text{z\Leftrightarrow z^{\prime} even}\} and thus, . By Claim 3.9, for each it holds . Consequently,
[TABLE]
a contradiction. Hence, the assumption that the construction fails in step treating the task is wrong. This shows that the construction described above is possible and is well-defined. In order to finish the proof of the Theorem 3.2, it remains to show that
- •
does not contain a pair -hard for ,
- •
each problem in has a -optimal proof system, and
- •
does not contain a -complete problem.
Claim 3.15
* does not contain a pair that is -hard for .*
**Proof ** Assume the assertion is wrong, i.e., there exist distinct such that and for every it holds . From if follows that for all there does not exist such that both and definitely accept. Hence, for no it holds and thus, by construction for some and all sufficiently large . The latter implies for all (cf. V3), which yields , i.e., . Thus, there exists such that via . Let be the step that treats task . This step makes sure that there exists such that at least one of the following properties holds:
- •
for all and definitely rejects.
- •
for all and definitely rejects.
As for all that is defined for, one of the following two statements holds.
- •
and is rejected by .
- •
and is rejected by .
This is a contradiction to via , which completes the proof of Claim 3.15.
Claim 3.16
Each problem in has a -optimal proof system.
**Proof ** By Corollary 2.4, it suffices to prove that has a -optimal proof system.
Let be an arbitrary proof system for and be an arbitrary element of . Define to be the following function :
[TABLE]
By definition, and as is a proof system for it holds . We show . Let . Assume for , , and (otherwise, clearly ). Let such that computes . Let be large enough such that is defined for , i.e. . As is -valid, we obtain by V1 that and by Claim 3.4 that is defined and for all . Then . This shows that is a proof system for .
It remains to show that each proof system for is -simulated by . Let be an arbitrary proof system for . Then there exists such that computes . By construction, , where is the number of the step that treats the task . Consider the following function :
[TABLE]
As and are proof systems for , for every there exists with . Hence, is total. Since is a constant, . It remains to show that for all . If , it holds . Otherwise, choose large enough such that (i) is defined (i.e., ) and (ii) is defined for . Then, as is -valid, V5 yields that . By Claim 3.4, is defined and hence, as well as . Hence, , which shows . This completes the proof of Claim 3.16.
Claim 3.17
* does not contain a -complete problem.*
**Proof ** Assume there exists an -complete problem. Then there exists such that is -complete for . As on every input, has at most one accepting path, there exists no with . Hence, by construction for some and all sufficiently large . Then for all (cf. V7) and consequently, . As is complete for , there exists such that via . Let be the step that treats the task . By construction, there exists such that one of the following two statements holds:
- •
for all and definitely rejects.
- •
for all and definitely accepts.
As and agree on all words that is defined for, one of the following two conditions holds:
- •
and rejects.
- •
and accepts.
This is a contradiction to via , which shows that does not have -complete problems. This completes the proof of Claim 3.17.
Now the proof of Theorem 3.2 is complete.
?refname?
- [BKM09]
O. Beyersdorff, J. Köbler, and J. Messner.
Nondeterministic functions and the existence of optimal proof systems.
Theor. Comput. Sci., 410(38-40):3839–3855, 2009.
- [CR79]
S. Cook and R. Reckhow.
The relative efficiency of propositional proof systems.
Journal of Symbolic Logic, 44:36–50, 1979.
- [DG19]
T. Dose and C. Glaßer.
NP-completeness, proof systems, and disjoint NP-pairs.
Technical Report 19-050, Electronic Colloquium on Computational Complexity (ECCC), 2019.
- [Dos19]
T. Dose.
and all sets in have P-optimal proof systems relative to an oracle.
arXiv e-prints, page arXiv:1909.02839, Sep 2019.
- [ESY84]
S. Even, A. L. Selman, and J. Yacobi.
The complexity of promise problems with applications to public-key cryptography.
Information and Control, 61:159–173, 1984.
- [EY80]
S. Even and Y. Yacobi.
Cryptocomplexity and NP-completeness.
In Proceedings 7th International Colloquium on Automata, Languages and Programming, volume 85 of Lecture Notes in Computer Science, pages 195–207. Springer, 1980.
- [GS88]
J. Grollmann and A. L. Selman.
Complexity measures for public-key cryptosystems.
SIAM Journal on Computing, 17(2):309–335, 1988.
- [GSSZ04]
C. Glaßer, A. L. Selman, S. Sengupta, and L. Zhang.
Disjoint NP-pairs.
SIAM Journal on Computing, 33(6):1369–1416, 2004.
- [HH88]
J. Hartmanis and L. A. Hemachandra.
Complexity classes without machines: On complete languages for UP.
Theor. Comput. Sci., 58:129–142, 1988.
- [Kha19]
E. Khaniki.
New relations and separations of conjectures about incompleteness in the finite domain.
arXiv e-prints, pages 1–25, Apr 2019.
- [KM00]
J. Köbler and J. Messner.
Is the standard proof system for sat p-optimal?
In S. Kapoor and S. Prasad, editors, FSTTCS 2000: Foundations of Software Technology and Theoretical Computer Science, pages 361–372, Berlin, Heidelberg, 2000. Springer Berlin Heidelberg.
- [KMT03]
J. Köbler, J. Messner, and J. Torán.
Optimal proof systems imply complete sets for promise classes.
Information and Computation, 184(1):71–92, 2003.
- [KP89]
J. Krajíček and P. Pudlák.
Propositional proof systems, the consistency of first order theories and the complexity of computations.
Journal of Symbolic Logic, 54:1063–1079, 1989.
- [MP91]
N. Megiddo and C. H. Papadimitriou.
On total functions, existence theorems and computational complexity.
Theor. Comput. Sci., 81(2):317–324, 1991.
- [Pap94]
C. M. Papadimitriou.
Computational complexity.
Addison-Wesley, Reading, Massachusetts, 1994.
- [Pud96]
P. Pudlák.
On the lengths of proofs of consistency.
In Collegium Logicum, pages 65–86. Springer Vienna, 1996.
- [Pud13]
P. Pudlák.
*Logical Foundations of Mathematics and Computational Complexity
- A Gentle Introduction*.
Springer monographs in mathematics. Springer, 2013.
- [Pud17]
P. Pudlák.
Incompleteness in the finite domain.
The Bulletin of Symbolic Logic, 23(4):405–441, 2017.
- [Raz94]
A. A. Razborov.
On provably disjoint np-pairs.
Electronic Colloquium on Computational Complexity (ECCC), 1(6), 1994.
The reference list from the paper itself. Each links out to its DOI / PubMed record.
- 1[BKM 09] O. Beyersdorff, J. Köbler, and J. Messner. Nondeterministic functions and the existence of optimal proof systems. Theor. Comput. Sci. , 410(38-40):3839–3855, 2009.
- 2[CR 79] S. Cook and R. Reckhow. The relative efficiency of propositional proof systems. Journal of Symbolic Logic , 44:36–50, 1979.
- 3[DG 19] T. Dose and C. Glaßer. NP-completeness, proof systems, and disjoint NP-pairs. Technical Report 19-050, Electronic Colloquium on Computational Complexity (ECCC), 2019.
- 4[Dos 19] T. Dose. P ≠ NP P NP \mathrm{P}\neq\mathrm{NP} and all sets in NP ∪ co NP NP co NP \mathrm{NP}\cup\mathrm{co NP} have P-optimal proof systems relative to an oracle. ar Xiv e-prints , page ar Xiv:1909.02839, Sep 2019.
- 5[ESY 84] S. Even, A. L. Selman, and J. Yacobi. The complexity of promise problems with applications to public-key cryptography. Information and Control , 61:159–173, 1984.
- 6[EY 80] S. Even and Y. Yacobi. Cryptocomplexity and NP-completeness. In Proceedings 7th International Colloquium on Automata, Languages and Programming , volume 85 of Lecture Notes in Computer Science , pages 195–207. Springer, 1980.
- 7[GS 88] J. Grollmann and A. L. Selman. Complexity measures for public-key cryptosystems. SIAM Journal on Computing , 17(2):309–335, 1988.
- 8[GSSZ 04] C. Glaßer, A. L. Selman, S. Sengupta, and L. Zhang. Disjoint NP-pairs. SIAM Journal on Computing , 33(6):1369–1416, 2004.
