Erdos-Szekeres型命题：一维中的Ramsey函数与可判定性

Erdos和Szekeres的一个经典且广泛使用的引理断言：对每个n，存在N使得每个N项实数序列a包含一个n项递增子序列或一个n项非递减子序列；定量地，具有此性质的最小N等于(n-1)^2+1。在本文的设定中，我们通过说谓词集合$\Phi=\{x_1<x_2,x_1\ge x_2\}$是Erdos-Szekeres的且Ramsey函数$ES_\Phi(n)=(n-1)^2+1$来表达这个引理。一般地，我们考虑任意有限个半代数谓词$\Phi=\{\Phi_1,\ldots,\Phi_m\}$，其中每个$\Phi_j=\Phi_j(x_1,\ldots,x_k)$是若干实数变量上的多项式方程和不等式的布尔组合。我们定义$\Phi$为Erdos-Szekeres的，如果对每个n存在N使得每个N项实数序列a有一个n项子序列b，使得至少一个$\Phi_j$在b上处处成立，这意味着对任意指标选择$i_1,i_2,\ldots,i_k$，$1\le i_1<i_2<\cdots<i_k\le n$，$\Phi_j(b_{i_1},\ldots,b_{i_k})$成立。记$ES_\Phi(n)$为具有上述性质的最小N。我们证明两个主要结果。第一，此设定中的Ramsey函数至多是双指数的（有时确实是双指数的）：对每个Erdos-Szekeres的$\Phi$，存在常数C使得$ES_\Phi(n) < \exp(\exp(Cn))$。第二，存在一个算法，给定$\Phi$，判定它是否是Erdos-Szekeres的；因此，一维的Erdos-Szekeres型定理原则上可以自动证明。