命题逻辑

命题与真值

命题: 能判断真假的陈述句。这种陈述句的判断只有两种可能：一种是正确的判断，一种是错误的判断。称判断为正确的命题的真值为真，称判断为错误的命题的真值为假。

因此又可称命题是具有唯一真值的陈述句或判断结果唯一的陈述句

📝 备注

感叹句、祈使句、疑问句都不是命题

陈述句中的悖论以及判断结果不唯一确定的也不是命题

命题符号

用小写英文字母 $p, q, r, \cdots, p_i, q_i, r_i$ $(i \geqslant 1)$ 表示简单命题，将表示命题的符号放在该命题的前面，称为命题符号化。其中“1”表示真，用“0”表示假

对简单命题而言，它的真值是确定的，因而又称为命题常项或命题常元。

例如，

• 命题 $p$：$\sqrt{2}$ 是有理数，则 $p$ 的真值为 0；
• 命题 $q$：$2 + 5 = 7$，则 $q$ 的真值为 1。

演绎系统

演绎系统提供了一种证明 $\Sigma \vDash \psi$ 的方法。

每个推理规则遵循如下的格式：

📝 备注

其中 $\Sigma$ 是一组公式的集合，$\varphi$ 表示一个公式。

$\Sigma \vDash \varphi$ 表示对于任意解释（赋值），如果它使 $\Sigma$ 中所有公式都为真，那么它也必然使 $\varphi$ 为真。

演绎系统由以下有限的推理规则集组成：

1. 单调和参考规则

2. 属于规则

3. 传递规则

4. 取反规则

5. 合取规则

6. 析取规则

7. 蕴含规则

8. 等价规则

一阶谓词逻辑

项（Terms）是可以通过有限次应用以下规则获得的表达式：

1. 变量和常量符号是项
2. 如果 $t_1, t_2 \cdots, t_m$ 是项，$f$ 是 $m$ 元函数符号 $(m \geqslant 0)$，则 $f(t_1, \cdots, t_m)$ 也是一个项

一阶公式（简称为公式）是通过有限次应用以下规则得到的表达式：

1. 如果 $t_1, t_2, \cdots, t_m$ 是项，$P$ 是 $m$ 元谓词符号，则 $P(t_1, t_2, \cdots, t_m)$ 和 $(t_1 = t_2)$ 是公式。这样的公式被称为原子公式。
2. 如果 $\varphi$ 和 $\psi$ 是公式，那么 $(\lnot \varphi)$，$(\varphi \land \psi)$，$(\varphi \lor \psi)$，$(\varphi \Rightarrow \psi)$，$(\varphi \Leftrightarrow \psi)$ 都是公式。
3. 如果 $\varphi$ 是一个公式，$x$ 是一个变量，$S$ 是一元谓词符号，那么 $\forall x:S \cdot \varphi$ 和 $\exist x:S \cdot \varphi$ 均是公式。在这两个公式中，$\varphi$ 分别被称为量词 $\forall x:S$ 和 $\exist x:S$ 的作用域。

逻辑推理

假设 $\Sigma = \{\varphi_1, \varphi_2, \cdots, \varphi_n\}$，$\varphi_1, \varphi_2, \cdots, \varphi_n$ 和 $\psi$ 是句子。如果

成立，则记作

（或 $\varphi_1, \varphi_2, \cdots, \varphi_n \vDash \psi$）。在这种情况下，我们说 $\psi$ 可以从 $\Sigma$ 导出。

当 $\varphi \vDash \psi$ 且 $\psi \vDash \varphi$ 时，则称 $\varphi$ 与 $\psi$ 等价，记作 $\varphi \equiv \psi$

以下是对这段描述的形式化定义：

一个推理结构包含以下要素：

1. 一个非空集 $A$，称为 $A$ 的论域；
2. 每个 $m$ 元谓词符号 $P$ 在 $A$ 上的关系 $P^A$；
3. 每个 $m$ 元函数符号 $f$ 在 $A$ 上的函数 $f^A$；
4. 每个常数符号 $c$ 的元素 $c^A \in A$。

