MathLabs

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

第 3/9 步：戴维斯1953年的猜想:r.e.集合恰好就是丢番图集合
上一步下一步
通俗地说

在库尔特·哥德尔早先证明可计算概念能被算术化为关于数的命题这一工作的基础上,马丁·戴维斯于1953年迈出了具体的第一步:他证明每个可枚举集合都能用一个只带一个受限“对所有”量词、其后跟一个纯代数命题的公式来描述(“戴维斯范式”)。

戴维斯猜想这个受限量词最终可以完全消去,只剩下一个纯多项式方程——也就是说,可枚举集合与丢番图集合其实是同一个概念。如果成立,这将是关键的桥梁,能让图灵那不可判定的停机问题直接编码为关于多项式整数根的问题。

S recursively enumerable =? {a:∃x1,…,xn∈Z≥0, P(a,x1,…,xn)=0}S \text{ recursively enumerable} \ \overset{?}{=} \ \{a : \exists x_1, \ldots, x_n \in \mathbb{Z}_{\ge 0},\ P(a, x_1, \ldots, x_n) = 0\}
详细分析

1953年,马丁·戴维斯猜想每个递归可枚举集合 S⊆Z≥0S \subseteq \mathbb{Z}_{\ge 0} 都等于一个丢番图集合:存在一个整数系数多项式 PP,使得 a∈Sa \in S 当且仅当 ∃x1,…,xn∈Z≥0\exists x_1, \ldots, x_n \in \mathbb{Z}_{\ge 0} 满足 P(a,x1,…,xn)=0P(a, x_1, \ldots, x_n) = 0。这建立在戴维斯自己“戴维斯范式”结果之上——该结果本身细化了哥德尔对可计算谓词的算术化——即每个r.e.集合已经拥有形如 ∃x ∀y≤x ∃z1,…,zk\exists x\, \forall y \le x\, \exists z_1, \ldots, z_k(多项式方程)的定义,也就是说,阻挡在纯粹存在型(丢番图)定义之前的,只剩一个受限的全称量词。

消去这唯一一个受限量词,结果需要将近二十年的进一步研究,因为这要求找到能够以某种方式模拟受限搜索与指数规模计算的多项式方程——而普通的多项式增长(被输入的固定次幂所限制)看起来从根本上太弱,做不到这一点。

从1950年代开始发展出的前进道路,是精确找出究竟缺少了什么额外要素;下一步将把它精确地确定为一个具有指数增长的关系。

本步骤中的术语
戴维斯范式
戴维斯1953年的结果:每个递归可枚举集合都可以用一个公式来定义,该公式在一个纯粹存在型多项式命题之前恰好有一个受限的全称量词——这正是戴维斯猜想试图消除的那道精确缺口。
本步骤用到的知识
递归函数与图灵机