数理逻辑及其 python 实现:10

prover.add_universal_instantiation

如果直接用 Proof 类写证明，相当于每个证明都要重新实现一个 Proof 的实例，每个公式都要手动用 fomula parse 的形式去添加到 Proof 的 Line 对象中，还要手动引用公理模板进行实例化等等，因此作者提供了一个 Prover 类，它相当于一个给人方便使用的构造 Proof 类的工厂类，抽象出了一些方便的生成或者修改 Proof 类的接口，可以称为渐进式证明编写器。

比如以下是添加三段论经典命题里的假设，并根据假设以及一个具体的人物名称 – 亚里士多德，直接从全称命题（这是公理模板）得到具体命题：

step1 = prover.add_assumption('Ax[(Man(x)->Mortal(x))]')
step2 = prover.add_universal_instantiation(
'(Man(aristotle)->Mortal(aristotle))', step1, 'aristotle')

但 add_universal_instantiation 实际是先要根据 UI 公理（schema）到具体的一个命题，然后通过 MP 规则获得该命题里的结论部分，即让以上的第 2 步展开成以下证明的 2 到 3 步

step2 = prover.add_instantiated_assumption(
'(Ax[(Man(x)->Mortal(x))]->(Man(aristotle)->Mortal(aristotle)))',
Prover.UI, {'R': '(Man(_)->Mortal(_))', 'c': 'aristotle'})
step3 = prover.add_mp('(Man(aristotle)->Mortal(aristotle))', step1, step2)

这里核心是构造出 UI 公理的替换表格

{'R': '(Man(_)->Mortal(_))', 'c': 'aristotle'}

prover.add_tautological_implication

问题出现在以下证明的 5 到 7 步，主要是想说明所有希腊人都是会死的，而利用的是 (p->q)->((q->r)->(p->r)) 这个重言式，一步步根据 p->q

prover = Prover({'Ax[(Greek(x)->Human(x))]', 'Ax[(Human(x)->Mortal(x))]'},
print_as_proof_forms)
step1 = prover.add_assumption('Ax[(Greek(x)->Human(x))]')
step2 = prover.add_universal_instantiation(
'(Greek(x)->Human(x))', step1, 'x')
step3 = prover.add_assumption('Ax[(Human(x)->Mortal(x))]')
step4 = prover.add_universal_instantiation(
'(Human(x)->Mortal(x))', step3, 'x')
step5 = prover.add_tautology(
'((Greek(x)->Human(x))->((Human(x)->Mortal(x))->(Greek(x)->Mortal(x))))')
step6 = prover.add_mp(
'((Human(x)->Mortal(x))->(Greek(x)->Mortal(x)))', step2, step5)
step7 = prover.add_mp('(Greek(x)->Mortal(x))', step4, step6)
step8 = prover.add_ug('Ax[(Greek(x)->Mortal(x))]', step7)

改成只需要一步就可以证明：

step5 = prover.add_tautological_implication(
'(Greek(x)->Mortal(x))', {step2, step4})

因此这是一个根据前提和结论，构造出级联的蕴含关系的命题，所以做法是，对给定的步骤反向构造出嵌套的 -> 串联公式，将该公式以重言公式加入（加入过程会自动检查是否是恒真），然后再一步一步用 MP 层层解开。

注意这实际是证明里的一个关键手段，因为很多时候，证明可以先把量词尽可能去掉，从而剩下类似命题逻辑的组合公式，比如包含了 p,q, 那么一切可以根据 p,q 证明的公式都是能够调用 add_tautological_implication 添加进去，比如 p&q, p->q 等等

add_existential_derivation

问题是希望优化以下最后 3 步骤

step1 = prover.add_assumption('Ax[(Man(x)->Mortal(x))]')
step2 = prover.add_assumption('Ex[Man(x)]')
step3 = prover.add_universal_instantiation(
    '(Man(x)->Mortal(x))', step1, 'x')
step4 = prover.add_instantiated_assumption(
    '(Mortal(x)->Ex[Mortal(x)])', Prover.EI,
    {'R': 'Mortal(_)', 'c': 'x'})
step5 = prover.add_tautological_implication(
    '(Man(x)->Ex[Mortal(x)])', {step3, step4})
step6 = prover.add_ug('Ax[(Man(x)->Ex[Mortal(x)])]', step5)
step7 = prover.add_instantiated_assumption(
    '((Ax[(Man(x)->Ex[Mortal(x)])]&Ex[Man(x)])->Ex[Mortal(x)])', Prover.ES,
    {'R': 'Man(_)', 'Q': 'Ex[Mortal(x)]'})
step8 = prover.add_tautological_implication(
    'Ex[Mortal(x)]', {step2, step6, step7})

