描述复杂性：ESO、最小不动点与有序结构

逻辑把算法预算换成描述方式。ESO 允许先猜出若干关系表，再用固定的一阶规则检查，这与 NP 的短证书接口相吻合。LFP 则从空关系开始，反复执行一条单调规则，直到没有新元组；固定元数使能加入的元组数量只有多项式多个。

顺序使公式可以组织元素与元组，从而表示机器的时间、位置和相邻配置。算法读入一个数组时自然看得到存储次序；一份只谈边关系的逻辑公式却没有自动获得数组下标。式 (2) 的有序条件把这项信息显式交给公式。

从正出现到最小不动点 ​

设 $S\subseteq T$。在 $\phi$ 的否定范式中，若一个 $R(\overline{b})$ 原子在 $R:=S$ 下为真，在 $R:=T$ 下仍为真。输入关系原子及它们的否定不随 $R$ 改变。合取和析取保持蕴涵；存在量词可以保留原见证；全称量词则对每个赋值使用归纳结论。沿一阶公式结构归纳，得到

因此可从底部迭代：

$S_0\subseteq S_1$ 自然成立；单调性归纳给出 $S_i\subseteq S_{i+1}$。每次严格变化至少增加一个元组，总共只有 $n^a$ 个可能元组，所以至多发生 $n^a$ 次严格变化；直接实现至多再求值一次即可检测稳定。

稳定值 $S_{\ast }$ 满足 $F(S_{\ast })=S_{\ast }$。对任意不动点 $T$，从 $S_0\subseteq T$ 出发，

所以 $S_{\ast }\subseteq T$。这证明了最小性，是Knaster–Tarski 定理公理库Knaster–Tarski 不动点定理Knaster-Tarski fixed-point theorem · Tarski fixed-point theorem完备格上的单调自映射之全部不动点构成完备格，并具有规范的最小与最大不动点。在有限关系格上的具体构造。单调性并不意味着任意 $S$ 都满足 $S\subseteq F(S)$；升链性质来自从空集启动。

嵌套时，内部不动点的单调性也可逐轮验证：若外部参数关系增大，使内部算子对每个候选关系的输出都增大，则其从空集开始的每轮结果都包含原结果，最小不动点也随之增大。将这一观察和正、负出现的结构归纳结合，就能递归处理良构 FO(LFP) 中的参数关系。

为什么固定 FO(LFP) 公式能在多项式时间求值 ​

一个固定一阶公式只有固定多个量化位置，可逐一枚举域元素完成求值；指数取决于公式，而不随输入结构改变。计算一个 $a$ 元算子的完整输出时，再枚举 $n^a$ 个候选元组；迭代至多 $n^a+1$ 轮，仍只有固定多项式因子。

对嵌套 LFP，沿语法结构归纳：每个真子公式的求值已有多项式界，外层增加固定元组枚举和固定元数的有限迭代。嵌套深度、关系元数和参数个数都是固定公式的一部分，所以多项式复合仍是多项式。显式编码使 $N\ge n$，因此这也是输入位长的多项式算法。

这个求值方向不依赖顺序；有序条件承担的是式 (2) 中“任意 P 性质都能被表达”的反方向。若公式也作为输入，量词数与元数不再固定，上面的指数就不能继续当成常数。

为什么固定 ESO 句子给出 NP 验证器 ​

对 $\mathrm{\exists }{S}_1\cdots \mathrm{\exists }{S}_r\psi$，若 $S_i$ 的元数为 $a_i$，用完整特征表猜测这些关系，证书位数为

$r,a_i$ 都固定，故证书长度多项式有界。接着在扩充结构上验证固定一阶公式 $\psi$，时间同样多项式。存在一个通过验证的表，恰好等价于 ESO 句子为真，完成 $\mathrm{ESO}\subseteq \mathrm{NP}$ 的证明。二阶量词没有一次猜测任意大小的无限集合。

四点有向链的全部 LFP 轮次 ​

取 $A=\{a,b,c,d\}$、$E=\{(a,b),(b,c),(c,d)\}$，使用

