Linguae Ordinis-Primi 一阶语言
由符号（symbol）组成的非空集合称为字母表（alphabet）．字母表 $\mathcal A$ 中的符号所组成有限长序列称为 $\mathcal A$ 上的字符串（string）或词语（word）．$\mathcal A$ 上的所有字符串所组成的集合记作 $\mathcal A^\ast$．任一字符串 $\zeta\in\mathcal A^\ast$ 中所含的符号数量（计算重复的符号）称为 $\zeta$ 的长度（length）．空字符串（简称空串）也属于 $\mathcal A^\ast$，其长度为 $0$，记作 $\square$．
若存在 $\mathbb N$ 到集合 $M$ 的满射，则称 $M$ 是可数（countable）的．若 $M$ 为无限集，则 $M$ 若非可数集合，则称为不可数（uncountable）集合．可数集与有限集统称为至多可数（at most countable）集合．
〔引理 1.a〕：
对任一非空集合 $M$，以下条件等价：
(α) $M$ 至多可数；
(β) 存在满射 $\alpha:\mathbb N\to M$；
(γ) 存在单射 $\beta:M\to\mathbb N$．
〔证明〕：
(α) $\Rightarrow$ (β)：
令 $M$ 至多可数，若 $M$ 可数，则由前文定义得证．若 $M$ 有限，令 $M:=\{a_0,\,a_1,\,\cdots,\,a_m\}$，定义 $\alpha$ 如下：
显然 $\alpha$ 为满射．
(β) $\Rightarrow$ (γ)：
令 $\alpha:\mathbb N\to M$ 为满射，定义 $\beta(b)$ 等于满足 $\alpha(n)=b$ 的最小 $n\in\mathbb N$，显然 $\beta$ 为单射．
(γ) $\Rightarrow$ (α)：
令 $\beta:M\to\mathbb N$ 为单射，$M$ 为有限集时显然．设 $M$ 为无限集，归纳定义 $\alpha:\mathbb N\to M$ 如下：$\alpha(0)$ 等于在 $\beta$ 作用下，像在 $\mathbb N$ 中最小的 $a\in M$．对任意 $n\in\mathbb N$，$\alpha(n+1)$ 等于在 $\beta$ 作用下，像在 $\mathbb N$ 中大于 $(α(0)),⋯,β(α(n))$ 而最小的 $a\in M$．
$\beta$ 的像是 $\mathbb N$ 的无限子集，由此可知 $\alpha$ 对任意 $n\in\mathbb N$ 均可定义，显然每个 $a\in M$ 均属于 $\alpha$ 的像，于是 $\alpha$ 是满射，这意味着 $M$ 可数．
■
〔引理 1.b〕：
若 $\mathcal A$ 是至多可数的字母表，则 $\mathcal A^\ast$ 可数．
〔证明〕：
即 $p_n$ 为第 $n$ 个质数，即 $p_1=2$，$p_2=3$，以此类推．若 $\mathcal A$ 有限，则 $\mathcal A:=\{a_0,\,\cdots,\,a_n\}$；若 $\mathcal A$ 可数，则 $\mathcal A:=\{a_0,\,a_1,\,a_2,\,\cdots\}$．定义映射 $\beta:\mathcal A^\ast\to \mathbb N$ 如下：
显然 $\beta$ 为单射，由此则 $\mathcal A^\ast$ 至多可数，而 $\mathcal A^\ast$ 无法为有限集（考虑 $a_0,\,a_0a_0,\,a_0a_0a_0,\,\cdots\in\mathcal A^\ast$），便得证．
■
〔定义 1.1〕：
令字母表 $\mathcal A$ 包含以下符号：
无限个变元（variable）：$v_0,\,v_1,\,v_2,\,\cdots$；
五个逻辑联结词：$\neg,\,\land,\,\lor,\,\to,\,\leftrightarrow$（非、与、或、若–则、当且仅当）；
两个逻辑量词：$\forall,\,\exists$（全称量词、存在量词）；
等值符号：$\equiv$；(1)
括号：$(,\,)$．
字母表 $S$ 包含以下符号：
若干个（或 $0$ 个，下同）$n$ 元关系符号（其中 $n\geq 1$），后文默认记作 $R^n_0,\,R^n_1,\,R^n_2,\,\cdots$ 或 $R^n$；
若干个 $n$ 元函数符号（其中 $n\geq 1$），后文默认记作 $f^n_0,\,f^n_1,\,f^n_2,\,\cdots$ 或 $f^n$；
若干个常元（constant），后文记作 $c_0,\,c_1,\,c_2,\,\cdots$，或 $c$．
记 $\mathcal A_S:= \mathcal A\cup S$，则 $\mathcal A_S$ 是一个一阶语言（first-order language）的字母表，$S$ 是该一阶语言的符号集（symbol set）．不同的 $S$ 决定了不同的一阶语言．
Termini & Formulae 项与公式
〔定义 1.2〕：
通过有限次应用以下所给出的规则得到的 $\mathcal A^\ast_S$ 中的字符串称为 $S$–项（$S$-term）：
(T1) 任一变元均为 $S$–项；
(T2) $S$ 中的任一常元均为 $S$–项；
(T3) 若 $t_1,\,\cdots,\,t_n$ 均为 $S$–项，而 $f \in S$ 是一个 $n$ 元函数符号，则 $ft_1\cdots t_n$(2) 亦为 $S$–项．
$S$–项的集合记为 $T^S$．
〔定义 1.3〕：
通过有限次应用以下所给出的规则得到的 $\mathcal A^\ast_S$ 中的字符串称为 $S$–公式（$S$-formula）：
(F1) 若 $t_1$ 与 $t_2$ 为 $S$–项，则 $t_1\equiv t_2$ 为 $S$–公式；
(F2) 若 $t_1,\,\cdots,\,t_n$ 均为 $S$–项，而 $R\in S$ 是一个 $n$ 元关系符号，则 $Rt_1\cdots t_n$ 为 $S$–公式；
(F3) 若 $\varphi$ 为 $S$–公式，则 $\neg\varphi$（否定）亦为 $S$–公式；
(F4) 若 $\varphi$ 与 $\psi$ 为 $S$–公式，则 $(\varphi\land\psi)$（合取）、$(\varphi\lor\psi)$（析取）、$(\varphi\to\psi)$（蕴含）、$(\varphi\leftrightarrow\psi)$（双条件）均为 $S$–公式；
(F5) 若 $\varphi$ 为 $S$–公式，而 $x$ 为变元，则 $\forall x\varphi$ 与 $\exists x\varphi$ 均为 $S$–公式．
$S$–公式的集合记为 $L^S$．
由以上规则得到项或公式的过程称为导出（derivation），而通常把这样的规则系统称为演算（calculus）．例如，设符号集 $S_\mathrm t=\{f,\,g,\,c\}$（其中 $f$ 为一元函数符号，$g$ 为二元函数符号），则关于 $S_\mathrm t$ 的项演算可导出项 $gv_0fgv_4c$(3)．又如，设符号集 $S_\mathrm f=\{R\}$，则关于 $S_\mathrm f$ 的公式演算可导出公式 $\forall v_0\forall v_1\forall v_2((Rv_0v_1\land Rv_1v_2)\to Rv_0v_2)$．
〔引理 1.c〕：
若符号集 $S$ 至多可数，则 $T^S$ 与 $L^S$ 可数．
〔证明〕：
若 $S$ 至多可数，则 $\mathcal A_S$ 亦然（$\mathcal A_S=\mathcal A\cup S$），由引理 1.b 则 $\mathcal A^\ast_S$ 亦然．
$T^S$ 与 $L^S$ 均为 $\mathcal A^\ast_S$ 的子集，因此二者亦至多可数．
由于 $T^S$ 包含无限个变元 $v_0,\,v_1,\,v_2,\,\cdots$，而由此则 $L^S$ 包含相应的无限个公式 $v_0\equiv v_0,\,v_1\equiv v_1,\,v_2\equiv\,v_2,\,\cdots$，因此二者均为无限集，便得证．
■
Inductio 归纳法
设符号集为 $S$，且令 $Z\subseteq\mathcal A^\ast_S$ 为 $\mathcal A_S$ 上的一个字符串集合．
演算中的规则或是指明特定字符串属于 $Z$，或是指明对于若干字符串 $\zeta_1,\,\cdots,\,\zeta_n,\,\zeta$，若 $\zeta_1,\,\cdots,\,\zeta_n\in Z$，则 $\zeta \in Z$．后一种规则会以记号表述为：
令 $n=0$，则得到上文所述的前一种规则（“无前提”的规则），于是项演算的规则可表述如下：
(T1) $\dfrac{\quad}v$；
(T2) $\dfrac{\quad}{c}$，若 $c\in S$；
(T3) $\dfrac{t_1,\,\cdots,\,t_n}{f^nt_1\cdots t_n}$，若 $f^n\in S$．
对于指定的字符串集合 $Z$，若要证明其所有元素均具有性质 $P$，则可证明其充分条件：
对于演算 $\mathfrak C$ 的任一规则 $\dfrac{\;\zeta_1,\,\cdots,\,\zeta_n\;}{\zeta}$，若 $\zeta_1,\,\cdots,\,\zeta_n$ 在 $\mathfrak C$ 中可导出且均具有性质 $P$（称为归纳假设（induction hypothesis）），则 $\zeta$ 亦有性质 $P$．
这一证明过程称为演算 $\mathfrak C$ 上的归纳（induction）．
当 $\mathfrak C$ 为项演算，则对于项的归纳证明即为证明以下各条：
(T1)’ 所有变元具有性质 $P$；
(T2)’ $S$ 中所有常元具有性质 $P$；
(T3)’ 若 $S$–项 $t_1,\,\cdots,\,t_n$ 均具有性质 $P$，且 $f^n\in S$，则 $f^nt_1\cdots t_n$ 亦具有性质 $P$．
当 $\mathfrak C$ 为公式演算，则相应地，对于公式的归纳证明即为证明以下各条：
(F1)’ 所有形如 $t_1\equiv t_2$ 的 $S$–公式均具有性质 $P$；
(F2)’ 所有形如 $R^nt_1\cdots t_n$ 的 $S$–公式均具有性质 $P$；
(F3)’ 若 $S$–公式 $\varphi$ 具有性质 $P$ ，则 $\neg\varphi$ 亦具有性质 $P$；
(F4)’ 若 $S$–公式 $\varphi$ 与 $\psi$ 具有性质 $P$，则 $(\varphi\land\psi),\,$ $(\varphi\lor\psi),\,$ $(\varphi\to\psi),\,$ $(\varphi\leftrightarrow\psi)$ 均具有性质 $P$；
(F5)’ 若 $S$–公式具有性质 $P$，而 $x$ 为变元，则 $\forall x\varphi$ 与 $\exists x\varphi$ 均具有性质 $P$．
〔例 1’a〕：
对任意符号集 $S$，空串 $\square$ 既非 $S$–项亦非 $S$–公式．
〔证明〕：
设性质 $P$ 如下：
对任意字符串 $\zeta\in\mathcal A^\ast_S$，$\zeta$ 具有性质 $P$ 当且仅当 $\zeta$ 非空．
对项归纳证明：
(T1)’，(T2)’：显然所有变元与 $S$ 中的所有常元均非空，即均具有性质 $P$．
(T3)’：由规则 (T3) 所得到的项必然起始于函数符号，因此必然非空．
对公式归纳证明：
由各条规则所得到的公式必然含有至少一个逻辑联结词、逻辑量词、等值符号、关系符号，因此均具有性质 $P$．
■
〔例 1’b〕：
对于任一符号集 $S$，所有 $S$–公式具有同等数量的左括号 “$\,(\,$” 与右括号 “$\,)\,$”．
〔证明〕：
对项归纳证明可得所有项都不含有括号．
对公式归纳证明，并设性质 $P$ 如下：
对任意字符串 $\zeta\in\mathcal A^\ast_S$，$\zeta$ 具有性质 $P$ 当且仅当 $\zeta$ 具有同等数量的左括号与右括号．
于是，考虑以下情况：
(T1)’：$\varphi=t_1\equiv t_2$ 时，观察可知 $\varphi$ 没有任何括号，因此 $\varphi$ 具有性质 $P$．
(T2)’：$\varphi=\neg \psi$ 时，假设 $\psi$ 具有性质 $P$．除了 $\psi$ 所具有的括号外，$\varphi$ 不具有其余括号，因此 $\varphi$ 具有性质 $P$．
(T3)’：$\varphi=(\psi \diamond \chi)$ 时(4)，假设 $\psi,\,\chi$ 均具有性质 $P$，则 $\varphi$ 相比 $\psi$ 与 $\chi$ 多一组括号，$\varphi$ 具有性质 $P$．
(T4)’：与 (T2)’ 同理．
■
〔引理 1.d〕：
(a) 对任意项 $t$ 与 $t’$，$t$ 不能作为 $t’$ 的真起始段（proper initial segment），即不存在非空串 $\zeta$ 使得 $t\zeta=t’$．
(b) 对任意公式 $\varphi$ 与 $\varphi’$，$\varphi$ 不能作为 $\varphi’$ 的真起始段．
〔证明〕：
令字符串 $\zeta$ 具有性质 $P$，当且仅当对于任意的项 $t’$，$t’$ 均不能作为 $\zeta$ 的真起始段，$\zeta$ 也不能作为 $t’$ 的真起始段．
对项归纳：
$t=v$：令 $t’$ 为任意的项．$t’$ 若为 $t$ 的真起始段，则必然为空串 $\square$，而〔例 1’a〕已证明空串不能作为项．此外，不难对项归纳证明 $v$ 是唯一起始于 $v$ 的项．因此，$t$ 不能作为 $t’$ 的真起始段．
$t=c$：同理．
$t=ft_1\cdots t_n$，其中 $t_1,\,\cdots,\,t_n$ 具有性质 $P$：令 $t’$ 为任意指定的项．以反证法设存在 $\zeta\neq\square$ 使得 $t=t’\zeta$．$t’$ 起始于 $f$，因此 $t’$ 不为变元或常元，而只能由规则 (T3) 得到．因此必然有若干合适的项 $t_1’,\,\cdots,\,t_n’$ 使得 $t’$ 形如 $ft_1’\cdots t_n’$．由反证假设得
消去 $f$，得
因此 $t_1$ 是 $t_1’$ 的起始段，或反之．由归纳假设 $t_1$ 具有性质 $P$，因此 $t_1$ 不能为 $t_1’$ 的真起始段，反之亦然，于是 $t_1=t_1’$．消去上式的 $t_1$ 与 $t_1’$ 便得 $t_2\cdots t_n=t_2’\cdots t_n’\zeta$．同理重复以上步骤，便得到
与反证假设矛盾．因此不存在 $\zeta\neq\square$ 使得 $t=t’\zeta$．
由此证出 $t’$ 不能作为 $t$ 的真起始段．类似可证明 $t$ 不能作为 $t’$ 的真起始段．
(b) 的证明从略．
■
〔引理 1.e〕：
(a) 若 $t_1,\,\cdots,\,t_n$ 与 $t’_1,\,\cdots,\,t’_m$ 均为项，而 $t_1\cdots t_n=t’_1\cdots t’_m$，则 $m=n$，且对任意 $1\leq i\leq n$ 均有 $t_i=t’_i$．
(b) 若 $\varphi_1,\,\cdots,\,\varphi_n$ 与 $\varphi’_1,\,\cdots,\,\varphi’_m$ 均为公式，而 $\varphi_1\cdots\varphi_n=\varphi’_1\cdots\varphi’_m$ 则 $m=n$，且对任意 $1\leq i\leq n$ 均有 $\varphi_i=\varphi’_i$．
由〔引理 1.d〕不难证明．
〔定理 1.f〕项与公式的唯一分解性：
(a) 任一个项 $t$ 均符合以下情况之中唯一一种：
(1) $t$ 是变元； (2) $t$ 是常元；
(3) $t$ 具有 $ft_1\cdots t_n$，其中 $f$ 是 $n$ 元函数符号，而 $t_1,\,\cdots,\,t_n$ 是唯一确定的．
(b) 任一个公式 $\varphi$ 均符合以下情况之中唯一一种：
(1) $\varphi=t_1\equiv t_2$； (2) $\varphi=Rt_1\cdots t_n$； (3) $\varphi=\neg\psi$；
(4) $\varphi=(\psi\diamond\chi)$； (5) $\varphi=\forall x\psi$； (6) $\varphi=\exists x\psi$．
上述所有情况中，所有项 $t_1,\,t_2,\,\cdots,\,t_n$、$n$ 元关系符号 $R$、公式 $\psi,\,\chi$、变元 $x$ 均是唯一确定的．
由〔引理 1.d〕〔引理 1.e〕易证．
由唯一分解性，可以以归纳定义（inductive definition）的方式，定义关于项或公式的函数．以下给出相应的例子：
〔定义 1.4〕：
(a) 函数 $\mathrm{var}$（更准确来说，应写成 $\mathrm{var}_S$）给出每个 $S$–项中所含有的变元集合，可以归纳定义如下：
(b) 函数 $\mathrm{SF}$ 给出每个公式的子公式集合，可以归纳定义如下：
Variabiles Liberae & Sententiae 自由变元与语句
〔定义 1.5〕：
对公式归纳定义函数 $\mathrm{fr}$ 如下：
集合 $\mathrm{fr}(\varphi)$ 的元素称为公式 $\varphi$ 的自由变元（free variable）．不含自由变元的公式（即满足 $\mathrm{fr}(\varphi)=\varnothing$ 的公式 $\varphi$）称为语句（sentence）．
令符号 $L_n^S$ 表示 $S$–公式的集合中，自由变元只出现于 $v_0,\,\cdots,\,v_{n-1}$ 之中的公式所组成的子集，即
Annotationes 注释
(1). 有时也写作 $=$，但为了区分等于号的其他意义，这里写作 $\equiv$． ↩
(2). $ft_1\cdots t_n$ 按照通常的 $n$ 元函数符号记法写作 $f(t_1,\,\cdots,\,t_n)$，这里为了简化而不使用括号与逗号，而认为 $n$ 元函数符号 $f$ 后的 $n$ 个符号各为其参数．对于 $n$ 元关系符号 $R$ 则同理． ↩
(3). 按一般的函数符号记法为 $g(v_0,\,f(g(v_4,\,c)))$． ↩
(4). 符号 $\diamond$ 表示 $\land,\,\lor,\,\to,\,\leftrightarrow$ 之中任意一个，后文均依此． ↩