这里我们希望从 "所有对象都是人，那么存在某个会死的对象" 直接得到 "存在某个会死的对象", 这可以作为一个预设的公理，但由于只提供了 ES 公理，我们必须先把句子上升到全称命题，再手动构造 ES 实例，然后通过重言命题构建推理，

直接用 step 6 替代

step5 = prover.add_tautological_implication(
    '(Man(x)->Ex[Mortal(x)])', {step3, step4})
step6 = prover.add_existential_derivation('Ex[Mortal(x)]', step2, step5)

核心也是构造替换字典，并封装以上三句。

prove_lovers

根据 "每个人都有各自喜欢的人"(喜欢别人的人被称为 lover) 以及 "如果 x 喜欢 y, 那么 x 会被所有人喜欢" (everyone loves a lover)

证明 "每个人都喜欢所有人"

这基本是一句无意义的话，可以从纯形式角度去证明，这里实际表明 everyone loves a lover 有歧义，以上选择的是一种比较极端的解释，逻辑上导出了一个现实中错误的结论（除非只限定在很小的团体）。

prove_homework

根据 "所有作业都是无趣的" 以及 "有些作业是阅读" 推导出 "有些阅读是无趣的"

{'~Ex[(Homework(x)&Fun(x))]', 'Ex[(Homework(x)&Reading(x))]'},
# 结论
'Ex[(Reading(x)&~Fun(x))]'

从语义的角度：

• 没有作业是有趣的，那么对于任何作业来说，它都是无趣的。H(x)->~F(x) 但包含存在量词的逻辑公理只有以下两条：

  #: Axiom schema of existential introduction
  EI = Schema(Formula.parse('(R(c)->Ex[R(x)])'), {'R', 'x', 'c'})
  #: Axiom schema of existential simplification
  ES = Schema(Formula.parse('((Ax[(R(x)->Q())]&Ex[R(x)])->Q())'),
              {'Q', 'R', 'x'})
  

  我们无法直接得到这个结论。

  不过 EI 看上去可行，至少可以构造出 Ex[(Homework(x)&Fun(x))] 相关的公式

• 有些作业是阅读，那么有些阅读就是作业； Homework(c), Reading(c)
• 那么有些阅读就是无趣的： ~F(c)

这个过程要拆分成很多看似没有意义的小步骤。

Prover.add_flipped_equality

本题开始用证明简单加法群中的一个定理 x+0=x 为例子，补充那些能够方便编写证明的函数。

Group 是相对简单的数学结构，加法群只有加法一个二元函数，和负数这个一元函数，群公理只有三条：

• Zero Axiom: ‘plus(0,x)=x’ 或 0+x=x • Negation Axiom: ‘plus(minus(x),x)=0’ 或 -x+x=0 • Associativity Axiom: ‘plus(plus(x,y),z)=plus(x,plus(y,z))’ 或 (x+y)+z = x+(y+z)

本题根据这些定理证明 x=y 能够推出 y=x, 这是证明 x + 0 = x 中需要用到的一个中间定理，当然这更是等价关系里的一条公理。

关于等于关系，目前有两条公理：

RX = Schema(Formula.parse('c=c'), {'c'})
ME = Schema(Formula.parse('(c=d->(R(c)->R(d)))'), {'R', 'c', 'd'})

看上去 ME 是最接近的，比如其中 R(c)->R(d) 可能对应成 x=y->y=x, 但 R 由于是一个一元关系，因此考虑将其定义为 "_=x", 但这里替换 R(x) 的时候是否违背禁令了？并不违背，因为 "_=x" 中的 x 不是受限的，它和传入的 x 在同一个作用于域下。

这里可以看到 ME 实际是一个很强的性质，ME 结合 RX 解可以推导出对称性公理，

Prover.add_free_instantiation

Prover.add_free_instantiation(self, instantiation
                               line_number: int,
                               substitution_map:
                               Mapping[str, Union[Term, str]]) -> int:

到目前为止，如果要把 x=-x 变成 -x=–x, 实际要经过三步：

• 用 UG 规则把 x=-x 变成全称形式 A(x)(x=-x)
• 用 UI 公理模板 '(Ax[R(x)]->R(c))' 见其中 R 替换成 P=-P 关系，其中 P 是 placeholder, c 替换成 -x.
• 用 MP 得到 -x=–x

本题就是添加一个快速规则，直接在具体公式层面进行替换，这类似命题逻辑里的 specialization 。

实现的时候，要注意变量名混淆的问题，这类似交换两个变量值的问题，我们不能用 x=y,y=x 来交换 x 和 y 的变量值，而是引入一个新的 z, 用 z=x,x=y,y=z 方式来实现，具体参考书本 guideline 。

Prover.add_substituted_equality,

当我们知道 0=a 时，我们希望能把某个式子中出现的某个 0 替换成 a, 得到以下等式：

(0 + x) + 0 = (a + x) + 0,

