On $\mathcal{NP}$ versus ${\rm co}\mathcal{NP}$ and Frege Systems

We prove in this paper that there is a language $L_{d}$ accepted by some nondeterministic Turing machines but not by any ${\rm co}\mathcal{NP}$-machines (defined later). Then we further show that $L_{d}$ is in $\mathcal{NP}$, thus proving that $\mathcal{NP}\neq{\rm co}\mathcal{NP}$. The main techniques used in this paper are lazy-diagonalization and the novel new technique developed in the author’s recent work [Lin21]. Further, since there exists some oracle $A$ such that $\mathcal{NP}^{A}={\rm co}\mathcal{NP}^{A}$, we then explore what mystery lies behind it and show that if $\mathcal{NP}^{A}={\rm co}\mathcal{NP}^{A}$ and under some rational assumptions, then the set of all polynomial-time co-nondeterministic oracle Turing machines with oracle $A$ is not enumerable, thus showing that the technique of lazy-diagonalization is not applicable for the first half of the whole step to separate $\mathcal{NP}^{A}$ from ${\rm co}\mathcal{NP}^{A}$. As a by-product, we reach the important result that $\mathcal{P}\neq\mathcal{NP}$ [Lin21] once again, which is clear from the above outcome and the well-known fact that $\mathcal{P}={\rm co}\mathcal{P}$. Next, we show that the complexity class ${\rm co}\mathcal{NP}$ has intermediate languages, i.e., there exists a language $L_{inter}\in{\rm co}\mathcal{NP}$, which is not in $\mathcal{P}$ and not ${\rm co}\mathcal{NP}$-complete. We also summarize other direct consequences implied by our main outcome, such as $\mathcal{NEXP}\neq{\rm co}\mathcal{NEXP}$, $\mathcal{BPP}\neq\mathcal{NEXP}$ and there exists no super proof system. Lastly, we show a lower bounds result for Frege proof systems, i.e., no Frege proof systems can be polynomially bounded.

It is well-known that computational complexity theory is a central subfield of theoretical computer science and mathematics, which mainly concerns the efficiency of Turing machines (i.e., algorithms), or the intrinsic complexity of computational tasks, i.e., focuses on classifying computational problems according to their resource usage, and relating these classes to each other (see e.g. [A1]). In other words, computational complexity theory specifically deals with fundamental questions such as what is feasible computation and what can and cannot be computed with a reasonable amount of computational resources in terms of time or space (memory). What’s exciting is that there are many remarkable open problems in the area of computational complexity theory, such as the famous $\mathcal{P}$ versus $\mathcal{NP}$ problem and the important unknown relation between the complexity class $\mathcal{NP}$ and the complexity class ${\rm co}\mathcal{NP}$, which deeply attract many researchers to conquer them like crazy. However, despite decades of effort, very little progress has been made on these important problems. Furthermore, as pointed out by Wigderson [Wig07], to understand the power and limits of efficient computation has led to the development of computational complexity theory, and this discipline in general, and the aforementioned famous open problems in particular, have gained prominence within the mathematics community in the past decades.

As introduced in the Wikipedia [A1], in the field of computational complexity theory, a problem is regarded as inherently difficult if its solution requires significant resources such as time and space, whatever the algorithm used. The theory formalizes this intuition, by introducing mathematical models of computing to study these problems and quantifying their computational complexity, i.e., the amount of resources needed to solve them. However, it is worth noting that other measures of complexity are also used, such as the amount of communication, which appeared in communication complexity, the number of gates in a circuit, which appeared in circuit complexity, and so forth (see e.g. [A1]). Going further, one of the roles of computational complexity theory is to determine the practical limits on what computers (the computing models) can and cannot do.

Recently, in the author’s work [Lin21], we left an important open conjecture in computational complexity untouched on, which is one of the aforementioned open problems, i.e., the $\mathcal{NP}$ versus ${\rm co}\mathcal{NP}$ problem (the unknown relation between complexity classes $\mathcal{NP}$ and ${\rm co}\mathcal{NP}$). Naturally, one will ask, are these two complexity classes the same? Further, also note that there is a subfield of computational complexity theory, namely, the proportional proof complexity, which was initiated by Cook and Reckhow [CR79] and is devoted to the goal of proving the conjecture

