一阶逻辑语法

先区分“一个对象”与“关于对象的一句话”。在整数语言中，$x+1$ 指向一个数，$x+1<y$ 则是在比较两个数。前者对应项，后者对应公式。项可以嵌入项，例如 $(x+1)+1$；公式可以用“且”“或”组合，也可以被“对所有”“存在”这样的量词包围。

签名只给出可以使用的符号及接口，不预先赋予数学意义。符号 $f$ 可以在一个结构中解释为后继，在另一个结构中解释为恒等函数。$R(f(x),y)$ 是否合式只取决于符号元数；它是否为真还需要结构和对自由变量的赋值。这样，语法检查与语义判断便被分开。

括号确定构造层次，量词确定作用域。$\mathrm{\forall }x(P(x)\to Q(x))$ 的两个 $x$ 都由外层量词约束；$(\mathrm{\forall }xP(x))\to Q(x)$ 中，最后一个 $x$ 不在该量词的作用域内。去掉括号之前，需要先规定优先级，不能靠句子看起来“差不多”来判断结构。

从符号表逐层生成 ​

对含 $c,f,R$ 的上述签名，$x$ 和 $c$ 是项，继而 $f(x)$、$f(f(c))$ 是项，因此 $R(f(x),c)$ 是原子公式，$\mathrm{\exists }xR(f(x),c)$ 是公式。每一步都能指出使用了哪条构造规则。

相反，$f(x,c)$ 给一元函数提供了两个参数，不合式；$R(x)$ 少了一个参数；$f(R(x,c))$ 则把公式塞进了应当放项的位置。它们不是“可能为假的公式”，而是没有被这套语法生成的表达式。

自由变量必须按作用域计算 ​

单独计算项时，其中的变量出现都记入该项的自由变量集合；放进公式后，这些出现仍可能被外层量词绑定。例如 $f(x)$ 含变量 $x$，但公式 $\mathrm{\forall }xP(f(x))$ 没有自由变量。公式的自由变量集合 $\mathrm{FV}$ 可递归计算：原子公式取各参数中的变量并集，否定不改变该集合，二元联结词取左右子公式的并集，而量词删去自己绑定的变量：

没有自由变量的公式称为句子。例如

的自由变量集合为 $\{y\}$：左支的 $y$ 自由，右支的 $y$ 被内层量词约束，所有 $x$ 都被外层量词约束。同一个名字在一个公式中可以有自由出现，也可以有约束出现；不能只统计名字是否出现。

替换为什么需要避免捕获 ​

记 $\phi [t/y]$ 为把 $\phi$ 中自由出现的 $y$ 替换成项 $t$。若将 $\mathrm{\forall }xR(x,y)$ 中的自由 $y$ 替换成 $x$，直接按字符替换会得到 $\mathrm{\forall }xR(x,x)$，新放进去的 $x$ 被外层量词捕获了。

正确做法是先把原来的绑定变量改成新名字 $z$，得到 $\mathrm{\forall }zR(z,y)$，再替换为

此时新 $x$ 仍然自由。两种结果确实可能意义不同：若论域含两个不同对象，$R$ 解释为相等，那么 $\mathrm{\forall }xR(x,x)$ 为真，而 $\mathrm{\forall }zR(z,x)$ 对任意给定的 $x$ 都为假。捕获不是排版上的小变化，而是改变了所断言的事情。

仅一致地更换绑定变量、并避免捕获，得到的是 $\alpha$-等价公式。它保留绑定结构；任意改动自由变量、或把一个名字的所有出现无差别替换，并不属于这种改名。

归纳语法同时给出递归算法与证明方法 ​

语法分析得到结构后，可以递归计算公式长度、自由变量集合、量词深度，也可以递归实现捕获规避替换。证明这些操作正确时使用结构归纳：先检查变量或原子公式，再证明每个构造步骤在子表达式正确的条件下仍正确。证明的分支直接对应语法规则，因此不需要猜测所有字符串可能长什么样。

一阶逻辑公理库一阶逻辑First-order logic · Predicate logic在命题逻辑上加入对象、关系、函数与量词的形式语言和模型语义。的语义随后给项一个对象值，给公式一个满足关系。替换引理把两层接起来：在捕获规避条件下，语法上以项替换变量，等价于语义上把该变量的赋值改成此项的解释值。漏掉绑定处理，后续可靠性证明便失去了这一连接。

“一阶”表示量词对论域中的对象取值；它不允许直接把普通关系符号或函数符号当作量词变量。用对象编码公式、函数或证明是另一回事：语法的哥德尔编码公理库语法的哥德尔编码Gödel coding of syntax · Arithmetization of syntax把有限项、公式和自由变量替换编码为自然数运算，为算术内部表达语法提供接口。可以把语法对象变成自然数来研究，但“对编码数字量化”与直接增加高阶量词是不同的语言设计。