AIL C4 一阶逻辑

在一阶逻辑的框架下研究知识的表示和推理:

• 谓词和量词的概念
• 一阶语言与对一阶语言的解释
• 一阶语义蕴涵，形式推演，算法和计算复杂性等。

谓语和量词

• 论域 ： 所有被讨论对象的集合。
• 个体：域中的元素，即被讨论的对象。
  • 常元：用于表示确定对象的符号。
  • 变元：用于表示给定论域上的任意一个对象的符号。
• 函词：给定一个论域，从一组个体到一个个体的映射关系。
• 项：
  1. 个体常元和个体变元是项。
  2. 如果$t_1,t_2,\cdots,t_n$是项，$f$ 是 $n$ 元函词， 那么 $f(t_1,\cdots , t_n)$ 也是项。
  3. 有限次使用(1)(2)生成的是项。
• 谓词：描述个体之间的关系。谓词包含着可放置讨论对象的位置，即 空位。 空位的数量称为谓词的元数。用一元谓词表示的关系称为个体的性质。
• 量词：
  • 全称量词：描述某个变元的取值范围涵盖一整个论域，记作 $\forall x$，读作“ 对于所有的 $x$”；
  • 存在量词：描述在给定论域中存在某个个体，记作 $∃x$，读作“ 存在 $x$”。

谓词和量词是一阶逻辑的主要研究对象。

• 单称命题
• 全称命题
• 特称命题

一阶语言 $\cal{L}$

一阶语言符号

组成

• 个体常元，正体小写拉丁文字母。

  $$\rm a,b,c$$

• 个体变元，正体小写拉丁文字母。

  $$\rm x,y,z$$

  • 个体自由变元: 变元不受到量词的约束。
  • 个体约束变元: 变元受到量词的约束。

• 函数符号：与自然语言语句中的函词对应，正体小写拉丁文字母。

  $$\rm f,g,h$$

  • 函数符号和函数

    函数符号是符号，函数是对函数符号的一种解释。通常对于函数符号$\rm f$，用$f$来表示解释的函数。

  • 函数符号的元数

    任何函数符号 $\rm f$ 有确定的元数$m ≥ 1$，称元数为$m$的$\rm f$ 为$m$元函数符号。特别地，当$m=0$，我们认为$0$元函数是一种个体。

• 关系符号：与自然语言语句中的谓词对应，正体大写拉丁文字母

  $$\rm F,G,H$$

  函数符号的元数

  任何关系符号$\rm F$ 有确定的元数$n ≥ 1$，称元数为$n$的$\rm F$ 为$n$元关系符号。特别地，当$n=0$，我们认为$0$元关系符号是一种命题。

• 量词符号：$\forall,\exist$

• 联结符号：与命题逻辑的相同。

• 标点符号： 左括号$($、右括号$)$和逗号$,$ 。

项，Term（符号）

1. 变元和常元是项。
2. 如果$t_1,t_2,\cdots,t_n$是项，$\rm f$ 是$m$元函数，则 $\rm f(t_1,t_2,\cdots,t_n)$ 是项。
3. 只有有限次使用 (1)(2) 条款生成的符号串才是项。

BNF 形式：

$$\rm t ::= x|a|f(t,t,\cdots,t)$$

基项：不含自由变元的项。表示的是论域中确定的个体。

公式

1. $\rm F(t_1, \cdots , t_n)$是公式，称为原子公式。其中$\rm F$是$n$元关系符号，$\rm t_1, \cdots , t_n$是项。
2. 如果 $\rm t_1$ 和 $t_2$ 是项，那么 $(t_1 \equiv t_2)$ 是原子公式。
3. 如果 $\phi$ 和 $\psi$ 是公式，且 $x$ 是出现于 $\phi$ 中的自由变元(可被记为$\phi(x)$)，则 $(\lnot\phi),(\phi \wedge \psi),(\phi \vee \psi),(\phi \rightarrow\psi),(\phi \leftrightarrow\psi),(\forall x\phi),(\exist x\phi)$ 是公式。
4. 只有有限次使用 (1)(2)(3) 条款生成的符号串才是公式。

• 子公式：在一个公式中，可以包含公式，则称后者为前者的子公式。
• 变元$x$ 在公式 $\phi$ 中约束出现：如果 $\phi$ 包含一个子公式 $\psi$，$x$ 出现于 $\psi$ 中，且 $\psi$ 是以$\forall x$ 或 $\exist x$ 为起始的字符串；
• 变元 $x$ 在公式 $\phi$ 中自由出现：如果$x$不是约束出现。
• 句子：任何变元都不是自由出现的公式。

谓词的顺序对语义的影响

