We start from a small open question, where Hetzl and Vierling asked whether two theories of induction, open induction and clause set cycles, are incomparable. They proved one direction and left the other open. Here we close it, and the proof is almost embarrassingly short, because the rules for addition can only fire when the first argument is $0$ or a successor, a Skolem constant is neither, so the terms $a{+}b$ and $b{+}a$ can never be touched, and a machine that can never touch them can never prove they are equal. The thing that separates the two theories is the order of two constants, and that order is a fact about numbers, not about symbols. We extract from this proof a small general principle, the Syntactic Invariance Principle, that names the shape of such arguments. We then close with a few speculative remarks on how this same shape appears, informally, in the known barriers to settling $\mathsf{P}$ versus $\mathsf{NP}$, where each barrier seems to point to a level of description that the techniques in the barrier cannot reach. We raise this as a suggestion rather than a theorem, since the analogy is real but we do not push it past the point where we can defend it. Along the way we raise an open question that the analogy suggests but does not settle, on whether a fast algorithm for $\SAT$, were it to exist, would always be exhibitable as a machine you can write down or whether it could be found, in some cases, only as a function on the numbers.

翻译：我们从Hetzl与Vierling提出的一个小型开放问题出发，询问两种归纳理论——开归纳与子句集循环——是否不可比较。他们证明了其中一个方向，而留下了另一个方向未解决。本文我们闭合了这一方向，其证明过程简短得近乎令人尴尬：因为加法规则仅当第一个参数为$0$或后继数时才能触发，而斯科伦常量既非$0$亦非后继数，因此项$a{+}b$与$b{+}a$永不能被触及；无法触及这些项的机器也永远无法证明它们相等。区分这两种理论的关键在于两个常量的顺序，而这种顺序是关于数字的事实，而非关于符号的事实。我们从这一证明中提炼出一个小型一般性原理——句法不变性原理——它命名了此类论证的形态。最后，我们以一些推测性评论作为结尾，探讨同样形态如何非正式地出现在解决$\mathsf{P}$与$\mathsf{NP}$问题的已知障碍中：每个障碍似乎都指向了该障碍中技术手段无法触及的描述层面。我们将此作为一种建议而非定理提出，因为其类比关系虽真实存在，但我们不会将其推进到无法辩护的程度。在此过程中，我们提出一个类比所暗示但未解决的问题：一个快速的$\SAT$算法（若存在的话）是否总能被展示为一台可写出的机器，还是在某些情况下只能作为数字上的函数被发现。