这是对 $R$ 正出现的公式。记 $D=\{(a,a),(b,b),(c,c),(d,d)\}$，用 $ab$ 简写有序对 $(a,b)$，得到：

一般地，对 $i\ge 1$，$R_i$ 恰由长度至多 $i$ 的有向游走端点组成，允许长度零。第一轮给出等号与单边。归纳时，第三个析取项给已有游走追加最后一条边；反过来，任何长度在二到 $i+1$ 之间的游走都可以拆成至多 $i$ 步的前段与最后一条边。因此没有加入不可达对，也没有漏掉最终可达对。

所以稳定关系中 $ad$ 为真、$da$ 为假、$dd$ 为真。去掉 $x=y$ 会改成正长度可达性，不能继续把所有对角元自动放进答案。

ESO 三染色：猜三张集合表再逐边检查 ​

对简单无向图，使用三个一元关系 $C_1,C_2,C_3$。以下句子定义至多三色可染性：

这里最后一行的有限析取是三个普通公式的简写，没有引入额外的数值量词。第一部分要求每个顶点恰属于一个颜色类，第二部分要求每条边两端颜色不同。

给定合法染色，取三种颜色的顶点集合就得到满足句子的解释。反过来，满足第一部分的三张表给每个顶点唯一颜色，第二部分使这个颜色赋值合法。于是两个方向均成立。某些颜色类可以为空；“三染色”不要求必须用足三种颜色。

三角形 $a,b,c$ 加一个孤立点 $d$ 有见证

$a,d$ 之间没有边，所以可以同色。$K_4$ 则无见证：四个顶点进入三个颜色类，必有同类的一对，而每对顶点之间都有边。若允许自环，公式也会自动拒绝带自环图，因为环的两端就是同一个已着色顶点。

编码长度与输入顺序的两道边界 ​

一个具体图编码可以由一元串 $1^n$、分隔符和按顶点编号字典序排列的 $n^2$ 个邻接位组成，位长为 $\mathrm{\Theta }(n+n^2)$。若还显式存储全序关系表，最多增加 $n^2$ 位。固定关系签名的一般编码则使用 $n+\sum _i{n}^{a_i}$ 量级的位数；换用其他合理的显式编码只引入多项式开销。

不能把“一元列出域”悄悄改成只给二进制整数 $n$、其余结构由短程序描述。尤其对空关系签名，二进制 $n$ 的位长只有 $\mathrm{\Theta }(\log n)$，枚举 $n^a$ 个元组可能已经是编码长度的指数时间。Fagin 原文也专门区分这两种计量；其作者补充摘要说明使用一元域大小后如何统一为式 (1)。[1]

同样，编码使用顶点编号，不代表不带 $<$ 的公式能够访问编号次序。以只有等号的纯集合结构为例，任意元素置换都是自同构；一阶或 LFP 的无参数定义都必须在这些置换下保持。域至少有两个元素时，没有一个严格全序能被所有互换保持，因此不能在这种结构中无参数定义出一个总顺序。

这个自同构论证解释了为何不能默默给公式增加一个顺序；它本身没有证明所有关于无序 FO(LFP) 的表达力下界。式 (2) 的精确适用范围仍应保留为有序有限结构。

描述复杂性把“用什么计算资源判定”与“用什么逻辑形式描述”放在同一接口下。ESO 中的关系表成为 NP 证书，LFP 中的有限升链成为确定性求值过程；两个方向都明确支付关系元组数量与公式求值的成本。

一般刻画的机器模拟方向需要更多构造。ESO 可以用额外关系记录猜测的计算历史并核验局部转移；有序 LFP 则能用固定长度元组表示多项式范围内的时间与带位置，按转移规则生成历史。[1,2] 这说明顺序和固定元数为什么出现在定理中，但这些提纲不能替代引用文献的完整模拟证明。

读者可以用上述两个实例自检接口：三染色猜测的是 $3n$ 位的一元关系表，而不是三个颜色编号字符串的无限集合；链的可达性最多在 $n^2$ 个二元事实中增长，而不是枚举所有可能路径。表达力结论、固定公式的求值算法、特定实例的结果是三种不同层次的陈述。