记 $A$ 为一个推理结构，对 $A$ 的赋值操作 $v$ 是一个函数，它将每个变量 $x$ 映射到 $A$ 论域中的一个元素 $x^v$。

记 $A$ 为一个推理结构，$v$ 为 $A$ 上的一个赋值操作，$t$ 为一个项，则有

1. 若 $t$ 为一个常量 $c$，则 $t^v = c^A$
2. 若 $t$ 为一个变量 $x$，则 $t^v = x^v$
3. 若 $t = f(t_1, t_2, \cdots, t_m)$，则 $t^v = f^A(t_1^v, t_2^v, \cdots, t_n^v)$

给定一个推理结构 $A$，$A$ 上的一个赋值操作 $v$，变量 $x$ 和元素 $\alpha \in A$，令 $v[\alpha / x]$ 表示满足下列关系的变量：

1. $x^{v[\alpha / x]} = \alpha$
2. 对任意的 $y \ne x$，有 $y^{v[\alpha / x]} = y^v$

在 $A, v \vDash \varphi$ 中，如果 $\varphi$ 是一个语句，则可以省略 $v$，只需写 $A \vDash \varphi$。

如果 $A \vDash \varphi$，那么我们说 $A$ 满足 $\varphi$，或者等价地说，$A$ 是 $\varphi$ 的模型。

设 $\Sigma$ 为一组句子。如果对于所有 $\varphi \in \Sigma$，都有 $A \vDash \varphi$，我们说 $A$ 是 $\Sigma$的模型。

由此，我们可以得出逻辑推论的定义：

记 $\Sigma$ 为一组公式，$\psi$ 为一个公式。如果对于 $A$ 上的所有赋值 $v$，都有

$$(\forall \varphi \in \Sigma:A, v \vDash \varphi) \Rightarrow A,v \vDash \varphi$$

那么我们说 $\Sigma$ 在逻辑上意味着 $\varphi$，写为 $\Sigma \vDash \varphi$，$\varphi$ 被称为 $\Sigma$ 的逻辑蕴含

一般地，我们有如下的表达：

含有量词的演绎系统

1. 全称量词

   $$\frac{\Sigma \vDash \forall x:S \cdot \varphi}{\Sigma \vDash t \in S \Rightarrow \varphi[t/x]} \quad [\forall-]$$
   $$\frac{\Sigma \vDash x \in S \Rightarrow \varphi}{\Sigma \vDash \forall x:S \cdot \varphi} \quad [\forall+]$$

2. 存在量词

   $$\frac{\Sigma, x \in S, \varphi \vDash \psi}{\Sigma, \exist x:S \cdot \varphi \vDash \psi} \quad [\exist-]$$
   $$\frac{\Sigma \vDash t \in S \land \varphi(t)}{\Sigma \vDash \exist x:S \cdot \varphi(x)} \quad [\exist+]$$

3. 相等

   $$\frac{\Sigma \vDash \varphi(t) \quad \Sigma \vDash t = t'}{\Sigma \vDash \varphi(t')} \quad [=-]$$
   $$\frac{}{\vDash x=x} \quad [=+]$$

程序正确性的证明

程序测试只能证明程序有错，不能说明程序正确。

― Edsger Dijkstra

正确性证明是论证程序达到预期⽬的的⼀般性陈述，⽽该论证不与程序输⼊数据的特定值有关，但能够代表穷举性测试。

三种程序正确性证明的技术

1. 以指称语义学为基础的描述⽅法，已被VDM开发计划中采⽤
2. 以代数语义学为基础的研究程序的终⽌性、⼀致性和等价性的证明⽅法
3. 以公理语义学为基础的正确性验证技术，理论上发展的最完善。包括Floyd的归纳断言法、Hoare的公理化方法、E.W.dijstra的最弱前置谓词法

程序正确性的概念

终止与部分正确

定义1：如果对于每⼀个使得 $P(\overline{a})$ 为真的输⼊ $\overline{a}$，程序 $S$ 计算都终止，称程序 $S$ 对 $P$ 是终止的。

