MathLabs

解法：MRDP定理:丢番图集合恰为递归可枚举集合(1970年)

第 5/9 步：戴维斯–普特南–鲁滨逊1961年:每个r.e.集合都是指数丢番图的
上一步下一步
通俗地说

“指数丢番图方程”是一种比普通多项式方程更宽松的方程:它允许变量也出现在指数位置,比如 xy=zx^y = z,而不仅仅是相乘相加。1961年,马丁·戴维斯、希拉里·普特南与朱莉娅·鲁滨逊证明,有了这种额外的宽松性,每一个可枚举集合都已经能被精确捕获——没有例外。

这意味着戴维斯1953年最初猜想中剩余的全部困难,已经被压缩为一个被精确表述的技术障碍:找到一种方法把指数重新压回普通多项式形式,而这恰恰就是上一步鲁滨逊的JR假设。

r.e. set  ⟺  ∃ exponential Diophantine eq. Q(a,x1,…,xk,y1,…,yl)=0, yi appear as exponents\text{r.e. set} \iff \exists \text{ exponential Diophantine eq. } Q(a, x_1, \ldots, x_k, y_1, \ldots, y_l) = 0,\ y_i \text{ appear as exponents}
详细分析

指数丢番图方程允许变量出现在指数位置,例如 Q(a,x1,…,xk,y1,…,yl)=0Q(a, x_1, \ldots, x_k, y_1, \ldots, y_l) = 0,其中某些 yiy_i 出现在 QQ 中的某个指数位置;集合 SS 是指数丢番图的,是指其成员关系可以像普通丢番图集合那样,通过这样一个方程来表达。

1961年,戴维斯、普特南与鲁滨逊证明每个递归可枚举集合都是指数丢番图的,方法是把戴维斯范式(单一受限全称量词)与鲁滨逊此前的存在可定义性技术结合起来,在有指数规模构件(再一次是佩尔方程的解)可用时消去受限量词。这就在更广泛的指数方程这一类别上完全证明了戴维斯猜想,尽管最初的猜想只涉及普通多项式方程。

这个1961年的结果与戴维斯1953年完整猜想之间剩下的全部缺口,现在恰好就是鲁滨逊的JR假设:找到一个纯多项式(非指数)、却具有指数增长的丢番图关系,那么每一个指数丢番图定义都可以改写成普通形式。堵上这最后一个缺口,一直等到1970年才实现,这正是下一步的主题。

本步骤中的术语
指数丢番图方程
由整数变量的加法、乘法与幂运算构成的方程,例如 xy+z=wx^y + z = w,其中允许变量(不仅仅是常数)出现在指数位置——这是一类表达能力严格强于普通多项式方程的方程。
本步骤用到的知识
一次不定方程