In history, the fundamental measure of time opened the door to the study of the extremely expressive time complexity class $\mathcal{NP}$, one of the most important classical complexity classes, i.e., nondeterministic polynomial-time. Specifically, $\mathcal{NP}$ is the set of decision problems for which the problem instances, where the answer is “yes”, have proofs verifiable in polynomial time by some deterministic Turing machine, or alternatively the set of problems that can be solved in polynomial time by a nondeterministic Turing machine (see e.g. [A2]). The famous Cook-Levin theorem [Coo71, Lev73] shows that this class has complete problems, which states that the Satisfiability is $\mathcal{NP}$-complete, i.e., Satisfiability is in $\mathcal{NP}$ and any other language in $\mathcal{NP}$ can be reduced to it in polynomial-time. At the same time, it is also worth noting that this famous and seminal result opened the door to research into the renowned rich theory of $\mathcal{NP}$-completeness [Kar72].

On the other hand, the complexity class ${\rm co}\mathcal{NP}$ is formally defined as follows: For a complexity class $\mathcal{C}$, its complement is denoted by ${\rm co}\mathcal{C}$ (see e.g. [Pap94]), i.e.,

where $L$ is a decision problem, and $\overline{L}$ is the complement of $L$ (i.e., $\overline{L}=\Sigma^{*}-L$ with assumption that the language $L$ is over the alphabet $\Sigma$). That is to say, ${\rm co}\mathcal{NP}$ is the complement of $\mathcal{NP}$. Note that, the complement of a decision problem $L$ is defined as the decision problem whose answer is “yes” whenever the input is a “no” input of $L$, and vice versa. In other words, for instance, according to the Wikipedia’s language [A3], ${\rm co}\mathcal{NP}$ is the set of decision problems where there exists a polynomial $p(n)$ and a polynomial-time bounded Turing machine $M$ such that for every instance $x$, $x$ is a no-instance if and only if: for some possible certificate $c$ of length bounded by $p(n)$, the Turing machine $M$ accepts the pair $(x,c)$. To the best of our knowledge, the complexity class ${\rm co}\mathcal{NP}$ was introduced for the first time by Meyer and Stockmeyer [MS72] with the name “$\prod_{1}^{P}$”, and Stockmeyer wrote a full paper on the polynomial hierarchy which also uses the notation ${\rm co}\mathcal{NP}$; see e.g. [Sto77].

The $\mathcal{NP}$ versus ${\rm co}\mathcal{NP}$ problem is deeply connected to the field of proof complexity. Here are some historical notes: In 1979, Cook and Reckhow [CR79] introduced a general definition of propositional proof system and related it to mainstream complexity theory by pointing out that such a system exists in which all tautologies have polynomial length proofs if and only if the two complexity classes $\mathcal{NP}$ and ${\rm co}\mathcal{NP}$ coincide; see e.g. [CN10]. We refer the reader to the reference [Coo00] for the importance of this research field and to the reference [Kra95] for the motivation of the development of this rich theory. Apart from those, Chapter $10$ of [Pap94] also contains the introductions of importance of the problem

In this paper, our main goal is to settle the above important open conjecture.

In the next few paragraphs, let us review some of the interesting background, the current status, the history, and the main goals of the field of proof complexity. On the one hand, as we all know well, proof theory is a major branch of mathematical logic and theoretical computer science with which proofs are treated as formal mathematical objects, facilitating their analysis by mathematical techniques (see e.g. [A4]). Some of the major areas of proof theory include structural proof theory, ordinal analysis, automated theorem proving, and proof complexity, and so forth. It should be pointed out that much research also focuses on applications in computer science, linguistics, and philosophy, from which we see that the impact of proof theory is very profound. Moreover, as pointed out in [Raz04] by Razborov, proof and computations are among the most fundamental concepts relevant to virtually any human intellectual activity. Both have been central to the development of mathematics for thousands of years. The effort to study these concepts themselves in a rigorous, metamathematical way initiated in the $20$th century led to flourishing of mathematical logic and derived disciplines.