定义2：对于满足 $P(\overline{a})$ 为真，且能够使程序 $S$ 计算终止的每个 $\overline{a}$，如果 $Q(\overline{a}, P(\overline{a}))$ 为真，则称程序 $S$ 对于 $P$ 和 $Q$ 是部分正确的。记为 $[P] S [Q]$。

定义3：对于满足 $P(\overline{a})$ 为真的每个 $\overline{a}$，如果程序 $S$ 能够计算终止，且 $Q(\overline{a}, P(\overline{a}))$ 为真，则称程序 $S$ 对于 $P$ 和 $Q$ 是完全正确的。记为 $\{P\}S\{Q\}$

中间断言

定义1：在程序任意一个中间点 $i$ 附上谓词 $p_i(\overline{x}, \overline{y})$。如果每当执行到达 $i$ 时，$p_i(\overline{x}, \overline{y})$ 对于该点的当前值必为真，则 $p_i(\overline{x}, \overline{y})$ 称为 $i$ 上的中间断言。

定义2：对于循环路径上的断言，因为每次循环执行到达该点时该断言必为真，所以该断言又称为循环不变式，简称不变式。

不变式断言法

步骤：

1. 建立断言：选取断点，建立断言
2. 建立检验条件
3. 验证检验条件

例如，设 $x_1$，$x_2$ 是正整数，求它们的最大公约数 $z = \gcd(x_1,x_2)$。该程序的流程图如下：

建立断言

建立输⼊断言和输出断言，

若有循环，在循环通路中选取⼀个断点来“分割”循环，并在此建立一个适当的断言。

对于求最大公约数的例子，则有：

建立检验条件

程序的执行可以分解为几条有限的通路，对每一条通路建立一个检验条件（程序运行时要想通过通路应当满足的条件）。

若将每一条通路看作一段程序，它的输入和输出断言分别为 $P_i(\overline{x}, \overline{y})$，$Q_i(\overline{x}, \overline{y})$，通过此通路的条件为 $R_i(\overline{x}, \overline{y})$，通过此路后 $y$ 的值变为 $r_i(\overline{x}, \overline{y})$，则相应的检验条件为

对于求最大公约数的例子，则有4条通路：

• $a_1: A \rightarrow B$，
  • $R_1(x,y) = \text{True}$
  • $r_1(x,y) = (x_1, x_2)$
  • 检验条件：$P(x) \land R_1(x,y) \Rightarrow p(x, r_1(x,y))$
• $a_2: B \rightarrow D \rightarrow B$
  • $R_2(x,y) = (y_1 \ne y_2) \land (y_1 > y_2)$
  • $r_2(x,y) = (y_1 - y_2, y_2)$
  • 检验条件：$p(x,y) \land R_2(x,y) \Rightarrow p(x, r_2(x,y))$
• $a_3: B \rightarrow E \rightarrow B$
  • $R_3(x,y) = (y_1 \ne y_2) \land (y_1 \leqslant y_2)$
  • $r_3(x,y) = (y_1, y_2-y_1)$
  • 检验条件：$p(x,y) \land R_3(x,y) \Rightarrow p(x, r_3(x,y))$
• $a_4: B \rightarrow G \rightarrow C$
  • $R_4(x,y) = (y_1 = y_2)$
  • $r_4(x,z) = y_1$
  • 检验条件：$p(x,y) \land R_4(x,y) \Rightarrow Q(x, r_4(x,z))$

验证检验条件

验证第2步中得到的所有的检验条件，如果每一通路的检验条件均为真，则该程序是部分正确的。

对于求最大公约数的例子，将上述的4个检验条件展开，证明它们为真。

良序集法

良序集的概念

设有一个非空集合 $W$ 和一个定义在 $W$ 上的二元关系 $\preccurlyeq$，满足以下性质：

