计算机科学逻辑/一阶逻辑

一阶逻辑

在命题逻辑中，我们考虑了关于原子对象的公式，这些对象只能是真或假。一阶逻辑是本章的主题，它建立在命题逻辑的基础上，并允许您查看公式中讨论的对象内部。我们可以通过将对象讨论为大于集合 $\{0,1\}$ 的集合的元素，并包括任意复杂的相互关系来提供这种更精细的粒度级别。

我们首先通过定义一阶 (FO) 逻辑的语法开始，然后赋予这些结构意义。

语法

一阶逻辑的讨论域是一阶结构或模型。一个一阶结构包含

关系，
函数，以及
常量（元数为 0 的函数）。

一阶逻辑的词汇是

一组具有关联元数的关系符号，以及
一组具有关联元数的函数符号。

以下是一些示例一阶逻辑词汇

图
- 关系集 = { $V$ : 一元， $E$ : 二元 }
- 函数集 = { ${\mathit {next}}$ : 一元 }
算术
- 关系集 = { $+$ : 三元， $\times$ : 三元， $\uparrow$ : 三元， $=$ : 二元， $<$ : 二元 }
- 函数集 = { ${\mathit {next}}$ : 一元， $0$ : 常量 }

这里，图是由一组顶点 $V$ 和一组边 $E$ 组成。对于算术集，请注意使用 $+$ 和 $\times$ 纯粹是语法上的，我们本可以使用“加”和“乘”符号来代替。我们还没有给这些符号赋予任何意义。

项表示一阶结构中的一个元素。项用于指代我们讨论域中的元素。以下是描述项是什么的规则

每个变量都是一个项，其中变量只是一个符号集合
每个常数都是一个项
如果 $t_{1},t_{2},\ldots ,t_{k}$ 是项，且 $f$ 是 $k$ 元函数，那么 $f(t_{1},t_{2},\ldots ,t_{k})$ 是一个项。

例如，如果 $f$ 是一个二元函数，而 $g$ 是一个三元函数，那么以下都是项： $x,a,f(x,y),g(x,f(x,y),a)$ .

原子公式是

R(t_{1},t_{2},\ldots ,t_{k})

,

其中 $R$ 是 $k$ 元关系，而 $t_{1},t_{2},\ldots ,t_{k}$ 是项。当将 $R$ 视为一个集合时，这只是另一种说法，即元组

(t_{1},t_{2},\ldots ,t_{k})\in R

.

一个特殊的“ $=$ ”关系表示“等于”，不能被解释为其他含义。例如， $t_{1}=t_{2}$ 代表

=(t_{1},t_{2})

.

一阶公式是由给定的一阶词汇表、变量和符号 $(,),\neg ,\vee ,\wedge ,\rightarrow ,\exists ,\forall$ 构成的表达式。一阶公式的集合是满足以下条件的最小集合。

原子公式是一阶公式
如果 $\phi$ 和 $\psi$ 是公式， $x$ 是一个变量，则以下也是公式

$(\phi \vee \psi )$
$(\phi \wedge \psi )$
$(\neg \phi )$
$(\phi \rightarrow \psi )$
$(\exists x\phi )$
$(\forall x\phi )$

语义

给定词汇表上的一个一阶结构包含以下内容：

一个域，它是一组元素（也称为宇宙）
一个映射，它将词汇表中的每个 $k$ 元关系符号与域上的 $k$ 元关系相关联，并将每个 $k$ 元函数符号与域上的 $k$ 元函数相关联。

这些组件赋予符号意义。

例子

关系集 = {

+

: 三元，

\times

: 三元，

\uparrow

: 三元，

=

: 二元，

<

: 二元 }

函数集 = {

next

: 一元，

0

: 常数 }

在这个词汇表上的一个一阶结构是

域：整数集
映射 : $+\rightarrow$ 加法， $\times \rightarrow$ 乘法， $\uparrow \rightarrow$ 幂运算， $<\rightarrow$ 排序， ${\mathit {next}}\rightarrow i+1$

在这个结构中，公式

\exists x\forall y\forall z[\times (y,z,x)\rightarrow ((y=1)\vee (z=1))]

表达了“存在质数”的命题（数字1也满足该命题）。

这里要注意 $\times (y,z,x)$ 等价于 $(x=y\times z)$ .

量词的作用域

