一阶逻辑语法

语法只规定哪些有限字符串是合法表达式以及它们如何分解，不给符号任何具体对象意义；意义要等结构和变量赋值提供。

一阶语法把符号串分层构造成项与公式：项指称对象，原子公式陈述关系，联结词与量词再生成复杂公式。递归定义使解析唯一、归纳证明可行，并明确变量出现何时自由、何时被量词绑定。语法本身不判断真假，真假只在结构与赋值下产生。

群语言可只有常元 $e$、二元函数 $\cdot$ 和一元函数 ${}^{-1}$；$\mathrm{\forall }x(x\cdot e=x)$ 是句子。若只写 $R(x)$，则 x 通常自由。元语言里的省略记号、自然语言括号和优先级必须能还原成唯一语法树。量词只遍历论域元素，不能在一阶语法中直接量化所有子集或关系。

若语言含函数 $f$ 与关系 $R$，则 $f(x,c)$ 是项，$R(f(x,c),y)$ 是公式；$R\wedge f$ 不是良构式。公式 $\mathrm{\forall }xR(x,y)$ 中 $x$ 被绑定而 $y$ 自由。替换 $y:=t$ 时若 $t$ 中变量会被现有量词捕获，必须先做变量改名。

严格语法使公式可编码、递归解析、替换和归纳证明，是满足关系、形式系统和 Gödel 编码的基础。不同签名决定可表达结构的词汇，但不改变一阶形成规则。

自由与约束变量公理库自由变量与约束变量Free and bound variables按量词作用域区分公式中由赋值决定的变量出现和被量化绑定的变量出现。控制代入，一阶替换引理公理库一阶替换引理Substitution lemma for first-order logic语法上的无捕获项替换与语义上的变量赋值更新相一致。连接语法替换与语义赋值。句法推导公理库句法可推导关系Syntactic derivability · Provability relation用有限形式证明把前提集与可由它推出的公式联系起来的元关系。只操作良构公式，Gödel 编码还把这些有限语法对象算术化。