1. 传递性：$\forall a, b, c \in W$，如果 $a \preccurlyeq b$，$b \preccurlyeq c$，那么 $a \preccurlyeq c$
2. 反对称性：$\forall a, b \in W$，如果 $a \preccurlyeq b$，则一定不存在 $b \preccurlyeq a$
3. 反自反性：$\forall a \in W$，一定不存在 $a \preccurlyeq a$

则称 $W$ 是具有关系 $\preccurlyeq$ 的偏序集，记作 $(W, \preccurlyeq)$

设 $(W, \preccurlyeq)$ 是一个偏序集，如果不存在由 $W$ 中的元素构成的无限递减序列 $a_0 \succcurlyeq a_1 \succcurlyeq a_2 \succcurlyeq \cdots$，则称 $(W, \preccurlyeq)$ 是一个良序集。

证明程序终止性

设程序 $S$ 的输入断言为 $P(x)$

1. 选择一个割点集合，去截断程序的各个循环部分，并在每一个截点 $i$ 处建立一个中间断言 $q_i(x,y)$。这样程序被分成若干个通路，同时规定每一通路都不含中间截断点。
2. 选取一个良序集 $(W, \preccurlyeq)$，并且在每一个截断点 $i$ 处定义一个终止表达式 $E_i(x,y)$
3. 证明所选取的断言是“良断言”，即对于每一个从程序入口到断点 $j$ 的通路 $a$ 有 $$P(x) \land R_a(x,y) \Rightarrow q_j(x, r_a(x,y))$$对于每个从断点 $i$ 到断点 $j$ 的通路 $b$ 有 $$q_i(x,y) \land R_b(x,y) \Rightarrow q_j(x, r_b(x,y))$$

步骤3证明了对于任何使 $P(x)$ 为真的 $x$，在每个断点 $i$ 处所给的断言 $q_i(x,y)$ 为真

4. 证明终止表达式是“良函数”。即对于每一个断言 $i$ 有： $$q_i(x,y) \Rightarrow (E_i(x,y) \in W)$$

步骤4证明了对每个断言 $i$，若断言 $q_i(x,y)$ 成立，则终止表达式 $E_i(x,y)$ 在所选取的良序集 $(W, \preccurlyeq)$ 中取值

5. 证明终止条件成立，即对于每一条从断点 $i$ 到 $j$，且是每个循环的一部分的通路 $a$ 有 $$q_i(x,y) \land R_a(x,y) \Rightarrow [E_i(x,y) \succcurlyeq E_j(x, r_a(x,y))]$$

步骤5进一步告诉我们，当程序通过与循环有关的每一条通路时，$E_i(x,y)$ 的值在所规定的关系 $\preccurlyeq$ 的意义续下递减

例：证明计算 $z=\sqrt{x}$ 的程序的终止性

1. 在 $B'$ 处将循环断开，有：$q(x,y_1,y_2,y_3): y_2 \leqslant x \land y_3>0$
2. 取良序集为 $(N,\preccurlyeq)$，即具有小于关系的自然数集合，并在 $B'$ 点定义终止表达式：$E(x,y) = x-y_2$
3. 证明 $q(x,y)$ 是良断言，即证明对路径 $A \rightarrow B'$ 有： $$P(x) \land \text{True} \Rightarrow q(x,0,0,1)$$即： $$x \geqslant 0 \Rightarrow 0 \leqslant x \land 1>0$$对路径 $B' \rightarrow B'$ 有： $$q(x,y) \land y_2+y_3 \leqslant x \Rightarrow q(x,y_1+1,y_2+y_3,y_3+2)$$即： $$y_2 \leqslant x \land y_3>0 \land y_2+y_3 \leqslant x \Rightarrow (y_2+y_3 \leqslant x \land y_3+2>0)$$可以证明上式为真，因此中间断言 $q(x,y)$ 是良断言。
4. 证明 $E(x,y)$ 是良函数，即 $q(x,y) \Rightarrow E(x,y) \in N$，等价于 $$y_2 \leqslant x \land y_3>0 \Rightarrow x-y_2 \geqslant 0$$
5. 证明终止条件成立，与循环有关的通路只有 $B' \rightarrow D \rightarrow B'$，因而只需证明 $$q(x,y) \land y_2+y_3 \leqslant x \Rightarrow (E(x,y)>E(x,y_1+1,y_2+y_3,y_3+2))$$即： $$y_2 \leqslant x \land y_3>0 \land y_2+y_3 \leqslant x \Rightarrow (x-y_2)>(x-(y_2+y_3))$$这样，就证明了程序的终止性。

