数理逻辑及其 python 实现:11

本节证明以下定理

Let A be a set of schemas that includes US, and let φ and ψ be two formulas. If A ∪ {φ} ` ψ via a proof that does not use UG over any variable name that is free in φ, then A ` ‘(φ→ψ)’.

theorem 11.1 (The Deduction Theorem for Predicate Logic)

首先回顾命题逻辑的演绎定理是如何被证明的，它实际是一种递推动态规划算法，对给定原始证明的每一行，都将其前提消除掉，如果前提是 p1, 而当前行是 q, 则转成 p1->q, 从而把前提 p1 从推理规则中消除，这里有两个问题：

• 为什么可以彻底消除某条假设 p1 对证明的影响？

  证明过程就像水流的汇聚，每个步骤得到的结论都有固定数量的来源：

  • 从假设中直接引用：例如我需要证明 p1, 这不是一个重言命题，因此必须有假设声称 p1 为真才行，因此在证明中， 可能直接根据假设引入了 p1. 这里虽然证明过程里只出现了 p1 这个看似孤立的公式, 但实际它是来自于源头的假设。

    而消除源头假设，实际是把假设明确地写出来，比如变成 p1->p1, 它表明 p1 是在 p1 为真的条件下成立的。

    所以消除证明中的假设实际是在明确地把假设编码到每一步结论公式本身里，把潜规则变成白纸黑字。

  • 除了直接引用假设，证明中，还用到以下推理规则

  I0: [] => ‘(p→p)’
  I1: [] => ‘(q→(p→q))’
  D:  [] =>  ‘((p→(q→r))→((p→q)→(p→r)))’
  MP: [p, 'p->q'] => ‘q’
  

  其中前三条规则是没有依赖的，也就是可以直接实例化成一条具体公式（证明的某一步），其中可能会包括假设命题，例如根据 I0 推理规则，我们直接可以实例化得到 (p1->p1), 但这条公式并不需要以 p1 为真而成立。

  因此对于 I0,I1 和 D 实例化的公式，可以不做处理，但考虑还有 MP 规则，MP 规则是会引用之前的证明步骤来支撑证明的，如果不对 I0,I1,D 产生的公式进行处理，一旦 MP 规则里依赖了假设命题，例如根据 p1 和 p1->q 证明了 q，由于假设命题已经从 p1 改成了 p1->p1, 因此它就失效了，而 p1->q 这条公式对证明也没有意义，因为我们目前需要的结论是 p1->q, 因此我们要的规则是 ((p1->p1)->(p1-q)), 结合 p1->p1 以及 MP 就可以得到。

  参考第五章，通过 I0, I1 和 D 是能够构造出这条规则。

• 谓词逻辑在消除前提上有哪些不同？

  首先，不考虑具体实现问题，谓词逻辑把命题细分了，命题之间的语义关系不是完全由联结词决定的，比如根据 x=y, y=z 得到 x=z 是由外部提供的等于关系的等价性所得到的。因此看上去也要用外部的公理来把前提消除掉。

  但从实现上看，本书中谓词逻辑的证明中，每一个公式所使用的规则都是 hard code 的，并且只包括 UG 和 MP, 而 在定理 11.1 中， UG 规则是不允许出现的，因为本书对自由公式的定义如 x>2 只表示当前阶段所有 x 大于 2， 它能够得到 Ax[x>1], 但如果演绎定理在 UG 下成立，那么得到 x>2->Ax[x>1] ，它等价于 x>2->Az[z>1] 也等价于 Ax[x>2->Az[z>1]], 其意义是，对于所有 x, x>2 时所有元素都大于 1, 否则对元素没有要求，那么该句子在模型元素都大于 2 的情况下是成立的，但它同样适用于没有任何元素大于 2 的模型，因为前提 x>2 永远不成立，这个句子仍然为真。

  因此谓词逻辑的证明中，要消除的前提是不包含自由变量的，在公理模板中，这类命题由 Q() 实例化而来。 由于我们可以直接用命题逻辑完备性的结论 – 任何重言式命题都可以被证明，因此我们 可以在适当的时候引入任何 p->X 形式的重言命题，比如 p->p, (q→(p→q)), 在证明命题逻辑演绎定理时，这些是预先提供的公理，分别对应以上提到的 I0 和 I1 。 这给了我们很大的灵活性，例如对于 MP 规则，命题逻辑证明中，要用 I0, I1, D 推理规则将 p,p->q 推导出 q 修正成 p->p, (p->p)->(p->q) 推导出 p->q 。

  但谓词逻辑里，直接修正成 p->p, p->(p->q), p->q 即可，因为在 p->p, p->(p->q) 为真情况下，p->q 是恒真的。

  只有对于证明中遇到 UG 规则的情况，需要用以下 US 公理去把前提 Q() 提取到量词前面

  US = Schema(
       Formula.parse("(Ax[(Q()->R(x))]->(Q()->Ax[R(x)]))"), {"Q", "R", "x"}
   )
  