On the other hand, according to the points of view given in [Rec76], logicians have proposed a great number of systems for proving theorems, which give certain rules for constructing proofs and for associating a theorem (formula) with each proof. More importantly, these rules are much simpler to understand than the theorems. Thus, a proof gives a constructive way of understanding that a theorem is true. Specifically, a proof system is sound if every theorem is true, and it is complete if every true statement (from a certain class) is a theorem (i.e., has a proof); see e.g. [Rec76].

Indeed, the relationship between proof theory and proof complexity is inclusion. Within the area of proof theory, proof complexity is the subfield aiming to understand and analyse the computational resources that are required to prove or refute statements (see e.g. [A5]). Research in proof complexity is predominantly concerned with proving proof-length lower and upper bounds in various propositional proof systems. For example, among the major challenges of proof complexity is showing that the Frege system, the usual propositional calculus, does not admit polynomial-size proofs of all tautologies; see e.g. [A5]. Here the size of the proof is simply the number of symbols in it, and a proof is said to be of polynomial size if it is polynomial in the size of the tautology it proves. Moreover, contemporary proof complexity research draws ideas and methods from many areas in computational complexity, algorithms and mathematics. Since many important algorithms and algorithmic techniques can be cast as proof search algorithms for certain proof systems, proving lower bounds on proof sizes in these systems implies run-time lower bounds on the corresponding algorithms; see e.g. [A5].

At the same time, propositional proof complexity is an area of study that has seen a rapid development over the last two decades, which plays as important a role in the theory of feasible proofs as the role played by the complexity of Boolean circuits in the theory of efficient computations, see e.g. the celebrated work [Raz15] by Razborov. In most cases, according to [Raz15], the basic question of propositional proof complexity can be reduced to that given a mathematical statement encoded as a propositional tautology $\psi$ and a class of admissible mathematical proofs formalized as a propositional proof system $P$, what is the minimal possible complexity of a $P$-proof of $\psi$? In other words, propositional proof complexity aims to understand and analyze the computational resources required to prove propositional tautologies, in the same way that circuit complexity studies the resources required to compute Boolean functions. In the light of the point of view given in [Raz15], the task of proving lower bounds for strong proof systems like Frege or Extended Frege modulo any hardness assumption in the purely computational world may be almost as interesting; see e.g. [Raz15]. It is worth noting that, it has been observed by Razborov [Raz15] that $\mathcal{NP}\neq{\rm co}\mathcal{NP}$ implies lower bounds for any propositional proof system. In addition, see e.g. [Raz03] for interesting directions in propositional proof complexity.

Historically, systematic study of proof complexity began with the seminal work of Cook and Reckhow [CR79] who provided the basic definition of a propositional proof system from the perspective of computational complexity. In particular, as pointed out by the authors of [FSTW21], the work [CR79] relates the goal of propositional proof complexity to fundamental hardness questions in computational complexity such as the $\mathcal{NP}$ versus ${\rm co}\mathcal{NP}$ problem: establishing super-polynomial lower bounds for every propositional proof system would separate $\mathcal{NP}$ from ${\rm co}\mathcal{NP}$.

Let us return back to the $\mathcal{NP}$ versus ${\rm co}\mathcal{NP}$ problem for this moment. As a matter of fact, the so-called $\mathcal{NP}$ versus ${\rm co}\mathcal{NP}$ problem is the central problem in proof complexity; see e.g. the excellent survey [Kra19]. It formalizes the question of whether or not there are efficient ways to prove the negative cases in our, and in many other similar examples. Moreover, the ultimate goal of proof complexity is to show that there is no universal propositional proof system allowing for efficient proofs of all tautologies, which is equivalent to showing that the computational complexity class $\mathcal{NP}$ is not closed under the complement; see e.g. [Kra19].