Hoare公理学方法

Hoare系统是一个关于形如 $[P]\ S\ [Q]$ 的断言的逻辑系统。$[P]\ S\ [Q]$ 是为了区别于完全正确的 $\{P\}S\{Q\}$ 断言的部分正确性断言的表示方法。这种方法是针对WHILE型程序提出的。

基本概念

不变式语句

其中，$P,Q$ 是逻辑表达式，$F$ 是一个程序段。它的含义是：“如果执行 $F$ 以前 $P$ 成立，且执行终止，则执行 $F$ 后 $Q$ 成立”，这时不变式语句为真，有时也称为归纳表达式。

推理规则

其中，$B$ 是一个不变式语句，$A_i(i=1,2,\cdots,n)$ 是一个逻辑表达式或是其它不变式语句。它的含义：“为了推导后项为真，只需证明前项 $A_1, A_2, \cdots, A_n$ 为真。”

采用上述记号，一个程序 $F$ 关于其输入断言 $P(x)$ 和输出断言 $Q(x,z)$ 的部分正确性可以表示为:

因而，证明程序 $F$ 的部分正确性，就可以归结为证明这一归纳表达式为真。

Hoare系统的公理及其推理规则

1. 赋值公理 $$[P(x,g(x,y))] \quad y \leftarrow g(x,y) \quad [P(x,y)]$$
2. 条件规则 $$\frac{[P \land R] \ F_1 \ [Q], \quad [P \land \lnot R] \ F_2 \ [Q]}{[P]\ \text{if} \ R \ \text{then} \ F_1\ \text{else} \ F_2 \ [Q] }$$或者 $$\frac{[P \land R] \ F_1 \ [Q], \quad P \land \lnot R \Rightarrow Q}{[P] \ \text{if} \ R \ \text{then} \ F_1 \ [Q]}$$
3. While规则 $$\frac{P \Rightarrow I, \quad [I \land R] \ F \ [I], \quad I \land \lnot R \Rightarrow Q}{[P] \ \text{while} \ R \ \text{do} \ F \ [Q] }$$
4. 并置规则 $$\frac{[P] \ F_1 \ [P_1], \quad [P_1] \ F_2\ [Q]}{[P] \ F_1; F_2 [Q]}$$
5. 结论规则 $$\frac{P \Rightarrow R,\quad [R] \ F\ [Q]}{[P] \ F\ [Q]}$$或者 $$\frac{[P] \ F\ [R], \quad R \Rightarrow Q}{[P] \ F\ [Q]}$$

📝 备注

1. 程序设计总是和具体的应用领域相关。
2. 程序 $F$ 是针对某一具体的论域的，$g(x,y)$ 和 $R$ 是论域中的项或谓词，另外 $P, Q, R, I$ 也是论域上的谓词公式。
3. 因此，上述公理和推理规则可以看作是对论域理论的扩充。

派生规则：

1. 赋值规则 $$\frac{P(x,y) \Rightarrow Q(x, g(x,y))}{[P(x,y)] \quad y \leftarrow g(x,y) \quad [Q(x,y)]}$$
2. 重复赋值规则 $$\frac{P(x,y) \Rightarrow Q(x, g_n(x, g_{n-1}(x, \cdots, g_2(x, g_1(x,y)) \cdots)))}{[P(x,y)] \quad y \leftarrow g_1(x,y); y \leftarrow g_2(x,y); \cdots; y \leftarrow g_n(x,y) \quad [Q(x,y)]}$$
3. 变形并置规则 $$\frac{[P] \ F_1\ [Q], \quad [R] \ F_2\ [S], \quad Q \Rightarrow R}{[P] \ F_1;F_2 \ [S]}$$

