自由变元与约束变元的区分：是引用的出现而非变元本身

谓词里的形参在逻辑学中称为自由变元（free variable）；对自由变元做量词化 （不管EXISTS还是FORALL），会把它转换为约束变元（bound variable，呼应 [[关系表达式的谓词含义可由关系变量谓词推导]]中已提前引入的这组术语）。自由 变元大致对应编程里的”参数”概念，约束变元没有直接对应的传统编程术语，它的 作用纯粹是把括号内的谓词和括号外的量词关联起来——正因如此，约束变元可以 被安全地改名而不改变整体含义（EXISTS x(x>3)和EXISTS y(y>3)语义完全 等价），但自由变元不能随意改名。这里有一个极容易混淆、书中特意强调”要时刻 警惕”的细节：真正区分”自由”与”约束”的对象，严格说不是变元本身，而是变元 在谓词里的每一次具体引用（出现，occurrence）。书中用EXISTS x(x>3)AND x<0这个例子说明：表达式里出现了3次x，前两次x（在EXISTS的作用域内）是约束 的，可以安全改名为y而不改变含义；第3次x（在EXISTS作用域外）却是自由的， 不能随意替换——如果把全部三个x都换成y，会得到EXISTS y(y>3)AND y<0，这个 表达式的含义和原表达式完全不同了。尽管”自由变元/约束变元”这种说法本身不太 严谨（连一些逻辑学教材都在延续这个不精确的表述），但因为它已经是约定俗成 的通用说法，作者也承认自己会继续沿用它，只是提醒读者时刻意识到这层潜藏的 混淆。命题最终可以重新定义为”所有变元都是约束变元（即不含任何自由变元）的 谓词”。