Particularly, in 1974, Cook and Reckhow showed in [CR74] that there exists a super proof system if and only if $\mathcal{NP}$ is closed under complement; that is, if and only if $\mathcal{NP}={\rm co}\mathcal{NP}$. It is, of course, open whether any super proof system exists. The above result has led to what is sometimes called “Cook’s program” for proving $\mathcal{NP}\neq{\rm co}\mathcal{NP}$: prove superpolynomial lower bounds for proof lengths in stronger and stronger proposition proof systems, until they are established for all abstract proof systems. Cook’s program, which also can be seen as a program to prove $\mathcal{P}\neq\mathcal{NP}$, is an attractive and plausible approach; unfortunately, it has turned out to be quite hard to establish superpolynomial lower bounds on common proof systems, see e.g. the excellent survey on proof complexity [Bus12].

In this paper, the proof systems we consider are those familiar from textbook presentations of logic, such as the Frege systems which were mentioned previously. It can be said that the Frege proof system is a “textbook-style” propositional proof system with Modus Ponens as its only rule of inference. In fact, before our showing that $\mathcal{NP}\neq{\rm co}\mathcal{NP}$, although $\mathcal{NP}\neq{\rm co}\mathcal{NP}$ is considered to be very likely true, researchers are not able to prove that some very basic proof systems are not polynomially bounded; see e.g. [Pud08]. In particular, the following open problem is listed as the first open problem in [Pud08]:

Prove a superpolynomial lower bound on the length of proofs for a Frege system (or prove that it is polynomially bounded).

However, despite decades of effort, very little progress has been made on the above mentioned open problem.

In this section, we introduce some notions and notation that will be used in what follows.

Let $\mathbb{N}_{1}=\{1,2,3,\cdots\}$ where $+\infty\notin\mathbb{N}_{1}$, i.e., the set of all positive integers. We also denote by $\mathbb{N}$ the set of natural numbers, i.e.,

Let $\Sigma$ be an alphabet, for finite words $w,v\in\Sigma^{*}$, the concatenation of $w$ and $v$, denoted by $w\circ v$, is $wv$. For example, suppose that $\Sigma=\{0,1\}$, and $w=100001$, $v=0111110$, then

The length of a finite word $w$, denoted as $|w|$, is defined to be the number of symbols in it. It is clear that for finite words $w$ and $v$,

The big $O$ notation indicates the order of growth of some quantity as a function of $n$ or the limiting behavior of a function. For example, that $S(n)$ is big $O$ of $f(n)$, i.e.,

means that there exist a positive integer $N_{0}$ and a positive constant $M$ such that

for all $n>N_{0}$.

The little $o$ notation also indicates the order of growth of some quantity as a function of $n$ or the limiting behavior of a function but with different meaning. Specifically, that $T(n)$ is little $o$ of $t(n)$, i.e.,

means that for any constant $c>0$, there exists a positive integer $N_{0}>0$ such that

for all $n>N_{0}$.

Throughout this paper, the computational modes used are nondeterministic Turing machines (or their variants such as nondeterministic Turing machines with oracle). We follow the standard definition of a nondeterministic Turing machine given in the standard textbook [AHU74]. Let us first introduce the precise definition of a nondeterministic Turing machine as follows:

Let $M$ be a nondeterministic Turing machine, and $w$ be an input. Then $M(w)$ represents that $M$ is on input $w$.

A nondeterministic Turing machine $M$ works in time $t(n)$ (or of time complexity $t(n)$), if for any input $w\in I^{*}$ where $I$ is the input alphabet of $M$, $M(w)$ will halt within $t(|w|)$ steps for any input $w$.

Now, it is time for us to introduce the concept of a polynomial-time nondeterministic Turing machine as follows:

By default, a word $w$ is accepted by a nondeterministic $t(n)$ time-bounded Turing machine $M$ if there exists a computation path $\gamma$ such that $M(w)=1$ (i.e., stop in the “accepting” state) on that computation path described by $\gamma$. This is the “exists” accepting criterion for nondeterministic Turing machines in general, based on which the complexity class ${\rm NTIME}[t(n)]$ is defined:

Apart from the “exists” accepting criterion for defining the complexity class ${\rm NTIME}[t(n)]$, there is another “for all” accepting criterion¹¹1Originally, for a polynomial-time nondeterministic Turing machine, it should be the “for all” rejecting criterion (i.e., all computation paths of $M(w)$ reject), but we can exchange the rejecting state and the accepting state, i.e., treat the rejecting state as the accepting state. Thus, in this sense, we can also call that the “for all” accepting criterion. for nondeterministic Turing machines, defined as follows:

With the Definition 2.4 above, we can similarly define the complexity class ${\rm coNTIME}[t(n)]$ of languages decided by nondeterministic Turing machines within time $t(n)$ in terms of the “for all” accepting criterion:

We can define the complexity class ${\rm co}\mathcal{NP}$ in a equivalent way using polynomial-time deterministic Turing machines as verifiers and “for all” witnesses, given as follows:

With the complexity class ${\rm co}\mathcal{NP}$ above, we next define the set of all ${\rm co}\mathcal{NP}$-machines as follows.

For convenience, we denote by the notation ${\rm co}NP$ the set of all ${\rm co}\mathcal{NP}$-machines, i.e., the set ${\rm co}NP$ consists of all ${\rm co}\mathcal{NP}$-machines:

In regard to the relation between the time complexity of $k$-tape nondeterministic Turing machines and that of single-tape nondeterministic Turing machines, we quote the following useful lemma, extracted from [AHU74] (see Lemma 10.1 in [AHU74]), which plays important roles in the following context:

Since ${\rm co}\mathcal{NP}$-machines are also polynomial-time nondeterministic Turing machines but with the “for all” accepting criterion for the input, we can similarly prove the following technical lemma:

Proof. The proof is similar to that of Lemma 2.1 and see [AHU74], so the detail is omitted.   

The following theorem about efficient simulation for universal nondeterministic Turing machines is useful in proving the main result in Section 4.

Other background information and notions will be given along the way in proving our main results stated in Section 1.

In this section, our main goal is to establish an important theorem that all ${\rm co}\mathcal{NP}$-machines are in fact enumerable, which is the prerequisite for the next steps.

Following Definition 2.2, a polynomial-time nondeterministic Turing machine can be represented by a tuple of $(M,k)$, where $M$ is the nondeterministic Turing machine itself and $k$ is the unique minimal degree of some polynomial $|x|^{k}+k$ such that $M(x)$ will halt within $|x|^{k}+k$ steps for any input $x$ of length $|x|$. We call such a positive integer $k$ the order of $(M,k)$.

By Lemma 2.1 stated above, we only need to discuss the single-tape nondeterministic Turing machines. Thus, in the following context, by a nondeterministic Turing machine we mean a single-tape nondeterministic Turing machine. Similarly, by Lemma 2.2, we only need to discuss the single-tape ${\rm co}\mathcal{NP}$-machines. Thus, in the following context, by a ${\rm co}\mathcal{NP}$-machine we mean a single-tape ${\rm co}\mathcal{NP}$-machine.

To obtain our main result, we must enumerate all ${\rm co}\mathcal{NP}$-machines and suppose that the set of all ${\rm co}\mathcal{NP}$-machines is enumerable (which needs to be proved) so that we can refer to the $j$-th ${\rm co}\mathcal{NP}$-machine in the enumeration.

To show that the set of all ${\rm co}\mathcal{NP}$-machines is enumerable, we need to study whether the whole set of polynomial-time nondeterministic Turing machines is enumerable, because by Definition 2.4 or by Remark 2.1, ${\rm co}\mathcal{NP}$-machines are nondeterministic Turing machines running within polynomial time but the accepting criterion for the input is the “for all” criterion, so the set ${\rm co}NP$ can be seen as a subset of all polynomial-time nondeterministic Turing machines but with the “for all” accepting criterion.

In what follows, we first use the method presented in [AHU74], p. 407, to encode a single-tape nondeterministic Turing machine into an integer.

Without loss of generality, we can make the following assumptions about the representation of a single-tape nondeterministic Turing machine with input alphabet $\{0,1\}$ because that will be all we need:

1. 1.

   The states are named

   $$q_{1},q_{2},\cdots,q_{s}$$

   for some $s$, with $q_{1}$ the initial state and $q_{s}$ the accepting state.