关系符号 $\rm F(x) : x$是安全事故，$\rm G(x,y):x$有原因$\rm y$。

1. 任何安全事故都有原因。

   $$\forall \rm F(x) \rightarrow \exist y,G(x,y)$$

2. 任何安全事故都有共同的原因。

   $$\exist\rm y,\forall x,F(x) \rightarrow G(x,y)$$

代换

可代换： 称项$\rm t$ 对$\phi$ 中自由变元$\rm x$是可代换的，若$\phi$中 $\rm x$的任何自由出现都不在$\rm \forall y,\exist y$的辖域内。(即$\rm x$是自由的，而不被约束)

代换 $\theta$ 是一个有限的对子集合 $\{x_1/t_1, \cdots , x_n/t_n\}$，其中 $x_i$ 是变元，$t_i$ 是项，$t_i$对$x_i$是可代换的。

给定公式$\phi$，代换$\theta$ ，则 $\phi\theta$ 是一个公式，在该公式中所有$x_i$ 的自由出现都被替换为$t_i$。 也把 $\phi\{x/t\}$ 写作 $\phi^x_t$。

一阶语言语义

解释

关系符号、函数符号、 变元符号、个体符号的含义与论域有关。

给定论域$D$，解释是一个映射：

• 把个体符号映射为$D$中的对象
• 把 $n$ 元函数符号映射为从$D^n$ 到$D$ 的函数
• 把 $n$ 元关系符号映射为$D$ 上的 $n$ 元关系。

另一方面，对于每个自由变元，可以把论域中的对象指派给它,指派也是一个映射。解释和指派统称作赋值，记作 $v$。

即有：

• 对于个体常元 $\rm a$, 把它解释为的$D$中的个体，记作$v(\rm a) \in D$。
• 对于 $n$ 元函数符号 $\rm f$, 把它解释为从$D^n$ 到$D$ 的函数，记作 $v(\rm f) : D^n \mapsto D$。
• 对于 $n$ 元谓词符号 $\rm F$, 把它解释为$D$ 上的 $n$ 元关系，记作 $v(\rm F) \sube D^n$。
• 对于自由变元 $\rm x$，给它指派$D$ 中的个体，记作 $v(\rm x) \in D$。

通常把 $v({\rm a}), v({\rm f}), v({\rm F}), v({\rm x})$ 分别记作 ${\rm a}^v,{\rm f}^v,{\rm F}^v,{\rm x}^v$。

项的值

一阶逻辑语言的项在以$D$为论域的赋值 $v$ 之下的值递归地定义如下：

1. ${\rm a}^v, {\rm x}^v \in D$.
2. ${\rm f(t_1,\cdots, t_n)}^v = {\rm f}^v({\rm t}^v_1,\cdots, {\rm t}^v_n) \in D$

公式的真假

类似公式的定义，一阶公式的真假值可递归地定义如下：

• ${\rm F(t_1,\cdots , t_n)}^v = \begin{cases}1,\ ({\rm t}_1^v,\cdots , {\rm t}_n^v)\in{\rm F}^v\\ 0,\ otherwise\end{cases}$

• $({\rm t_1 \equiv t_2)}^v = \begin{cases}1,\ {\rm t}_1^v = {\rm t}_2^v = a \in{\rm F}^v\\ 0,\ otherwise\end{cases}$

• $(\lnot \phi)^v = \begin{cases}1,\ \phi^v = 0\\ 0,\ otherwise\end{cases}$

• $(\psi\wedge \phi)^v = \begin{cases}1,\ \phi^v = \psi^v = 1 \\ 0,\ otherwise\end{cases}$

• $(\psi \vee \phi)^v = \begin{cases}0,\ \phi^v = \psi^v = 0\\ 1,\ otherwise\end{cases}$

• $(\phi \rightarrow\psi)^v = \begin{cases}1,\ \phi^v = 0\ or\ \psi^v = 1\\ 0,\ otherwise\end{cases}$

• $(\phi \leftrightarrow\psi)^v = \begin{cases}1,\ \phi^v = \psi^v\\ 0,\ otherwise\end{cases}$

• $(\forall {\rm x\phi})^v = \begin{cases}1,\ \forall a\in D,\phi^{v(x/a) }= 1\\ 0,\ otherwise\end{cases}$

• $(\exist {\rm x\phi})^v = \begin{cases}1,\ \exist a\in D,\phi^{v(x/a) }= 1\\ 0,\ otherwise\end{cases}$

其中，$v({\rm x} / {\it a})$ 表示一个以 $D$ 为论域的赋值，除了 $\rm x^{\it v(\rm x/\it a)} = \it a \in D$ 之外，和 $v$ 完全相同（即把$\rm x$固定地指派为$a$）。

