We prove in this paper that there is a language $L_s$ accepted by some nondeterministic Turing machine that runs within time $O(n^k)$ for any positive integer $k\in\mathbb{N}_1$ but not by any ${\rm co}\mathcal{NP}$ machines. Then we further show that $L_s$ is in $\mathcal{NP}$, thus proving a groundbreaking result that $$\mathcal{NP}\neq{\rm co}\mathcal{NP}. $$ The main techniques used in this paper are simulation and the novel new techniques developed in the author's recent work. Our main result has profound implications, such as $\mathcal{P}\neq\mathcal{NP}$, etc. Further, if there exists some oracle $A$ such that $\mathcal{P}^A\ne\mathcal{NP}^A={\rm co}\mathcal{NP}^A$, we then explore what mystery lies behind it and show that if $\mathcal{P}^A\ne\mathcal{NP}^A={\rm co}\mathcal{NP}^A$ and under some rational assumptions, then the set of all ${\rm co}\mathcal{NP}^A$ machines is not enumerable, thus showing that the simulation techniques are not applicable for the first half of the whole step to separate $\mathcal{NP}^A$ from ${\rm co}\mathcal{NP}^A$. Finally, a lower bounds result for Frege proof systems is presented (i.e., no Frege proof systems can be polynomially bounded).

翻译：本文证明：存在一个语言 $L_s$，可被某个在 $O(n^k)$ 时间内运行的非确定性图灵机接受（其中 $k\in\mathbb{N}_1$ 为任意正整数），但该语言不能被任何 ${\rm co}\mathcal{NP}$ 机器接受。进一步，我们证明 $L_s$ 属于 $\mathcal{NP}$，从而得出一个开创性结论：$$\mathcal{NP}\neq{\rm co}\mathcal{NP}. $$ 本文采用的主要技术是模拟方法以及作者近期工作中发展的新型技术。我们的主要结果具有深远意义，例如可推导出 $\mathcal{P}\neq\mathcal{NP}$ 等结论。此外，若存在某个谕示 $A$ 使得 $\mathcal{P}^A\ne\mathcal{NP}^A={\rm co}\mathcal{NP}^A$，我们将探究其背后的奥秘，并证明：若 $\mathcal{P}^A\ne\mathcal{NP}^A={\rm co}\mathcal{NP}^A$ 且在若干合理假设下，则所有 ${\rm co}\mathcal{NP}^A$ 机器的集合不可枚举，从而表明模拟技术不适用于分离 $\mathcal{NP}^A$ 与 ${\rm co}\mathcal{NP}^A$ 的整个步骤的前半部分。最后，我们给出弗赖格证明系统的一个下界结果（即不存在多项式有界的弗赖格证明系统）。