2. 2.

   The input alphabet is $\{0,1\}$.

3. 3.

   The tape alphabet is

   $$\{X_{1},X_{2},\cdots,X_{t}\}$$

   for some $t$, where $X_{1}=\mathbbm{b}$, $X_{2}=0$, and $X_{3}=1$.

4. 4.

   The next-move function $\delta$ is a list of quintuples of the form,

   $$\{(q_{i},X_{j},q_{k},X_{l},D_{m}),\cdots,(q_{i},X_{j},q_{f},X_{p},D_{z})\}$$

   meaning that

   $$\delta(q_{i},X_{j})=\{(q_{k},X_{l},D_{m}),\cdots,(q_{f},X_{p},D_{z})\},$$

   and $D_{m}$ is the direction, $L$, $R$, or $S$, if $m=1,2$, or $3$, respectively. We assume this quintuple is encoded by the string

   $$10^{i}10^{j}10^{k}10^{l}10^{m}1\cdots 10^{i}10^{j}10^{f}10^{p}10^{z}1.$$

5. 5.

   The Turing machine itself is encoded by concatenating in any order the codes for each of the quintuples in its next-move function. Additional $1$’s may be prefixed to the string if desired. The result will be some string of $0$’s and $1$’s, beginning with $1$, which we can interpret as an integer.

Next, we encode the order of $(M,k)$ to be

so that the tuple $(M,k)$ should be the concatenation of the binary string representing $M$ itself followed by the order $10^{k}1$. Now the tuple $(M,k)$ is encoded as a binary string, which can be explained as an integer. In the following context, we often use the notation $\langle M\rangle$ to denote the shortest binary string that represents the same $n^{k}+k$ time-bounded nondeterministic Turing machine $(M,k)$. We should further remark that the shortest binary string $\langle M\rangle$ that represents the same $n^{k}+k$ time-bounded nondeterministic Turing machine $(M,k)$ is by concatenating in any order the codes for each of the quintuples in its next-move function followed by the order $10^{k}1$ without additional $1$ prefixed to it, from which it is clear that $\langle M\rangle$ may not be unique (since the order of codes of the quintuples may be different), but the lengths of all different $\langle M\rangle$ are the same.

By this encoding, any integer that cannot be decoded is assumed to represent the trivial Turing machine with an empty next-move function. Every single-tape polynomial-time nondeterministic Turing machine will appear infinitely often in the enumeration since, given a polynomial-time nondeterministic Turing machine, we may prefix $1$’s at will to find larger and larger integers representing the same set of $(M,k)$. We denote such a polynomial-time nondeterministic Turing machine by $\widehat{M}_{j}$, where $j$ is the integer representing the tuple $(M,k)$, i.e., $j$ is the integer value of the binary string representing the tuple $(M,k)$.

For convenience, let us introduce an additional notation $NP$ to denote a set of all polynomial-time nondeterministic Turing machines, i.e., we denote the set of all polynomial-time nondeterministic Turing machines by the notation $NP$.³³3The reader should not confuse $NP$ and $\mathcal{NP}$. Note that $NP$ is the set of all polynomial-time nondeterministic Turing machines; however, $\mathcal{NP}$ is the set of all languages where, for any language $L\in\mathcal{NP}$, there is some polynomial-time nondeterministic Turing machine $(M,k)\in NP$ such that $(M,k)$ accepts $L$. In short, $NP=\{(M,k)\}$.

From the above arguments, we have reached the following important result:

As mentioned earlier, by Definition 2.4 or further by Remark 2.1, the set ${\rm co}NP$ can be seen as a subset of all polynomial-time nondeterministic Turing machines with the “for all” accepting criterion. Thus, Lemma 3.1 implies that we also establish the following important theorem:

In computational complexity, the most basic approach to show hierarchy theorems uses simulation and diagonalization, because the simulation and diagonalization technique [Tur37, HS65] is a standard method to prove lower bounds on uniform computing models (i.e., the Turing machine model); see for example [AHU74]. These techniques work well in deterministic time and space measures; see e.g. [For00, FS07]. However, they do not work for nondeterministic time, which is not known to be closed under complement at present — one of the main issues discussed in this paper; hence it is unclear how to define a nondeterministic machine that “does the opposite”; see e.g. [FS07].

For nondeterministic time, we can still do a simulation but can no longer negate the answer directly. In this case, we apply the lazy diagonalization to show the nondeterministic time hierarchy theorem; see e.g. [AB09]. It is worth noting that Fortnow [For11] developed a much more elegant and simple style of diagonalization to show nondeterministic time hierarchy. Generally, lazy diagonalization [AB09, FS07] is a clever application of the standard diagonalization technique [Tur37, HS65, AHU74]. The basic strategy of lazy diagonalization is that for any $n\leq j<m=n^{t(n)}$, $M$ on input $1^{j}$ simulates $M_{i}$ on input $1^{j+1}$, accepting if $M_{i}$ accepts and rejecting if $M_{i}$ rejects. When $j=m$, $M$ on input $1^{j}$ simulates $M_{i}$ on input $x$ deterministically, accepting if $M_{i}$ rejects and rejecting if $M_{i}$ accepts. Since $m=n^{t(n)}$, $M$ has enough time to perform the trivial exponential-time deterministic simulation of $M_{i}$ on input $1^{n}$, what we are doing is deferring the diagonalization step by linking $M$ and $M_{i}$ together on larger and larger inputs until $M$ has an input large enough that it can actually “do the opposite” deterministically; see e.g. [FS07] for details.

For our goal in this section to establish the lower bounds result, we first make the following remarks, which will be referred to in what follows:

Our main goal of this section is to establish the following lower bounds theorem with the technique of lazy diagonalization from [AB09]:

Proof. By Theorem 3.2, it is convenient that let

be an effective enumeration (denoted by $e$) of all ${\rm co}\mathcal{NP}$-machines.

The key idea will be lazy diagonalization, so named (in accordance with the point of view presented in [AB09]) because the new machine $D$ is in no hurry to diagonalize and only ensures that it flips the answer of each ${\rm co}\mathcal{NP}$-machine $M_{i}$ in only one string out of a sufficiently large (exponentially large) set of strings.

Let $D$ be a five-tape nondeterministic Turing machine which operates as follows on an input string $x$ of length of $|x|$.

1. 1.

   On input $x$, if $x\notin 1^{*}\langle M_{i}\rangle$, reject $x$. If $x=1^{l}\langle M_{i}\rangle$ for some $l\in\mathbb{N}$, then $D$ decodes $M_{i}$ encoded by $x$, including to determine $t$, the number of tape symbols used by $M_{i}$; $s$, its number of states; $k$, its order of polynomial

   $$T(n)=n^{k}+k;$$

   and $m$, the shortest length of $M_{i}$, i.e.,

   $$m=\min\{|\langle M_{i}\rangle|\,:\,\text{different binary strings $\langle M_{i}\rangle$ represent the same $M_{i}$}\}.$$

   The fifth tape of $D$ can be used as “scratch” memory to calculate $t$, $s$, $k$ and $m$.

2. 2.

   Then $D$ lays off on its second tape $|x|$ blocks of

   $$\lceil\log t\rceil$$

   cells each, the blocks being separated by single cell holding a marker $\#$, i.e., there are

   $$(1+\lceil\log t\rceil)|x|$$

   cells in all. Each tape symbol occurring in a cell of $M_{i}$’s tape will be encoded as a binary number in the corresponding block of the second tape of $D$. Initially, $D$ places its input, in binary coded form, in the blocks of tape $2$, filling the unused blocks with the code for the blank.

3. 3.

   On tape $3$, $D$ sets up a block of

   $$\lceil(k+1)\log n\rceil$$

   cells, initialized to all $0$’s. Tape $3$ is used as a counter to count up to

   $$n^{k+1},$$

   where $n=|x|$.