以根据 a=b 证明 b=a 为例，原始证明步骤为

1. a=b: 直接引用假设实例化
2. (a=b->(a=a->b=a)): 从 ME 公理实例化得到
3. (a=a->b=a): MP 规则从 1,2 得到
4. a=a: 从等式自反性 RX 公理实例化得到
5. b=a: MP 规则由 3, 4 得到
6. Ax(b=a): UG 规则。因为 b=a 中没有自由变量，但为了说明 UG 规则的处理方式强行加上全称量词

要将以上证明变成直接从 a=b->b=a，那么

1. (a=b->a=b): 引用 p->p 这个重言公式

2. (a=b->(a=a->b=a)): 从 ME 公理实例化得到，和原始证明第二步，保留

   2.5: (a=b->(a=b->(a=a->b=a))), 根据 2 得到的重言公式

3. (a=b->(a=a->b=a)): 2, 2.5 得到的重言公式

4. a=a: 从等式自反性 RX 公理实例化得到，等于元证明第 4 步，保留； q

   4.5: (a=b->a=a), 从 4 得到的重言公式

5. (a=b->b=a): 3 和 4.5 得到的重言公式
6. Ax((a=b->b=a)): UG 规则
7. (Ax[(a=b->b=a)]->(a=b->Ax[b=a])): 引入 US 得到
8. a=b->Ax[b=a]: 由于 6,7 从 MP 规则得到

这里可以看到：

• 如果是假设直接引入，那么把这句话变成 p->p 形式即可，不增加行数
• 如果是引入公理，那么先保留本行，再插入一行加入了 p-> 前缀的行，且本行直接依赖上一行

• 如果是 UG 行，则在量词内部加上 p-> 前缀，然后添加新的两行，

  这里有许多实现上的细节，比如替换出 US 中 R 的模板

• UG 规则和 MP 规则的依赖行号都需要修正
• 对于原本就是重言式的情况，直接修改成 p->X 形式，这还是重言式

本节证明反证法的合理性：

