We analyze the cubic fragment $\mathcal D_3$ over $\mathbb N$ by isolating the uniform closure principle any total correct cubic solver would have to realize. In $\mathsf{HA}$ we give a fully constructive, additive and degree-controlled encoding of bounded verification: for each externally fixed bound, we effectively produce a finite system of degree-3 Diophantine equations whose solutions represent the existence of the corresponding finite proof or computation trace. The encoding is purely syntactic, using "gadgets" and "Carryless Pairing". In a classical metatheory (e.g. $\mathsf{PA}$) we show that the global solver hypothesis implies a uniform operator eliminating the bound inside $\mathcal D_3$, which is incompatible with standard non-uniformity/realizability constraints. Hence no uniform cubic can exist clasically.
翻译:我们通过分离任意完全正确的三次求解器必须实现的均匀闭包原理,分析了在自然数集上的三次片段$\mathcal D_3$。在$\mathsf{HA}$中,我们给出了一种完全构造性、可加且次数受控的有界验证编码方法:对于每个外部固定的界,我们能够有效地生成一个有限的三次丢番图方程组,其解对应着相应有限证明或计算轨迹的存在性。该编码是纯语法的,使用了“构件”和“无进位配对”技术。在经典元理论(如$\mathsf{PA}$)中,我们证明了全局求解器假设意味着存在一个在$\mathcal D_3$内部消除边界的均匀算子,这与标准的非均匀性/可实现性约束条件不相容。因此,在经典意义下不存在均匀的三次求解器。