证明过程

正向“证明”：从某些公理出发，使用规则，直到最后获得结果。

1. 根据给出的不变式断言，建立一些引理；
2. 根据引理和赋值公理，对程序中的每一个赋值语句 $F_i$ 导出相应的不变式语句 $[R_i] \ F_i\ [Q_i]$；
3. 再根据这些不变式语句和上述的推理规则逐步地组成越来越长的程序段，一直到推演出 $[P(x)] \ F\ [Q(x,z)]$ 为止。

反向“证明”：先用规则，把总目标分成若干子目标，最后寻根于公理。

1. 从不变式语句 $[P(x)]\ F\ [Q(x,z)]$ 出发，利用有关的规则将它逐步分解，一直到将所有的语句推演为逻辑表达式（即检验条件）；
2. 然后，证明这些逻辑表达式成立；
3. 这样就证明了程序的部分正确性。

最弱前置条件

最弱前置条件是Dijkstra提出的一种演绎系统，它提供了一种算法解决方案，在向后方向上对程序语句执行符号执行，以推断出满足给定后条件的谓词。

假定 $S$ 是一个语句，$R$ 是一个谓词，它描述 $S$ 执行后所确定的某种关系。从 $S$ 和 $R$ 定义另外一个谓词，记为 $\text{wp}(S,R)$，表示：所有这样的状态的集合，S从其中任一状态开始执行，必将在有限的时间内终止于满足R的状态。我们称经过这样推导出的谓词为最弱前置条件。语句 $S$ 和后置条件 $Q$ 的最弱前置条件 $P$ 记作

性质和公理

排奇律

要从某个状态集的任何一个状态出发执行 $S$ 后必定会终止，终止时满足 $F$ ，即使 $F$ 为真，这样的状态是找不到的，因此对应的状态集为空。

单调律

如果 $R \subset Q$，则

合取分配律

表示从某一状态开始执行 $S$ 能终止，且分别满足 $Q$ 和 $R$ 的状态，那它终止时当然满足 $Q \land R$，反之亦然。

析取分配律

对于确定程序：从某一个状态出发，程序不管执行多少次，所经过的路径相同，所得的结果也相同。

对于不确定程序：从某一个状态出发，程序的任何两次执行可能得到的结果都不同，有时即便所得的结果相同，可能经过的路径也不同。

几种常用语句

跳过（Skip）

跳过语句是一个空白语句，不会改变程序状态。更具体地说，它不影响后置条件，即

例如，对于如下语句：

则有 $\text{wp}(\text{skip}, x>0) = x>0$

每个语句都可以被视为一个谓词转换器，将前置条件转换为后置条件。$\text{wp}(S，Q)$进行逆变换。

赋值（Assignment）

赋值语句的格式为 $\text{value} = \text{expression}$。赋值语句将更改程序状态，导致左侧的变量发生变化。即

例如，对于如下语句：

则有 $\text{wp}(x=y+5, x>7) = y+5>7 = y>2$

后置条件可以有许多前置条件。对于上述示例，$y>2$、$y>34$、$y>100$ 都可以确保后置条件 $x>7$。其中 $y>2$ 是约束条件最小的，因此是最弱前置条件。

序列（Sequence）

序列表示一组语句，一个序列通常会导致状态发生多次变化。即

其实这是两个语句的结合：

$$\text{wp}(S_2, R) = \text{wp}(x=E_2, R) = R[x \leftarrow E_2] = Q$$

$$\text{wp}(S_1, Q) = \text{wp}(x=E_1, Q) = Q[x \leftarrow E_1] = P$$

例如对于如下语句：

则有

📝 备注

一般地，有

$$ \text{wp}(S_1; \cdots; S_n, Q) = \text{wp}(S_1; \cdots; S_{n−1},P_{n−1}) \cdots = \text{wp}(S_1, P_1) = P$$

其中 $P_n=R$，$P_{i−1}=\text{wp}(S_i ,P_i)$，$P_0 = P$

分支（Branching）

格式为

例如对于如下语句：

则有