在公式 $(\forall x\phi )$ 或 $(\exists x\phi )$ 中， $\phi$ 被称为变量 $x$ 的量化作用域。公式中变量的出现，如果在该变量的量化作用域内，则称该出现是约束的，否则称该出现是自由的。您可以将量词的用法视为变量声明。

句子是一个没有自由变量的公式（即所有变量都是约束的）。句子要么为真要么为假。

包含自由变量的公式可以被认为是描述自由变量的属性。例如， $\phi (x)$ 表示一个包含 $x$ 自由变量的公式，并描述了 $x$ 的属性。

如果一个句子 $\phi$ 在结构 $I$ 上评估为真，我们说 $I$ 满足 $\phi$ ，并将其记为 $I\models \phi$ 。

$I\models R(t_{1},t_{2},\ldots ,t_{k})$ 当且仅当 $(t_{1},t_{2},\ldots ,t_{k})\in I(R)$ ，其中 $I(R)$ 是 $R$ 在 $I$ 中的解释。
$I\models \phi \wedge \psi$ 当且仅当 $I\models \phi$ 且 $I\models \psi$ 。（对于 $\vee$ 类似）。
$I\models \neg \varphi$ 当且仅当 $I\not \models \varphi$ 。
$I\models \exists x\phi (x)$ 如果 $I\models \phi (x\leftarrow c)$ 对于某些 $c$ 在域中。
$I\models \forall x\phi (x)$ 如果 $I\models \phi (x\leftarrow c)$ 对于每个 $c$ 在域中。

注意: $\phi (x\leftarrow c)$ 表示用 $c$ 替换 $x$ 在 $\phi$ 中的所有自由出现的结果。替换将在本章后面进一步讨论。

公理化方法

公理是一组句子，旨在区分“期望”模型与其他模型。但通常，也存在“非期望”模型，称为非标准模型。

例如: 考虑词汇表 $({\mathit {next}},+,\times ,\uparrow ,0,=,<)$ ，其中符号具有通常的含义（由关于此词汇表的 FO 句子定义）。这组公理的标准解释（见本章末尾）是整数，但模 $p$ 的整数集也满足这些公理。通过将以下句子添加到公理中，可以排除这种可能性: $\forall x(x<{\mathit {next}}(x))$

问题: 所有非标准模型都可以通过公理化排除吗? 答案是否定的。考虑 [TODO: 导入图形] 中所示的模型，该模型的词汇表仅包含 $0,<,\sigma$ （上行中的所有元素都大于下行中的元素）。

没有一组一阶句子可以区分此模型与自然数。直观地，原因是，我们无法在一阶句子中任意“回溯”（向 $0$ ）。对于上面的完整词汇表，也可以获得类似的非标准模型。

评估 FO 句子

给定一阶结构 $I$ 和 FO 句子 $\phi$ ，我们能否判断 $I\models \phi$ ？

对于有限结构，这个问题是可判定的。例如，假设 $E$ 是一个表示图边界的二元关系，而给定句子是

\exists x_{1}\exists x_{2}\exists x_{3}(E(x_{1},x_{2})\wedge E(x_{2},x_{3})\wedge E(x_{3},x_{1})\wedge x_{1}\neq x_{2}\wedge x_{2}\neq x_{3}\wedge x_{3}\neq x_{1})

.

我们可以通过尝试 $x_{1},x_{2}$ 和 $x_{3}$ 的所有可能值来评估这个句子的真值。（朴素评估：“嵌套循环”。）这在域大小上是多项式时间，但在公式大小上是指数时间。

在无限域上，我们可能能够评估句子的真值，也可能不能。在词汇 $(N,0,\sigma ,<,+)$ 中，其中 $N$ 是自然数集，如果句子为真，则它是可判定的。（这被称为普雷斯伯格算术。）但是，如果我们包含乘法，则句子的真值将变得不可判定。

FO 的演绎系统

FO 句子的集合 $\Delta$ 是

可满足的，如果存在某个结构 $I$ 使得 $I\models \Delta$
不可满足的，如果它不可满足
有效的，如果对所有结构 $I$ ，都有 $I\models \Delta$

给定一组 FO 句子 $\Sigma$ 和一个句子 $\phi$

$\Sigma$ 蕴涵 $\phi$ （记为 $\Sigma \models \phi$ ），如果每个满足 $\Sigma$ 的结构也满足 $\phi$ 。
$\Sigma \models \phi$ 当且仅当 $\Sigma \cup \{\neg \phi \}$ 是不可满足的。
如果 $\Sigma$ 是有限的，那么， $\Sigma \models \phi$ 当且仅当 $\neg \Sigma \lor \phi$ 是有效的。
如果公式 $\phi$ 有自由变量 ${\vec {X}}=(x_{1},\ldots ,x_{k})$ ， $\phi$ 是有效的，当且仅当 $\forall {\vec {X}}\phi$ 是有效的。