目前能用的手段是和实现 T10.6 之前想证明 x=y -> y=x 类似：

• 用 ME 公理，其中 R 是目标结果的模板，例如我们想要得到 (0 + x) + 0 = (a + x) + 0, 于是就要构造模板 (0 + x) + 0 = (_ + x) + 0,

  这时候就可以把 0 和 a 分别代入，得到 0=a->(((0 + x) + 0 = (0 + x) + 0)->((0 + x) + 0 = (a + x) + 0)). 然后根据 MP 得到：

  (((0 + x) + 0 = (0 + x) + 0)->((0 + x) + 0 = (a + x) + 0)). 然后根据 MP

• 其中蕴含左侧是 ((0 + x) + 0 = (0 + x) + 0), 这是一个 c=c 形式，于是要对 RX 公理实例化， 再通过 MP 得到蕴含右侧的 ((0 + x) + 0 = (a + x) + 0)), 也就是最终结果。

  RX = Schema(Formula.parse('c=c'), {'c'})
  ME = Schema(Formula.parse('(c=d->(R(c)->R(d)))'), {'R', 'c', 'd'})
  

  本题就是把以上思路实现封装成函数。

  换一个角度看，把 (_+x)+0 看作函数的话，这里实际体现出了这样一种性质： 如果 a=b, 那么 f(a)=f(b)

Prover.add_chained_equality 

这里是证明等于关系的传递性，并且可以扩展到任意多，如 a=b,b=c,c=d, 那么 a=d 。

和 T10.6 证明对称性、T10.8 证明变量替换性思路类似，先考虑证明 a=b,b=c 得到 a=c 。

有了 a=c, 就可以循环使用以上方式，结合 c=d 来得到 a=d 。

根据 T10.8 的替换性质，定义函数 f 是 -a+_, 那么直接得到 -a + a+c =-a+a

-a + a + c = 0+c 0+c = c -a+a = 0

然后各种 flip 再用 T10.9 的方法串联起来，更多是熟悉编程接口

虽然非常简单的几步，但是写起来相对非常繁琐，要考虑封装。

群中只有一个一元运算，要么是乘法要么是加法，而域则包含加法和乘法，加法和乘法要满足群里的（交换、结合）公理，同时乘法和加法交互上要符合分配率，此外还有各自的逆元性质：

FIELD_AXIOMS = frozenset(GROUP_AXIOMS.union(
    {'plus(x,y)=plus(y,x)', 'times(x,1)=x', 'times(x,y)=times(y,x)',
     'times(times(x,y),z)=times(x,times(y,z))', '(~x=0->Ey[times(y,x)=1])',
     'times(x,plus(y,z))=plus(times(x,y),times(x,z))'}))

要证明 0x=0

• 0+x=x 得到 0+0=0
• 根据替换性，两边代入乘 x 操作，那么 x(0+0)=x0
• 根据分配率，那么 x0+x0=x0
• 类似 T10.10, 得到 x0=0
• 根据乘法交换律，0x=x0
• 根据等式传递性，0x=0

Peano 公理系统是用于定义自然数以及其上的加法和乘法，注意它既不是群也不是域，核心原因是没有加法和乘法逆元， 它的局部如加法下自然数集合只能说形成了一个交换半群。

INDUCTION_AXIOM = Schema(
    Formula.parse('((R(0)&Ax[(R(x)->R(s(x)))])->Ax[R(x)])'), {'R'})
#: The seven axioms of Peano arithmetic
PEANO_AXIOMS = frozenset({'(s(x)=s(y)->x=y)', '~s(x)=0', 'plus(x,0)=x',
                          'plus(x,s(y))=s(plus(x,y))', 'times(x,0)=0',
                          'times(x,s(y))=plus(times(x,y),x)', INDUCTION_AXIOM})

公理中加法和乘法交换律都没有给出，但它们实际可以从以上公理推导出来，而为了证明交换律，先要证明 0x=0 以及 0+x=0, 注意公理给出了 x0=0 以及 x+0=0

文中给出了 0x=0 的证明，本题则是 0 + x = x 的证明实现，描述上也是相对简单的，核心是转换为编程语言。 以下是思路

• 根据公理 x+0=x 得到 base case 0+0=0
• 接着假设 0+x=x, 那么有 s(0+x)=s(x), 根据公理 x+s(y)=s(x+y) 有 s(0+x) = 0+s(x) 因此就有了 0+s(x) = s(x), 接着就可以使用数学归纳法了。

关键是用到 ME 和数学归纳法。

这里使用 ME 要非常灵活，比如在归纳阶段，需要证明 0+x=x->0+s(x)=s(x), 如果我们可以随意引入一个假设空间（一些书本称为想象规则），那么这个证明是相对简单的，问题在于本文公理中不支持随意引入假设，因此只能通过 ME 规则间接引入。

