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 \cite{Lin21}. Further, since there exists some oracle $A$ such that $\mathcal{NP}^A={\rm co}\mathcal{NP}^A$, we then explore what mystery behind it and show that if $\mathcal{NP}^A={\rm co}\mathcal{NP}^A$ and under some rational assumptions, 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}$ \cite{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 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}$ and other which belongs to the area of proof complexity. Lastly, we show a lower bounds result for Frege proof systems, i.e., no Frege proof systems can be polynomially bounded.

翻译：本文证明存在一种语言$L_d$，它可被某些非确定性图灵机接受，但无法被任何${\rm co}\mathcal{NP}$机（定义见后文）接受。进而我们证明$L_d$属于$\mathcal{NP}$，由此证得$\mathcal{NP}\neq{\rm co}\mathcal{NP}$。本文采用的主要技术是惰性对角化方法及作者近期研究\cite{Lin21}中提出的创新技术。此外，由于存在某谕示$A$使得$\mathcal{NP}^A={\rm co}\mathcal{NP}^A$，我们继而探究其背后机理，并证明在$\mathcal{NP}^A={\rm co}\mathcal{NP}^A$及若干合理假设下，所有带谕示$A$的多项式时间共非确定性谕示图灵机构成的集合不可枚举，从而表明惰性对角化技术不适用于分离$\mathcal{NP}^A$与${\rm co}\mathcal{NP}^A$的第一阶段。作为副产品，我们再次得出$\mathcal{P}\neq\mathcal{NP}$的重要结论\cite{Lin21}，这从上文结果及$\mathcal{P}={\rm co}\mathcal{P}$的熟知事实中显而易见。接着，我们证明复杂度类${\rm co}\mathcal{NP}$存在中间语言，即存在语言$L_{inter}\in{\rm co}\mathcal{NP}$，它既不属于$\mathcal{P}$也不是${\rm co}\mathcal{NP}$完全问题。我们还总结了主要结果衍生的其他直接推论，如$\mathcal{NEXP}\neq{\rm co}\mathcal{NEXP}$以及属于证明复杂性领域的其他结论。最后，我们给出Frege证明系统的下界结果：任何Frege证明系统均不可能具有多项式有界性。