有限域下的谓词逻辑
在本章中, 我们介绍有限域下的谓词逻辑 (Propositional Logic of Finite Domains, PLFD) , 它可被用于描述那些状态可以通过指定变量的值而定义的状态转换系统的属性. 我们认知下的谓词逻辑 (Propositional Logic) 可被视为一种特殊的 PLFD: 在该系统中, 任何谓词变量的取值都是布尔值.
我们将首先解释 PLFD 的语法和语义. 在此之后, 我们会进一步地通过引入 PLFD 与谓词逻辑之间的模式转换 (Model-Preserving Translations), 从而使利用谓词逻辑解决 PLFD 问题成为可能. 最后, 我们为 PLFD 引入语义表系统 (Tableau System).
10.1 语法和语义
有限域下的谓词逻辑实际上是一类具有相同特征的逻辑系统的总和. 这一类逻辑系统都包含存储变量的有限集 $\mathscr{X}$ 和一个由 域 组成的有限集. 在其中, 我们称有限集 $\mathscr{X}$ 中的元素为 值, 每个值都和某个域相关联, 记为 $\text{dom}(x)$. 我们称, $\text{dom}(x)$ 为变量 $x$ 的定义域.
定义 10.1.1 (有限域下谓词逻辑中的公式)
我们使用下列的归纳法定义有限域下谓词逻辑中公式的概念:
- 若 $x$ 为变量, $v \in \text{dom}(x)$ 为 $x$ 的定义域中的一个值, 则 $x=v$ 为 公式 (原子公式), 或称为 原子.
- 使用原子公式, 利用逻辑联结词构造的复合公式也是 公式.
PLFD 语义的定义和谓词逻辑类似. 我们首先定义 “解释” 的概念, 再定义在某个解释中原子公式的含义. 我们下面解释 PLFD 的语义:
定义 10.1.2 (有限域下谓词逻辑的解释)
称对由一系列变量组成的结合 $X$ 的 解释 为一个从 $X$ 到一个集合的映射 $I$, 满足
\[\forall x, ~ I(x) \in \text{dom}(x).\]同时有:
- $I(x=v) = 1$ 当且仅当 $I(x)=v$.
- 若 $F$ 不为原子公式, 则 $I(F)$ 的定义和谓词逻辑中的定义一致.
此外, 有限域下谓词逻辑的 真性. 模型 (model), 重言性, 可满足性 和 等价性 都与谓词逻辑一致.
需要注意的是: PLFD 的语法和语义是 参数化 的. 也就是说, PLFD 的一些性质实际上可能受一些特定变量的定义域的影响. 如公式 door = open \/ door = closed 对任何满足 $\text{dom}(\text{door}) = {\text{open}, \text{closed}}$ 的逻辑均满足, 但若某个逻辑实例的 $\text{dom}(\text{door})$ 包含三个或以上元素时, 情况就不一样了.
10.2 模式转换
我们将在本节中讨论 PLFD 和谓词逻辑的转换问题, 并提供一种转换方法. 我们将看到, 谓词逻辑本质上是 PLFD 的一个实例.
10.2.1 谓词逻辑到 PLFD 的转换
考虑 PLFD 的一个实例, 在该实例中, 任何变量 $p_i$ 的定义域都是 ${0, 1}$, 也就是布尔值. 显然, 谓词逻辑和我们刚才定义的实例具有相同的解释: 这两个逻辑系统中的任何一个的任一解释本质上都是将变量映射到某个布尔值上. 在本章中, 我们给出的转换法将具有把任何谓词逻辑中的公式 $F$ 转换为 PLFD 中的公式 $F’$, 使得在谓词逻辑中 $I \vDash F$ 当且仅当在 PLFD 中 $I \vDash F’$.
谓词逻辑到 PLFD 的转换的定义如下: 对任意谓词逻辑下的公式 $F$, 公式 $\text{plfd}(F)$ 将通过从 $F$ 中将任何谓词原子 $p$ 替换为 PLFD 原子公式 $p=1$ 所得到.
定理 10.2.1
谓词公式 $F$ 和通过上述规则转换得到的公式 $\text{plfd}(F)$ 具有相同的模型.
10.2.2 PLFD 到谓词逻辑的转换
下面考虑从 PLFD 到谓词逻辑的转换.
对任意包含非布尔变量的 PLFD 而言, 我们是无法找到保持语义不变的转换方法将其转换为谓词逻辑的. 在这种情况下, 我们仍可构造出一个 保持 PLFD 和谓词逻辑的部分性质之间的映射, 我们也可以使用这样的映射寻找 PLFD 公式的模型, 检验其可满足性和其他的属性.
我们使用这样的思想构造保持性质的映射: 对 PLFD 中的原子公式, 我们可以引入 布尔变量 来将其表示, 如使用 $x_v$ 表示公式 $x=v$. 在对 PLFD 中的所有原子公式都这样替代后, 我们记这样得到的谓词公式为 $F’$. 一般地, 在执行完这样的转换后, 我们往往还需要附加一些限制条件以排除掉一些在 $F’$ 中合法, 但在 PLFD 中无效的模型.
定义 10.2.1 (域公理)
设 $x$ 为变量, 其定义域为 $\text{dom}(x) ={v_1, \cdots, v_n}$. 则 $x$ 的 域公理 为谓词公式:
\[(x_{v_1} \vee \cdots \vee x_{v_n}) \wedge \bigwedge_{i < j} (\neg x_{v_i} \wedge \neg x_{v_j}).\]
引理 10.2.1
记 $\text{dom}(x) = {v_1, \cdots, v_n}.$ 记 $F$ 为 $x$ 的域公理, $I$ 为定义在一系列布尔变量 $X = {x_{v_1}, \cdots, x_{v_n}}$ 上的解释. 则 $I \vDash F$ 当且仅当 $X$ 中 恰有一个 布尔变量在 $I$ 中是被满足的.
证明
显然 $x_{v_1} \vee \cdots \vee x_{v_n}$ 表示的是 “解释 $I$ 至少要满足 $X$ 中的一个元素”, 而 $\neg x_{v_i} \wedge \neg x_{v_j}$ 表示的是 “解释最多满足变量 $x_{v_i}, x_{v_j}$ 中的一个”. 因此结合可知, 域公理的 模型 恰为: 恰好满足 $X$ 中某一个变量的那些解释 (Intepretation). $\blacksquare$
10.3 PLFD 的语义表系统
在本节中, 我们通过对谓词逻辑的 语义表 构造规则进行扩展, 引入 PLFD 的语义表系统.
考虑变量 $x$ 与集合 $D$, $D \in \text{dom}(x)$, 认定 $x \in D$ 为具有下列语义的原子公式:
对某个解释 $I$, 我们有 $I \vDash x \in D$ 当且仅当 $I(x) \in D$, 显然 任何形如 $x=v$ 的公式都和公式 $x \in {v}$ 等价, 且任何形如 $x \in {v_1, \cdots, v_n}$ 的公式都等价于 $(x=v_1) \vee (x=v_2) \vee \cdots (x=v_n)$.
PLFD 的语义表系统基本上使用与谓词逻辑中的语义表系统相同的分支扩展规则, 但是在此基础上我们还要引入两条新的规则;
注意我们可以对有符号公式进行如下的简化;
- $(x \in D)=1$ 的简化表述是 $x \in D$.
- $(x \in D)=0$ 的简化表述是 $x \notin D$.
此外, 需要注意的是, 第二条新规则要求公式 $x \in D_1, x \in D_2$ 位于相同的分支上 $(D_1, D_2 \in \text{dom}(x))$.
我们同时称语义表中的某个分支为 闭的, 若它包含下列的有符号公式的至少一种: $\top = 0, ~ \perp = 1, ~ x \in {}$.
定理 10.3.1 (正确性和完备性)
令 $T$ 为由某个有符号公式 $\gamma$ 表示的已终止的决策所得到的表, 则公式 $\gamma$ 为可满足的, 当且仅当 $T$ 中所有分支都是闭的.