ME = Schema(Formula.parse("(c=d->(R(c)->R(d)))"), {"R", "c", "d"})

ME 规则如上，当需要要 0+x=x->0+s(x)=s(x) 形式的公式时，可以直接把 R 设置成 0+x=x->_=s(x), 然后从一个已经有的公式直接得到稍微复杂一点的嵌套公式，然后逐步去解开。

一些技巧案例：

• 假设 a=b, 证明 b=a, 这里如果公理中给出了等于关系的对称性，是可以直接应用的，但如果没有给出，就需要 ME

  a=b->(a=a->b=a), 接着用 a=b 这个假设以及等于关系自反性公理 a=a 证得 b=a

• 如果是在有假设情况下的等于关系呢？，例如 a=b, 要证明 p->b=a, 这仍然使用 ME: R 关系设置为 p->_=a a=b->((p->a=a)->(p->b=a)) 得到 ((p->a=a)->(p->b=a)) 这时候要证明 (p->a=a), 需要先引入命题 a=a 为恒真，那么就是构造重言式。
• 根据 p->(q->r) 以及 q 可以直接得到重言的 p->r

Peano 公理的问题在于无法表达某种特定的无限对象，尽管它表达的那个模型的空间是无限大的，即有无数的自然数， 但它本身基本还是只能描述有限结构，注意它可以描述一些无理数的性质，比如根号 2 不是有理数，但它

ZFC 避开了罗素悖论

这就需要引入集合论作为模型，并且随之构建一套关于集合论的公理，朴素集合论中的无限制概括公理会导致罗素悖论， 这条公理的描述如下：

#: Axiom schema of (unrestricted) comprehension
COMPREHENSION_AXIOM = Schema(
Formula.parse('Ey[Ax[((In(x,y)->R(x))&(R(x)->In(x,y)))]]'), {'R'})

以上称为无限制的概括公理，这条公理说的是某个对象 y 可以通过它与其他任意对象的关系来构建，如果要谈这是什么关系， 那么可以说这是集合中的包含关系，这是人类直觉所提供的概念。

问题在于以上式子中的 R 关系也可以是包含，并且可以是不包含

• 实例化存在量词： 假设存在的集合就是 c, 那么可以写成 Ax[((In(x,c)->R(x))&(R(x)->In(x,c)))]
• 替换 R(x) 为 ~In(c,c) 关系： Ax[((In(x,c)->~In(c,c))&(~In(c,c)->In(x,c)))]
• UI 公理实例化全称量词：((In(c,c)->~In(c,c))&(~In(c,c)->In(c,c)))
• 以上是一个矛盾语句，可以推导出任何命题

但实现上，我们没有直接用个例去替换存在量词变量的公理规则，因此形式上没法这么操作。

• 考虑先把 R(x) 替换为 ~In(_, _) ，因为后者没有自由变量，不违反禁令，得到

  Ey[Ax[((In(x,y)->~In(x,x))&(~In(x,x)->In(x,y)))]]

• 对存在量词的处理 出现存在量词的两个公理如下

  EI = Schema(Formula.parse("(R(c)->Ex[R(x)])"), {"R", "x", "c"})
  ES = Schema(
       Formula.parse("((Ax[(R(x)->Q())]&Ex[R(x)])->Q())"), {"Q", "R", "x"}
   )
  

  能把存在量词消除的似乎是 ES, 因为可以把 Ex 语句变成一个任意的 Q() 语句，首先 Q() 是不带 x 和 y 变量的， 并且它应该是一个矛盾语句，即前文提到的把 x,y 都变成一个固定集合 c

  ((In(c,c)->~In(c,c))&(~In(c,c)->In(c,c)))
  

• 因此，核心目标是构造一个命题，其中根据两重全称量词得到一个具体的特例命题，类似：

  Ax[Ay[R(x,y)->R(c,c)]]
  

  但要注意的是，ES 的格式其实是：

  Ax[Ay[R(x,y)]->R(c,c)]
  

  UI 公理形式如下：

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

  因此看上去是做一次 UI

  我们把 R(x) 替换成 Z(x,y)

根据 UI, 以下定理是成立的

(Ay[Ax[((In(x,y)->~In(x,x))&(~In(x,x)->In(x,y)))]]->Ax[((In(x,c)->~In(x,x))&(~In(x,x)->In(x,c)))])

因此根据 ES, Q() 成立，这里的 Q 就是 Ax[((In(x,c)->~In(x,x))&(~In(x,x)->In(x,c)))] c 是常量，那么继续替换 x 为 c 就可以得到矛盾命题。

这里写起来要非常细，需要熟悉这种底层纯形式操作。

注意这里的证明实际没有太多意义，核心都是字符串模式的观察，真正的意义还是来自于六条基本公理。