有效性公理

有效性公理分为三类：

布尔有效性公理。这些公理从命题逻辑中继承而来。
等式公理。
量化公理。

布尔有效性

给定一个一阶逻辑公式 $\varphi$ ， $\varphi$ 的布尔形式是一个命题公式 $\psi$ ，使得 $\varphi$ 是通过将 $\psi$ 中的每个命题变量替换为 $\varphi$ 的子公式得到的。

$\varphi$ 的布尔形式集合用 $BF(\varphi )$ 表示。

例子

对于一阶逻辑公式 $\forall xP(x)\lor \neg \forall xP(x)$ ，布尔形式为 $p\lor \neg p$ 。
如果 $\varphi \equiv \forall xG(x,y)\land \exists xG(x,y)\land (G(z,x)\lor \forall xG(x,y))$ ，那么 $BF(\varphi )\equiv x_{1}\land x_{3}\land (x_{2}\lor x_{1})$ ，其中 $x_{1}=\forall xG(x,y),x_{2}=G(z,x),x_{3}=\exists xG(x,y)$ 。

断言: 如果 $\psi \in BF(\varphi )$ 并且 $\psi$ 是有效的，那么 $\varphi$ 是有效的。

等式公理

令 $t,t_{1},\ldots ,t_{k},t'_{1},\ldots ,t'_{k}$ 是项。以下是一阶逻辑的有效公式。

$t=t$
$(t_{1}=t'_{1}\land \cdots \land t_{k}=t'_{k})\rightarrow (f(t_{1},\ldots ,t_{k})=f(t'_{1},\ldots ,t'_{k}))$ , 其中 $f$ 是一个 $k$ 元函数。
$(t_{1}=t'_{1}\land \cdots \land t_{k}=t'_{k})\rightarrow (R(t_{1},\ldots ,t_{k})\rightarrow R(t'_{1},\ldots ,t'_{k}))$ , 其中 $R$ 是一个 $k$ 元关系。

替换

给定一个公式 $\varphi$ ，其中变量 $x$ 出现自由（表示为 $\varphi (x)$ ）和一个项 $t$ ，我们定义将 $t$ 代入 $x$ 的 $\varphi$ ，记为 $\varphi (x\leftarrow t)$ ，为将 $\varphi$ 中每个 $x$ 的自由出现用 $t$ 代替得到的结果公式，但必须满足约束条件： $t$ 不包含任何在 $\varphi$ 中被量化的变量 $y$ ，使得 $x$ 出现在 $y$ 量化范围内的自由位置。如果 $x$ 不在 $\varphi$ 中自由出现，那么 $\varphi (x\leftarrow t)$ 被定义为 $\varphi$ 。

例如：设 $\varphi$ 为

((x=1)\rightarrow \exists x(x=y))

,

那么

$\varphi (x\leftarrow (y+1))$ 是一个有效的替换
$\varphi (y\leftarrow (x+1))$ 不是一个有效的替换。

量化公理

$\forall x\varphi \rightarrow \varphi (x\leftarrow t)$ ，其中 $t$ 是一个项， $\varphi (x\leftarrow t)$ 是一个有效的替换
$(\forall x(\varphi \rightarrow \psi ))\rightarrow ((\forall x\varphi )\rightarrow (\forall x\psi ))$
$\varphi \rightarrow \forall x\varphi$
$\exists x\varphi \leftrightarrow \neg \forall x\neg \varphi$

总之，有效性的公理是 ${\mathbf {Ax} }$

布尔有效性公理。这些公理从命题逻辑中继承而来。
等式公理。
量化公理。

定义：一个证明是一个序列 $\phi _{1},\phi _{2},\ldots ,\phi _{k}$ 的 FO 语句，使得对于每个 $i\in \{1,\ldots ,k\}$ 或者 $\phi _{i}\in {\mathbf {Ax} }$ 或者 $\exists j,k<i$ 使得 $\phi _{j}\equiv \psi$ 以及 $\phi _{k}\equiv (\psi \rightarrow \phi _{i})$ .