Let A be a set of schemas that includes US, and let φ be a formula. If a contradiction (i.e., negation of a tautology) is provable from A ∪ {φ} without using UG over any variable name that is free in φ, then A ` ‘~ φ’.

theorem 11.2 (Soundness of Proofs by Way of Contradiction in Predicate Logic)

回顾第五章，为什么有了演绎定理才能去说明反证法的有效性，没有它就说不了吗？

这是因为，反证法说的是，如果引入某个命题的反面 ~p, 能证明出矛盾命题，如 (~p&p)，那么就可以得出结论说 p 是正确的。这里 "能证明出矛盾命题" 描述的是证明过程，在代码中对应的是一个 Proof 对象，而有了演绎定理之后， 我们立刻可以把 ~p 从前提中拿掉，将整个证明变成从其他前提以及公理到 (~p->(~p&p)) 公式的 Proof 对象，而该公式结合以下的逆否公理

N = InferenceRule([], Formula.parse('((~q->~p)->(p->q))'))

就可以得到 ~(~p&p)->p, 由于 ~(~p&p) 是恒真（在命题逻辑里，这个结论一般是来自逻辑公理），因此再加上一个 MP 公理就证明了命题 p 。 所以说演绎定理在这里的作用是把反证法的前提编码到证明中，从而直接从而将反证法变成 正面证明法。

对于谓词逻辑，我们已经接纳了所有重言公式，因此不需要专门引用逆否公理，当有了 (~p->(~p&p)) 后，用重言蕴含 (add_tautological_implication) 一步就可以得到结论 p.

而当可以任意使用重言公式时，我们也不需要通过否定前提 ~p 去证明某个否定的公理，只要证明任何假的命题即可。

具体实现是：

• 给定 proof 对象，其中前提是 p, 结论是一个假命题 f
• 调用 remove_assumption 证明出 p->f
• 向其中直接添加结论 ~p

Prenex 是放在前面的形式，这里指的是可以把量词放到公式前面，个人称其为量词前缀化

A formula is said to be in prenex normal form if there is an initial sequence of nodes of the formula that all contain quantifications, and all other nodes in the formula do not contain quantifications.

definition 11.1 (Prenex Normal Form)

这里的要求解析树的前几层节点都是量词，而之后不存在量词，因此 ∀x[(∃y[R(x,y)]→Q(x))] 虽然在字符串形态上看所有量词都在前面，但实际从解析树上看，蕴含 -> 比 ∃y 更前，因此不是 prenex 形式。

此外 ~Ax[P(x)] 也不是 prenex 形式，需要把否定算子推后。

本题实现分成 a,b 两部分，a 是用递归方式去找当前公式是否包含量词，b 基于 a 去递归判断是否是 prenex, 实际可以合起来，但这里不考虑效率。

predicates/some_proofs.py _prove_not_exists_not_implies_all
predicates/some_proofs.py _prove_exists_not_implies_not_all
predicates/some_proofs.py prove_not_all_iff_exists_not

本节引入了量词前缀化定理，表明通过 UI, EI, US, ES 这四条公理就可以证明（不需要原本六条公理里的和等于相关的两条公理），所有谓词逻辑公式都可以写成 prenex 形式：

For every formula φ there exists an equivalent formula ψ in prenex normal form, such that the equivalence between φ and ψ (i.e., ‘((φ→ψ)&(ψ→φ))’) is provable from UI, EI, US, and ES.

theorem 11.3 (The Prenex Normal Form Theorem)

文中给出了额外的用于公式前缀化的 16 条公理，这些公理实际都可以通过 UI,EI,US,ES 推导出来，T11.4 就是四条公理证明额外公理的第一条，即 ‘~∀x[φ(x)]’ 与 ‘∃x[~φ(x)]’ 等价，拆分成三步：

• 证明 (~∃x[~φ(x)]→∀x[φ(x)])

  用到 EI, UG, Deduction 定理

• 证明 (∃x[~φ(x)]→~∀x[φ(x)])
  • ∃x[~φ(x)] ： 假设引入
  • ∀x[φ(x)]->φ(x) ： UI
  • ~φ(x)->~∀x[φ(x)] ： 上一条逆否
  • ~∀x[φ(x)] ： exist_derivation
  • 演绎定理综合起来
• 以上两步合起来 第二步已经是两个式子等价的第二个方向了， 而对第一步取反，得到 ~∀x[φ(x)]->∃x[~φ(x)], 这是等价的第一个方向。 再将二者合并即可。

一个疑问是， ~E(x)[P(x)] 等价于 A(x)[~P(x)] 是怎么根据以上公理来证明的？

其他一些比较微妙的等式：

‘(∀x[φ(x)]→ψ)’ is equivalent to ‘∃x[(φ(x)→ψ)]’
‘(∃x[φ(x)]→ψ)’ is equivalent to ‘∀x[(φ(x)→ψ)]’

个人感觉命题逻辑规则本身和集合论直觉是一体的，核心就是量词，它本身代表一种集合

predicates/prenex.py _uniquely_rename_quantified_variables

由于上一节引入了 16 条公理且从形式上证明了其中第一条是可证的，对于其他公理则直接证明其语义上的保真性 和证明谓词逻辑保真性类似，由于无法遍历模型空间，因此更多是在说明替换规则的性质。

在 prenex 化过程中，我们核心关注的就是量词在移动过程中，该量词所对应的变量的作用域是不变的。

本节是整个证明里第一步，确保变量之间不会混淆，例如 Ax[P(x)]&Ex[R[x]] 中 x 实际是不一样的，在将量词移动中，要保持命名的独立。

A formula is said to have uniquely named variables if no two quantifications in the formula quantify over the same variable name, and no variable name has both bound and free occurrences in the formula.

definition 11.2 (Uniquely Named Variables)

Ax[P(x)]&Ex[R[x]] 就不是有唯一独特变量名的公式，要将其转为 Ax[P(x)]&Ey[R[y]] 额外地，我们还要给出从替换前公式到替换后公式的证明，证明中可以用到额外的 16 条公理。

考虑最简单情况，如何把 Ax[P(x)] 通过公理形式化得到 Ay[P(y)], 可以根据 UI 性质，把 Ax[P(x)] 转成 P(y), 然后 ug 变成 Ay[P(y)] 问题是存在量词呢？此外各种连接符例如 ~,|,->,& 串联起来的量词如何处理？

这里的思路是垂直方向的，由于两个公式是同结构的，因此可以先建立起子结构之间的等价， 对于没有量词的部分，那么不需要替换变量名，它们之间是自然等价的，对于有量词的字句， 如果是存在量词就用公理 16 如果是全称量词就用公理 15, 更高层级等价则用重言推断，例如 p1&q1 和 p2&q2 ，如果有 p1<->p2 和 q1<->q2, 那么 (p1&q1)<->(p2&q2) 会是自然的。

算法总体是：

• 如果遇到 ~p 形式，那么对 p 递归，然后通过重言蕴含得到 ~p 上替换前后的等价关系
• 如果遇到 |,->,& 两边分别递归，再通过重言蕴含得到 pq 上替换前后的等价关系
• 如果是关系（或等于），说明这是自由的，不会被替换。 这里利用的核心性质是，对于关系或者等于，要么在量词中，要么是自由的不需替换。 只有逻辑联结词（在解析树上）才能在量词的上一层级。

• 如果遇到量词直接用公理 15 和 16, 然而实际没有这么简单，因为还存在嵌套情况，例如

  (Ax[(Ax[R(x)]&x=7)]|x=6)

  因此实际还是要继续递归，例如 Ax[R(x)] 已经被替换成 Az[R(z)] 并且有了

Ax[R(x)] <-> Az[R(z)] 的证明，这时候对于公理 15 中的 Q(x) 其实就是 Az[R(z)] 它没有 placeholder, 这个地方实现起来有许多细节。

如下是公理 15 和 16. 15 是相对容易证明，对于 15 只需要用重言蕴含拆分出 R(x)->Q(x) 和 Q(x)->R(x) ，然后用 UG 并再用一次重言蕴含即可。 16 则更像是对 Q(x) 这种写法的解释

Schema(Formula.parse('(((R(x)->Q(x))&(Q(x)->R(x)))->''
((Ax[R(x)]->Ay[Q(y)])&(Ay[Q(y)]->Ax[R(x)])))'),
{'x', 'y', 'R', 'Q'}) # 15
Schema(Formula.parse('(((R(x)->Q(x))&(Q(x)->R(x)))->''
((Ex[R(x)]->Ey[Q(y)])&(Ey[Q(y)]->Ex[R(x)])))'),
{'x', 'y', 'R', 'Q'}) # 16

_pull_out_quantifications_across_negation

这里实际是用代码实现来证明德摩根定律在谓词逻辑上扩展是可行的，并且可以在嵌套的情况下仍然生效。

核心是用到扩展的公理 1 和公理 2:

1. ~∀x[φ(x)]<->∃x[~φ(x)]
2. ~∃x[φ(x)]<->∀x[~φ(x)]

根据以上公理，我们可以得到一层嵌套，本题是证明多层嵌套，例如以下是两层 ~∀x[∀x[φ(x)]]<->∃x[∃x[~φ(x)]]

算法实现上肯定是递归的，但细节上看，最外层的证明依赖于内层，当我们从递归得到了内层等价的证明，还需要公理 15 和 16 去添加上一层量词，再用公理 1,2 去转换量词。

• 如何确定 base case:

  由于输入公式一定是以 ~ 开头的，这个性质应该始终保持，也就是进入到最内层递归时，

  看到的公式是 ~φ(x) 形式的，这时候 formula.root 是 ~, 而 formula.first 并不是量词，这时候返回 ~φ(x) 以及 (~φ(x)<->~φ(x)) 关系的证明。

• 递归过程： 先取当前公式 formula.first.state 取反后得到 ~s 作为参数进行递归调用，得到公式 f 和证明 proof

  检查当前量词，如果是 E 则取 Q=A, 否则取 Q=E, 变量是 x, 对 ~s 和 f 添加量词，得到 Qx[~s]<->Qx[f], 以上的 proof 就是对该公式的证明

  (对于 basecase 前一层), 根据公理 15/16 构建出

  Qx[~φ(x)]<->Qx[~φ(x)] 等价关系。

  同时根据公理 1/2 得到 ~Q'x[φ(x)]<->Qx[~φ(x)] 的证明，这是 Q' 就是当前层级的量词。

  用重言推理得到 ~Q'x[φ(x)] 和 Qx[~φ(x)] （下层返回的公式）的等价关系并返回公式 Qx[~φ(x)] 以及证明。

  再上一层根据公式 ~Q'x[φ(x)]<->Qx[~φ(x)] 加上当前量词的相反量词 O 和变量 y, 结合公理 15/16 得到：

  Oy[~Q'x[φ(x)]]<->Oy[Qx[~φ(x)]] 等价关系。

  再根据公理 1/2 得到 Oy[~Q'x[φ(x)]]<->~O'y[Q'x[φ(x)]], 右侧是当前的 formula.

  根据重言推理得到 ~O'y[Q'x[φ(x)]]<->Oy[Qx[~φ(x)]]

  返回 Oy[Qx[~φ(x)]]

_pull_out_quantifications_from_left_across_binary_operator
_pull_out_quantifications_from_right_across_binary_operator

上一节是讨论量词和否定运算符 ~ 的关系，本节讨论量词如何从 & | -> 这种二元运算符中提取出来。

本题分成了两个部分，分别是把左侧的量词提取出来，如 Ax[P(x)]|z 变成 Ax[P(x)|z] 以及把右侧的量词提取出来，如 z|Ax[P(x)] 变成 Ax[z|P(x)]

这里用例子说明 Ey[Ax[P(x)]]|z 变成 Ey[Ax[P(x)|z]], 总体思路基本和 11.6 是一样的，只不过用额外定理中的其他几条，更多是细节：

• 对于 base case, 仍然是递归到 P(x) 然后返回 (P(x)|y) 以及对 (P(x)|z)<->(P(x)|z) 的证明

• 最里层递归：

  当前输入 formula 为 Ax[P(x)]|z, 取出 formula.first.statement 并且和 z 组合传入递归函数得到结果： (P(x)|z) 以及 (P(x)|z)<->(P(x)|z) 的证明

  • 用公理 15/16 得到 Ax[P(x)|z]<->Ax[P(x)|z]
  • 用公理 7 得到 Ax[P(x)|z]<->Ax[P(x)]|z
  • 重言蕴含得到 Ax[P(x)|z]<->Ax[P(x)]|z
  • 返回 Ax[P(x)|z] 和上一条公式的证明

• 再上一层递归

  当前输入 formula 为 Ey[Ax[P(x)]]|z, 取出 formula.first.statement 并且和 z 组合传入递归函数得到结果： Ax[P(x)|z] 以及 Ax[P(x)|z]<->Ax[P(x)]|z 的证明

  1. 用公理 15/16 得到 Ey[Ax[P(x)|z]]<->Ey[Ax[P(x)]|z]

     量词来自本层公式量词，左侧公式是对返回公式加上一层包装的结果 右侧是对传入递归参数加上一层量词包装的结果。

  2. 用公理 8 得到 Ey[Ax[P(x)]|z]<->Ey[Ax[P(x)]]|z

     左侧是对传入递归的参数加上一层量词包装的结果。 右侧是当前输入的 formula

  3. 重言蕴含得到 Ey[Ax[P(x)|z]]<->Ey[Ax[P(x)]]|z
  4. 返回 Ey[Ax[P(x)|z]] 和以上公式的证明

注意，如果是 -> 符号， A 要变成 E, 例如：

当前输入 formula 为 Ey[Ax[P(x)]]->z, 取出 formula.first.statement 并且和 z 组合传入递归函数得到结果： Ax[P(x)->z] 以及 Ax[P(x)->z]<->Ax[P(x)]->z 的证明

1. 用公理 15/16 得到 Ay[Ax[P(x)->z]]<->Ay[Ax[P(x)]->z]

   量词来自本层公式量词取反的结果，左侧公式是对返回公式加上一层包装的结果 右侧是对传入递归参数加上一层量词包装的结果。

2. 用公理 10 得到 Ay[Ax[P(x)]->z]<->Ey[Ax[P(x)]]->z

   左侧是对传入递归的参数加上一层量词包装的结果。 右侧是当前输入的 formula

3. 重言蕴含得到 Ay[Ax[P(x)->z]]<->Ey[Ax[P(x)]]->z
4. 返回 Ay[Ax[P(x)->z]] 和以上公式的证明

对于 z 在右前侧的情况例如 z->Ax[Px] ，那么 Ax 不需要变换成 Ex, 它等价于 Ax[z->Px]

_pull_out_quantifications_across_binary_operator

上节分别讨论了量词(前缀塔形式的)公式只在二元运算符连接的公式的左边或者右边的情况， 本节则扩展到更广的情形： P[z]->Q[y] 形式的公式，这里 P 是一个嵌套的量词 prenex 塔（如 AxEx1），其最内层是 z， Q 也是一个 Prenex 嵌套塔（如 Ez1Ax2…），最内层公式是 y，需要变成 PQ(z->y), PQ 是两个 prenex 塔的重叠（如AxEx1Ez1Ax2… ）。

这里做法是先变成 P[z->Q[y]], 然后 P[Q[z->y]]

核心是如何把多个步骤的证明串联起来，比如从 P[z]->Q[y] 到 P[z->Q[y]] 只需要调用 T11.7a 的左 prenex 化实现即可，但 P[z->Q[y]] 到 P[Q[z->y]] 并不直接，还需要拆分，因为 T11.7b 只能从 z->Q[y] 到 Q[z->y] 如何在 P 这个 prenex 层叠塔下进行证明呢？

这里需要不断循环用公理 15/16 把 z->y 从 prenex 塔里一层一层取出来。

_to_prenex_normal_form_from_uniquely_named_variables

这里是把 T11.6 到 T11.8 的函数继续组合起来，核心还是在联结词上递归：

• 如果遇到 ~: 先对 formula.first 进行递归，递归的结果调用 T11.6 函数
• 如果遇到 |,& 和 ->: 在两边进行递归，对递归结果组合成公式后调用 T11.8 的结果
• 如果是量词，对 statment 部分递归，对递归的结果用公理 15/16 连接起来
• base case 是关系，直接返回等价证明

to_prenex_normal_form

对 11.5 和 11.9 的综合：

• 先对公式的变量名进行唯一化
• 将唯一化后的公式放入 11.9 函数中
• 将两个步骤的证明整合起来

总的来说，本章主要是在对公式做语法上的规范，本书中涉及到的规范形式有：

• 对于静态公式：命题逻辑的 CNF
• 对于证明：只包括 ~ 和 -> 的，用于证明命题逻辑演绎定理，服务于希尔伯特公理系统
• 谓词逻辑的 prenex 形式，用于下一章证明谓词逻辑的演绎定理