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}$语句所断言其完全性的全体一般递归函数，在所有全体一般递归函数的集合中在增长率意义下是共尾的。随后我们提出一个论证，该论证利用了通过对角引理应用所构造的语句序列，这些语句在广义上是休·伍丁在其文集《数学中的真理》第18章文章“汉诺塔”中概述的“汉诺塔”构造的推广。该论证确立了在PA中可证$P \neq NP$的结果。我们进一步说明了如何将整个论证完全下放到SEFA系统。