符号: 如果存在使用 ${\mathbf {Ax} }$ 的 $\phi$ 的证明，我们用 $\vdash _{\mathbf {Ax} }\phi$ 来表示这个事实。

事实 (可靠性): 如果 $\vdash _{\mathbf {Ax} }\phi$ ，那么 $\phi$ 是有效的。

备注: 可以证明有效的公式集是递归可枚举的。

示例: 公式 $\forall x(\phi \land \psi )\rightarrow (\forall x\phi \land \forall x\psi )$ 的证明

\forall x(\phi \land \psi )

\forall x(\phi \land \psi )\rightarrow (\phi \land \psi )(x\leftarrow x)

\phi \land \psi

\phi

\forall x(\phi \land \psi )\rightarrow \phi

\forall x(\forall x(\phi \land \psi )\rightarrow \phi )

\forall x\forall x(\phi \land \psi )\rightarrow \forall x\phi

\forall x(\phi \land \psi )\rightarrow \forall x\phi

\forall x\phi

$\forall x\psi$ 的证明是对称的。

\forall x\phi \land \forall x\psi

\forall x(\phi \land \psi )\rightarrow (\forall x\phi \land \forall x\psi )

有用的等价关系

$\forall x(\phi \land \psi )\leftrightarrow (\forall x\phi )\land (\forall x\psi )$
$\forall x(\phi \lor \psi )\not \leftrightarrow (\forall x\phi )\lor (\forall x\psi )$ 例如 $\phi (x)\approx$ "x 是偶数" 以及 $\psi (x)\approx$ "x 是奇数"
$\forall x(\phi (x)\lor \neg \phi (x))\not \leftrightarrow (\forall x\phi (x)\lor \forall x\neg \phi (x))$
$\exists x(\phi \lor \psi )\leftrightarrow (\exists x\phi )\lor (\exists x\psi )$
$\neg \exists x\phi \leftrightarrow \forall x\neg \phi$
$\neg \forall x\phi \leftrightarrow \exists x\neg \phi$

前束范式

断言：每个 FO 语句都等价于一个形如 $Q_{1}x_{1}\cdots Q_{k}x_{k}\phi$ 的 FO 语句，其中 $Q_{i}\in \{\exists ,\forall \}$ 且 $\phi$ 是无量词的。

这是通过使用量词的分配律证明的。可能需要重命名变量，以避免歧义。虽然你总是可以将所有量词移动到左侧，但所得公式的大小实际上可能比原始公式大很多倍。

例子:

\phi \equiv \forall x(G(x,x)\land (\forall yG(x,y)\lor \exists y\neg G(y,y)))\land G(x,0)

\equiv (\forall x(G(x,x)\land (\forall yG(x,y)\lor \exists y\neg G(y,y))))\land G(w,0)

\equiv \forall x(G(x,x)\land (\forall yG(x,y)\lor \exists y\neg G(y,y))\land G(w,0))

\equiv \forall x(G(x,x)\land (\forall yG(x,y)\lor \exists z\neg G(z,z))\land G(w,0))

\equiv \forall x(G(x,x)\land \forall y(G(x,y)\lor \exists z\neg G(z,z))\land G(w,0))

\equiv \forall x\forall y(G(x,x)\land (G(x,y)\lor \exists z\neg G(z,z))\land G(w,0))

\equiv \forall x\forall y(G(x,x)\land \exists z(G(x,y)\lor \neg G(z,z))\land G(w,0))

\equiv \forall x\forall y\exists z(G(x,x)\land (G(x,y)\lor \neg G(z,z))\land G(w,0))

回顾公理方法

使用一个（可能是无限的，但递归的）公理集 $\Delta$ （一阶句子）尽可能详细地描述所需模型。

使用演绎证明事物。

符号: 我们说 $\phi$ 是 $\Delta$ 的有效推论（记为 $\Delta \models \phi$ ），如果每个满足 $\Delta$ 的模型也满足 $\phi$ 。

事实: $\Sigma \models \phi$ 当且仅当 $\Sigma \cup \{\neg \phi \}$ 不可满足。

旁注: 数论的非逻辑公理

以下十四个一阶公理描述了算术和数字的性质，即加法 ( $+$ )，乘法 ( $\times$ )，幂运算 ( $\uparrow$ ，相等 ( $=$ )，排序 ( $<$ )，后继函数 ( $\sigma$ ) 和余数 (mod)。这个例子展示了一阶语句的表达能力，最初人们希望它能为“唯一真正的数学”提供基础。