We show that it is provable in PA that there is an arithmetically definable sequence $\{φ_{n}:n \in ω\}$ of $Π^{0}_{2}$-sentences, such that - PRA+$\{φ_{n}:n \in ω\}$ is $Π^{0}_{2}$-sound and $Π^{0}_{1}$-complete - the length of $φ_{n}$ is bounded above by a polynomial function of $n$ with positive leading coefficient - PRA+$φ_{n+1}$ always proves 1-consistency of PRA+$φ_{n}$. One has that the growth in logical strength is in some sense "as fast as possible", manifested in the fact that the total general recursive functions whose totality is asserted by the true $Π^{0}_{2}$-sentences in the sequence are cofinal growth-rate-wise in the set of all total general recursive functions. We then develop an argument which makes use of a sequence of sentences constructed by an application of the diagonal lemma, which are generalisations in a broad sense of Hugh Woodin's "Tower of Hanoi" construction as outlined in his essay "Tower of Hanoi" in Chapter 18 of the anthology "Truth in Mathematics". The argument establishes the result that it is provable in PA that $P \neq NP$. We indicate how to pull the argument all the way down into SEFA.

翻译：我们证明在PA中可证存在一个算术可定义的$Π^{0}_{2}$语句序列$\{φ_{n}:n \in ω\}$，满足以下条件：- PRA+$\{φ_{n}:n \in ω\}$是$Π^{0}_{2}$可靠且$Π^{0}_{1}$完备的；- $φ_{n}$的长度被一个具有正首项系数的$n$的多项式函数上界控制；- PRA+$φ_{n+1}$总能证明PRA+$φ_{n}$的1-一致性。该序列逻辑强度的增长在某种意义上是“尽可能快的”，这体现在：序列中真$Π^{0}_{2}$语句所断言其完全性的全体一般递归函数，在增长速率的意义上与所有全体一般递归函数的集合是共尾的。随后，我们提出一个论证，该论证利用通过对角线引理应用所构造的一个语句序列，这些语句在广义上是Hugh Woodin在其文集《数学中的真理》第18章文章“Tower of Hanoi”中概述的“汉诺塔”构造的推广。该论证确立了在PA中可证$P \neq NP$的结果。我们进一步说明了如何将这一论证完全下放到SEFA系统中。