请注意 符号 和 个体 之间的区别。注意$\phi$可为任意复杂的公式。

e.g 设$D = \{s_1,s_2,s_3,b_1,b_2,b_3\}$，赋值$v$:

• $F^v = \{s_1, s_2, s_3\}$
• $G^v = \{b_1, b_2, b_3\}$
• $H^v = \{(s_1, b_1), (s1, b_2), (s_2, b_1), (s_3, b_3)\}$

则对$\forall x\exist y(F(x)\rightarrow G(y)\wedge H(x,y))^v$的解释为：

$$\begin{align*}&\forall a \in D,\exist b \in D,(F(x)\rightarrow G(y)\wedge H(x,y))^{v(x/a,y/b)}\\\models\!|& \forall a \in D,\exist b \in D,(F^v(a)\rightarrow G^v(b)\wedge H^v(a,b)) = 1\\\end{align*}$$

逻辑推论

逻辑推论

给定一组一阶公式集合$\Phi$，公式$\phi$。则逻辑推论$\Phi \models \phi$成立，当且仅当对于非空论域$D$ 下的 任意 赋值 $v$，如果$\Phi^v = 1$ 则 $\phi^v = 1$。

则逻辑推论$\Phi \models \phi$不成立，也记作$\Phi \not \models \phi$，当且仅当对于非空论域$D$ 下的 存在 赋值 $v$，如果$\Phi^v = 1$ 且 $\phi^v = 0$。

可满足性和有效性

设 $\psi$是一个一阶公式。

• $\psi$是有效的，即 $\models \psi$，当且仅当 对于任何 论域$D$下任何赋值$v$，$\psi^v = 1$。
• $\psi$是可满足的，当且仅当 存在某个论域$D$ 下的某个赋值 $v$ 使得 $\psi^v = 1$。

语义等价

给定命题公式$\phi,\psi$，$\phi,\psi$语义等价 当且仅当

$$\phi \models \psi \wedge \psi \models \phi$$

记作$\phi |\!\!\!=\!\!\!| \psi$ 。

一阶逻辑中常见的语义等价关系：

• $\lnot \forall x\phi \models\!\!\!|\exist x\lnot\phi$
• $\lnot \exist x\phi \models\!\!\!|\forall x\lnot\phi$

一下均假设 $x$ 不在 $\phi$ 中出现：

• $\forall y\phi \models\!\!\!| \forall x\phi^y_x$
• $\exist y\phi \models\!\!\!| \exist x\phi^y_x$
• $\phi \wedge \forall x \psi \models\!\!\!| \forall x(\phi \wedge \psi)$
• $\phi \wedge \exist x \psi \models\!\!\!| \exist x(\phi \wedge \psi)$
• $\phi \vee \forall x \psi \models\!\!\!| \forall x(\phi \vee \psi)$
• $\phi \vee \exist x \psi \models\!\!\!| \exist x(\phi \vee \psi)$

前束范式

称一阶逻辑公式 $\phi$ 为前束范式，当且仅当它有如下的形式：

$$Q_1x_1\cdots Q_nx_n\ \phi'$$

其中,

• $Q_1\cdots Q_n$是量词$\forall$或 $\exist$;
• $x_1,\cdots x_n$是变元；
• $\phi'$ 是不含量词的公式。

称$Q_1x_1\cdots Q_nx_n$为前束词，$\phi'$为母式。前束范式的母式可以进一步变换为合取范式或析取范式。

消解原理

一阶消解推演规则

当对包含自由变元的子句进行消解时，如果这些子句都是全称量化的，则可以去掉量词。

不含存在量词的前束范式

子句形式与命题逻辑的相同，但原子公式是 $F(t_1,\cdots , t_n)$；对子句的理解与之前一样，但变元被理解成全称量化。

给定两个子句 $c_1 ∪\{L_1\}$ 和 $c_2\cup\left\{\overline{L_2}\right\}$，如果它们没有公共变元，且存在一个代换 $θ$，使得 $L_1θ = L_2θ$，那么可以推出子句 $(c_1 ∪ c_2)θ$。这时我们说 $θ$ 是 $L_1$ 和 $L_2$ 的合一。

• $\Phi \vdash_{res} \bot$ 当且仅当 $\Phi \models_{res}\bot$ .

含存在量词的前束范式:斯科伦化

对于包含存在量词的公式，可把该存在量词所管辖的变元变成确定的个体，表示该确定个体的项被称为斯科伦常元；表示受限制的该确定个体的函词被称为斯科伦函词。

斯科伦化，即把 $\rm \forall x_1\forall x_2\cdots\forall x_n\exist y\phi$ 变换为$\rm \forall x_1\forall x_2\cdots\forall x_n \phi^y_{ f(x_1,x_2,\cdots,x_n)}$。