4. 4.

   $D$ simulates $M_{i}$, using tape $1$, its input tape, to determine the moves of $M_{i}$ and using tape $2$ to simulate the tape of $M_{i}$ (i.e., $D$ will place $M_{i}$’s input to the tape $2$). The moves of $M_{i}$ are counted in binary in the block of tape $3$, and tape $4$ is used to hold the states of $M_{i}$. If the counter on tape $3$ overflows, $D$ halts with rejecting. The specified simulation is the following:

   “On input $1^{n-m}\langle M_{i}\rangle$ (note that $m=|\langle M_{i}\rangle|$), then $D$ uses the fifth tape as “scratch” memory to compute $j$ such that

   $$f(j)<n\leq f(j+1)$$

   where

   $$f(j+1)=\left\{\begin{array}[]{ll}2,&\hbox{$j=0$;}\\ 2^{f(j)^{k}},&\hbox{$j\geq 1$.}\end{array}\right.$$

   (by Remark 4.1, to compute $j$ can be done within time

   $$O(n^{k+\delta})$$

   with $0<\delta<1$ which is less than time

   $$n^{k+1},$$

   so $D$ has sufficient time) and

   • (i).

     If $f(j)<n<f(j+1)$ then $D$ simulates $M_{i}$ on input $1^{n+1-m}\langle M_{i}\rangle$ ⁴⁴4$D$ first erases the old content of the second tape, then $D$ lays off on its second tape $|1^{n+1-m}\langle M_{i}\rangle|$ (i.e., $n+1$) blocks of $\lceil\log t\rceil$ cells each, the blocks being separated by single cell holding a marker $\#$, i.e., there are $(1+\lceil\log t\rceil)|1^{n+1-m}\langle M_{i}\rangle|$ cells in all. Each tape symbol occurring in a cell of $M_{i}$’s tape will be encoded as a binary number in the corresponding block of the second tape of $D$. (where $m=|\langle M_{i}\rangle|$) using nondeterminism in $(n+1)^{k}+k$ time and output its answer, i.e., $D$ rejects the input $1^{n-m}\langle M_{i}\rangle$ if and only if $M_{i}$ rejects the input $1^{n+1-m}\langle M_{i}\rangle$. ⁵⁵5 Because as a ${\rm co}\mathcal{NP}$-machine with the “for all” accepting criterion, $M_{i}$ rejects an input $w$ if and only if $\exists u\in\{0,1\}^{p(|w|)}$ as a sequence of choices made by $M_{i}$ such that $M_{i}(w)=0$ on the computation path described by $u$, where $p(|w|)$ is the time bounded of $M_{i}$.

   • (ii).

     If $n=f(j+1)$, then $D$ simulates $M_{i}$ on input $1^{f(j)+1-m}\langle M_{i}\rangle$.⁶⁶6Similarly, $D$ first erases the second tape of $D$, then $D$ lays off on its second tape $|1^{f(j)+1-m}\langle M_{i}\rangle|$ (i.e., $f(j)+1$) blocks of $\lceil\log t\rceil$ cells each, the blocks being separated by single cell holding a marker $\#$, i.e., there are $(1+\lceil\log t\rceil)|1^{f(j)+1-m}\langle M_{i}\rangle|$ cells in all. Each tape symbol occurring in a cell of $M_{i}$’s tape will be encoded as a binary number in the corresponding block of the second tape of $D$. Then, $D$ rejects $1^{n-m}\langle M_{i}\rangle$ if $M_{i}$ accepts $1^{f(j)+1-m}\langle M_{i}\rangle$ in $(f(j)+1)^{k}$ time; $D$ accepts $1^{n-m}\langle M_{i}\rangle$ if $M_{i}$ rejects $1^{f(j)+1-m}\langle M_{i}\rangle$ in $(f(j)+1)^{k}$ time.⁷⁷7 Note again that as a ${\rm co}\mathcal{NP}$-machine with the “for all” accepting criterion, $M_{i}$ accepts an input $w$ if and only if $\forall u\in\{0,1\}^{p(|w|)}$ as the sequences of choices made by $M_{i}$ such that $M_{i}(w)=1$ on the computation path described by $u$, where $p(|w|)$ is the time bounded of $M_{i}$.”