Hilbert's tenth problem, Gödel's incompleteness theorem
希尔伯特第十问题说的是：给定一个具有任意数量的未知量和有理整数系数的丢番图方程，能不能设计一个能行的过程可以通过在有限步内确定该方程是否有有理整数解。
一个丢番图方程，就是一个多项式$p=0$，如$x^2 − 4x + 3, x^3 − 3xy^2 + 7x − 9, −7x^2y^2 + 4y^2 − 17xy$等都是多项式，而√x和指数函数n^x都不是多项式。丢番图方程$p=0$的一组解就是一组对在多项式中的变元$x_1, x_2, x_k$的数字赋值。例如$x^2-4x+3$有两个根$1, 3$；$x^2+y^2-z^2$的解是毕达哥拉斯三元组$(3, 4, 5), (5, 12, 13)$, ……
很显然，希尔伯特问题的原始形式可以化归成是问：
存不存在一个算法能够判定任意一个丢番图方程在自然数中有没有解？
我们称一个数的集合$S$是 “丢番图的”，当且仅当存在一个多项式$p$，使得$p(x, y_1, y_2, . . . , y_k) = 0$的解$x$刚好就是那些属于$S$的数$x$。 例如所有要么是$2$的倍数要么是$3$的倍数的数是丢番图的，因为它们是丢番图方程$(x − 2y)(x − 3y)=0$的解；所有不是$2$的幂的数也是丢番图的，它们是方程$(x − y_1y_2)^2 + (y_1 − y_3 − 2)^2 + (y_1 − 2y_4 − 1^2)$的解；所有素数也是丢番图的。那么有没有什么对丢番图集的一般性的刻画呢？ 我们有： 所有丢番图集都是能行可枚举的。 而Matiyasevich证明了这个的逆命题：所有能行可枚举的数集都是丢番图的。（在此之前，Martin Davis和普特南已经证明了在一个数论猜想的前提下，所有能行可枚举的数集都是“指数丢番图”的（exponential diophantine），Julia Robinson发现了避免这个假设的方法。指数丢番图集就是丢番图集这个猜想被称为Robinson猜想（而tarski早就提出了一个相反的猜测，即指数丢番图集不是丢番图集）。最后M解决了这个问题。所以这个定理又叫作MRDP定理） 因为存在不可计算的能行可枚举集，所以我们可以立即得出希尔伯特第十问题的结果。 $∃y1∃y2, . . . ∃ykϕ(x, y1, y2, . . . , yk)$ 这样形式的公式，其中$ϕ$只有bounded quantier，被称为$Σ_1$的。我们有：一个数集是 能行可枚举的当且仅当对某个$Σ_1$公式 $ψ(x), n ∈ K$ 当且仅当 $N \models ψ(n)$，$N$是自然数的标准模型。 一个形如$∃y(τ_1(x, y) = τ_2(x, y))$的语言$L_A$的公式，其中$τ_i$是项，$y$是多元组，被称作 丢番图的。 而一个丢番图集恰好就是那些使得对于某个丢番图公式$ψ(x)，N \models ψ(n)$的$n$的集合。 而M证明的定理说得就是，对所有 语言$L_A$的$Σ1$公式$ψ(x)$，都存在一个丢番图公式$δ(x)$，使得$PA \vdash ∀x(ψ(x) ↔ δ(x))$。（事实上$PA$（Peano Arithmetic）可以弱化到$IΣ1$，其中只有$Σ_1$公式能做数学归纳）。 将否定符号插入进去我们就能得到， $ϕ(x)$ 是个$PA$的$Π_1$句，就会有一个形如$∀y(τ_1(x, y) ≠ τ_2(x, y))$公式使得$PA \vdash ∀x(ϕ(x) ↔ ∀y(τ_1(x, y) ≠ τ_2(x, y))$。 考虑原本的$Π_1$的$PA$的哥德尔句$G$，那么就会有一个相应的说的是一个特定的丢番图方程没有解的语句，这个语句在$PA$中是不可判定的。generalize一下，对任意的不可判定的$Π_1$语句都有。 现在我们考虑不用哥德尔句$G$来从MRDP定理证明不完备性定理。$T$是一个，例如包含了Robinson算术的，形式系统（可递归公理化的）。那么对有解数组$n$的正丢番图方程$τ_1(x) = τ_2(x)，x$是多元组，$T \vdash τ_1(n) = τ_2(n)$。 并且如果T是一致的，那么如果$T \vdash ∀x τ_1(x) ≠ τ_2(x)$，那就确实是这样（也就是说$∀x τ_1(x) ≠ τ_2(x)$是真的）。 现在，
- 我们考虑在$T$中可证的丢番图方程的哥德尔数的集合$D$，这是能行可枚举的；
- $U$是确实没有解的丢番图方程的哥德尔数的集合，$D ⊆ U$；
- $U$不是能行可枚举的（$U$的补是能行可枚举的，如果$U$还是能行可枚举的，那么$U$就将会是递归的，而这违反了MRDP定理）；
- 所以$D ≠ U$，并且有在$U - D$中的丢番图方程（的哥德尔数）。也就是说，有不可解，但我们不能在T中证明它不可解的丢番图方程（也就是形如$∀x τ_1(x) ≠ τ_2(x)$）的真的但不可证得公式），只要$T$是一致的并且包含了足够的算术的话。 $T$会否证这些真的但又不可证的语句吗？这留作一个练习。 现在，我们知道了，如果$T$是一个$ω$-一致的包含了足够算术的形式系统，那么就会有一个形如$∀x τ_1(x) ≠ τ_2(x)）$的公式，在T中不可判定。 这种对旧结果的新证明——也就是“重复造轮子”的工作——引起我们兴趣的原因是，比起原来的哥德尔句来，这个不可判定句似乎更为自然，更具数学意义（当然，具体的特定的丢番图方程可能是“不自然地”复杂的）。其次，虽然关于递归函数上我们要用到对角线化，但这个证明，似乎不依赖明显的自指技巧。
Verena Dyson, James Jones and John Sheperdson在Archiv Math. Logik 22 (1982) 51–60中证明了一个结果： 让$T$是一个可公理化的$ω$-一致的包含了Robinson算术的理论，那么就会存在一个$n$（根据具体的理论不同而不同），使得如下的句子在$T$中不可判定：
$∃a∃b∀(i ≤ n)∃s∃w∃p∃q∀j∀v∃e∃g$ $\{(s + w)^2 + 3w + s = 2i ∧ ([j = w ∧ v = q] ∨ [j = 3i ∧ v = p + q] ∨[j = s ∧ (v = p ∨ (i = n ∧ v = q + n))] ∨ [j = 3i + l ∧ v = pq] → a = v + e + ejb ∧ v + g = jb)\}$
哇……
Matiyasevich定理联系了两个领域，一个是递归论，一个是数论，并且会有一些意想不到的结果。
我们可以把一个丢番图集的degree说成是定义该集的方程中多项式的最小的degree。同样的，我们可以把这样一个定义方程中最小的未知数称为集合的dimension。这两个量都有绝对的上限，而且人们对确定这些上限很感兴趣。Skolem，Davis，Robinson和马蒂亚塞维奇都有一些结果。MRDP定理的证明已经在Coq中形式化（https://www.ps.uni-saarland.de/Publications/documents/Larchey-WendlingForster_2019_H10_in_Coq.pdf）。 同样，希尔伯特第十问题可以扩展到环上。