如果$\phi$是原有公式，$\phi$′ 是包含斯科伦化的子句，那么$\phi$在逻辑上不等值于$\phi$′。例如，$\exist xF(x)$ 在逻辑上不等值于 $F(a)$。不过，$\phi$ 是可满足的，当且仅当 $\phi$′ 是可满足的。这也是消解所真正需要的。

LEMMA 1

• $\rm \exist x\phi$ 是可满足的，当且仅当 $\rm \phi^x_a$是可满足的；
• $\rm \forall x_1\forall x_2\cdots\forall x_n\exist y\phi$是可满足的，当且仅当$\rm \forall x_1\forall x_2\cdots\forall x_n \phi^y_{f(x_1,x_2,\cdots,x_n)}$ 是可满足的。

其中，$\rm a$ 是 $\phi$中未出现过的新常元，$\rm f$ 是 $\phi$中未出现的新 $n$ 元函词，即前述斯科伦常元和斯科伦函词。

PROOF

给定论域$D$。

1. $\rm \exist x\phi$ 是可满足的,当且仅当存在某个赋值$v$，$\exist b \in D,\phi^{v(\rm x/\it b)} = 1$。将斯科伦常元 $\rm a$ 指派为 $\rm a^{\it v} = \it b$，则$\rm (\phi^x_a)^{\it v} = 1$。
2. • 考虑$n = 1$的情况。设$v$是$D$上的一个赋值使得$(\forall x\exist y \phi)^v = 1$，即$\forall a \in D,(\exist y\phi)^{v(x/a)} = 1$，即$\forall a \in D,\exist b \in D, \phi^{v(x/a,y/b)} = 1$。 现作$D$上函数$f$，使得对于每一个$a \in D$，指定$f(a)$为满足 $\phi^{v(x/a,y/b)} = 1$的$b$中的一个。
     考虑赋值$v'$，使得在除$\rm f$以外的其他符号以外均与$v$相同，${\rm f}^{v'} = f$。则对于赋值$v',\forall a \in D,\phi^{v'(x/a,y/f(a))} = 1$，即说$\forall x\phi^y_{\rm f(x)}$ 可满足。
     反之，若$\forall x\phi^y_{\rm f(x)}$ 可满足，即$\exist v: \forall a \in D,(\phi^y_{\rm f(x)})^{v(a/x)} = 1$，即$\phi^{v(a/x,y/ f(a))} = 1$，其中$f = {\rm f}^v$ 是$D$上的函数。换言之，对于每一个$a \in D$，$\exist b = f(a) \in D,\phi^{v(x/a,y/b)} = 1$，即$(\exist y\phi)^{v(x/a)} = 1$，也就是说$\rm \forall x\exist y\phi$是可满足的。
   • 假设 $n = 2,3,\cdots,k$时命题均成立。则$n = k + 1$时，$\rm \forall x_1\forall x_2\cdots\forall x_{k+1}\exist y\phi$ 可满足，即$\exist v:\forall a \in D,(\forall x_2\cdots\forall x_{k+1}\exist y\phi)^{v(a/x_1)} = 1$。由假设可知，

赫布兰德定理

用消解原理不一定都有易解的算法。在一阶逻辑的情况下，可能存在无限循环的情况。

赫布兰德域

给定子句集合$S$，$S$的赫布兰德域（H-域）是所有基项的集合。集合$H$称为子句集$S$的$H-$域，如果

$$H = \cup_{i = 0}^{\infty}H_i$$

其中，$H_i$ 递归确定如下：

• $H_0 =\begin{cases} \{a\},\quad there\ doesn't\ exist\ constant.\\\{c|c\ exists\ in\ S\},\quad otherwise\end{cases}$
• $H_{i+1} = H_i\cup\{f(t_1,t_2,\cdots,t_n)|t_1,\cdots,t_n \in H_i,f\ exists\ in\ S\}$

赫布兰德基底

子句集 $S$ 的赫布兰德基底 (H-基底），如果该集合为所有形如 $c\theta$ 的基原子公式的集合，其中 $c \in S$，$\theta$ 给 $c$ 中的变元指派 H-域中的元素。

赫布兰德定理

$S$ 是可满足的当且仅当$S$的 H-基底是可满足的。

• H-基底没有变元，故尽管 H-基底通常是无穷的，但其本质上是命题公式集合。
• 当$S$中没有函数符号而只有有穷的常元时，它的H-域是有穷的，此时其H-基地也是有穷的。
• 用 H-基底进行推理时，不必使用合一，因为并不存在变元。因此，总是存在可靠的和完备的推理过程。