数理逻辑及其 python 实现:4

Notes on 「Mathematical logic through python」

2023-10-30 一 15:26 2025-02-02 日 20:45

四、命题逻辑的演绎证明

本章引入了 Proof, InferenceRule 这些语法上的操作对象，同时引入了它们的语义特点（是否 sound），并且最终证明了 soundness 定理（从语法连接到语义）

An inference rule is composed of a list of zero or more propositional formulas called the assumptions of the rule and one additional propositional formula called the conclusion of the rule.

definition 4.1 (Inference Rule)

首先定义推理规则类 InferenceRule, 它包括 assumptions （tuple of formula 或者空 tuple）和 conclusion 对象。

class InferenceRule:
    assumptions: Tuple[Formula, ...]
    conclusion: Formula

    def __init__(self, assumptions: Sequence[Formula], conclusion: Formula):
        self.assumptions = tuple(assumptions)
        self.conclusion = conclusion

    def __repr__(self) -> str:
        return str([str(assumption) for assumption in self.assumptions]) + \
               ' ==> ' + "'" + str(self.conclusion) + "'"

    def __eq__(self, other: object) -> bool:
        return isinstance(other, InferenceRule) and \
               self.assumptions == other.assumptions and \
               self.conclusion == other.conclusion

    def __ne__(self, other: object) -> bool:
        return not self == other

    def __hash__(self) -> int:
        return hash(str(self))

assumptions 就是一组公式或者是空集，conclusion 则是一个公式（Formula）

推理规则可以让我们进行演绎(deduce)，或者说是生成公式，可以把推理规则看作是字符串（公式）生成规则或函数。

T4.2 模型和推理规则的关系

We say that a set of assumption formulas A entails a conclusion formula φ if every model that satisfies all the assumptions in A also satisfies φ. We denote this by A |= φ.

We say that the inference rule whose assumptions are the elements of the set A and whose conclusion is φ is sound(truth-preserving ) if A |= φ.

definition 4.2 (Entailment; Soundness)

以上对推理规则可靠性（也称保真性）的定义是纯语义上的，因为只涉及到命题和 model 之间的关系，如果某推理规则是可靠的：

所有使得前提为真的 model 在结论中都为真
或者没有任何 model 使得前提为真
或者前提为空但 conclusion 恒真

以上语义的描述和逻辑运算符 -> 非常像，但它是动态的生成规则，而 -> 是静态的公式连接符号。在后文中会证明这两者是等价的。正如在第一章第一节提到，命题逻辑发明的一个重要原因就是研究 "蕴含", 而蕴含通过 -> 符号以及该符号的语义定义体现在了逻辑表达式中，也通过对推理规则的 soundness 体现在了推理过程中，不过：

推理规则一般不用"真"或"假"来分类：推理规则的“真”是用 sound 来表示（可以称为可靠或者保真）
公式才用真和假来表示； Modus Ponens 说的是，给定 P 和 P->Q 可以生成 Q, 这里 P,Q 不是具体的命题，而是一种模版。它虽然和 "(p^(p->q))->q" 很像，但它们并不是同一类对象（尽管最后完备定理就是证明类似它们等价）

比如以下的对推理规则语义检查函数，它返回的也是 True 和 False, 但这里的 True 表示的是该推理规则在某个模型下。

def evaluate_inference(rule: InferenceRule, model: Model) -> bool:
    assert is_model(model)
    # Task 4.2
    for formula in rule.assumptions:
        if not evaluate(formula, model):
            return True
    return evaluate(rule.conclusion, model)

注意：在以上代码中，根据 soundness 的定义，我们只关心符合 assumptions 的 model, 因此如果 model 使得推理规则中的某个 assumption 为 Fasle, 那么它就不会被作为验证推理规则是否为 soundness 的候选模型了，因此这里认为该推理规则在该模型下是 True，这个“隐性”的性质直接使得推理的语义和 imply 非常相似

T4.3 验证推理规则的 soundness

我们只需要验证所有为 True 的模型，这里需要暴力遍历，假设推理规则涉及 n 个变量，那么得到 2**n 个 model, 检查该推理规则是否对每个 model 的 evaluate 结果都是 True; 这与验证 (p&q&r)->z 形式的 formula 是否是 tautlogy 的算法是类似的。

def is_sound_inference(rule: InferenceRule) -> bool:
    for model in all_models(rule.variables()):
        if not evaluate_inference(rule, model):
            return False
    return True

T4.6 检查证明（Proof）是否有效

本节引入了另一个重要对象：证明；它包括：

要证明的对象 statement, 这是一个推理规则；
证明中使用到的推理规则 rules
以及整个证明的路径 lines, 这是一个由 Proof.Line 对象组成的序列，而 Proof.Line 本质是公式，但它还需要别的辅助信息，包括推导出这条公式所用的推理规则以及它所依赖的前提（是一个 int 数组，表示之前的 line 的下标）

class Proof:
    statement: InferenceRule
    rules: FrozenSet[InferenceRule]
    lines: Tuple[Proof.Line, ...]
    
    def __init__(self, statement: InferenceRule,
                 rules: AbstractSet[InferenceRule],
                 lines: Sequence[Proof.Line]):
        self.statement = statement
        self.rules = frozenset(rules)
        self.lines = tuple(lines)

    def __repr__(self) -> str:
        r = 'Proof of ' + str(self.statement) + ' via inference rules:\n'
        for rule in self.rules:
            r += '  ' + str(rule) + '\n'
        r += 'Lines:\n'
        for i in range(len(self.lines)):
            r += ('%3d) ' % i) + str(self.lines[i]) + '\n'
        r += "QED\n"
        return r

    class Line:
        formula: Formula
        rule: Optional[InferenceRule]
        assumptions: Optional[Tuple[int, ...]]

        def __init__(self, formula: Formula,
                     rule: Optional[InferenceRule] = None,
                     assumptions: Optional[Sequence[int]] = None):
            assert (rule is None and assumptions is None) or \
                   (rule is not None and assumptions is not None)
            self.formula = formula
            self.rule = rule
            if assumptions is not None:
                self.assumptions = tuple(assumptions)

        def __repr__(self) -> str:
            if self.rule is None:
                return str(self.formula)
            else:
                r = str(self.formula) + '    (Inference Rule ' + str(self.rule)
                if len(self.assumptions) == 1:
                    r += ' on line ' + str(self.assumptions[0])
                elif len(self.assumptions) > 1:
                    r += ' on lines ' + ','.join(map(str, self.assumptions))
                r += ')'
                return r

        def is_assumption(self) -> bool:
            return self.rule is None

接着定义可证明性：

Given a formula \(\phi\), a set of formulas A, and a set of inference rules R, a proof via R of the inference rule having conclusion \(\phi\) and assumptions A, or simply a proof via R of the conclusion \(\phi\) from the assumptions A, is a list of formulas whose last formula is \(\phi\), such that each of the formulas in the list is either in A or the conclusion of a specialization of a rule in R such that the assumptions of this specialization are preceding formulas in the list.

We say that the inference rule having assumptions A and conclusion \(\phi\) is provable via R, or simply that \(\phi\) is provable from A via R, if there exists a proof of that rule via R. We denote this by \( A\vdash_{R} \phi \)

definition 4.4 (Proof; Provability)

对其中提到符号再做一些解释：

A 和 \( \phi \) （用 phi 表示) 实际组成一个推理规则：
```
x_rule = InferenceRule(A, phi)
```
证明的时候，实际是用另外一些推理规则集合 R 去证明推理规则 x_rule
推理规则 R 实际就是逻辑系统中预设的公理集合（assumption 为空的推理规则）和推理规则集合的并集
\( A\vdash_{R} \phi \) 也会写成 A |-R phi, 表示的是，可以借助 R 从公式集合 A 中推导出公式 phi, 在实际应用中 A 是具体场景里的公式集合，可以看作公理，比如"如果红灯（p）那么停车（q）" 。然而，由于命题逻辑表达能力比较弱，因此很少有某个应用领域仅依赖命题逻辑就可以充分表达自身。在命题逻辑中，假设集合 A 通常用于证明某些恒真的定理。例如，如果假设集合 A 中包含命题 q，我们可以尝试证明 "p->q"。命题逻辑里这些恒真式或 sound 的推理规则经常被用作更复杂逻辑系统或数学理论中的基础公理或推理规则。

此外要说明的是，以上定义是纯粹语法上的（因为没有提到任何 model 或者可满足相关字眼），它完全是字符串规则变换，在没有语义加入的情况下我们可以检查这个证明是否有效（ valid ），即便推理规则是错误的，valid 也是可检查的。比如有推理规则说如果出现 p 就可以生成 q, 那么如果公理中有 p, 就可以通过这个规则得到 q, 这个证明是有效的。

以下实现的函数是给定证明行的编号，从中提取出推理规则实例，比如以上例子，有一行是的结论是 q, 它需要依赖 p, 因此这一行的 assumptions 中应该有 p 的编号，那么得到本行结论的推理规则实例就是 InferenceRule([p], q)

def rule_for_line(self, line_number: int) -> Union[InferenceRule, None]:
    assert line_number < len(self.lines)
    # Task 4.6a
    line = self.lines[line_number]
    conclusion = line.formula
    assumptions = []
    if hasattr(line, "assumptions"):
        for i in line.assumptions:
            assumptions.append(self.lines[i].formula)
        return InferenceRule(assumptions, conclusion)
    return None
Proof.rule_for_line = rule_for_line

接着根据推理规则检查本次推理是否合法，上一个函数得到的是推理规则的实例，而 line.rule 对象保存的是推理规则模版，因此我们要判断这个实例是否是该模版的实例：

def is_line_valid(self, line_number: int) -> bool:
    assert line_number < len(self.lines)

    # Task 4.6b
    line = self.lines[line_number]
    rule = self.rule_for_line(line_number)
    if rule is None:
        if line.formula in self.statement.assumptions:
            return True
        return False
    if not all(i < line_number for i  in line.assumptions):
        return False
    print(line_number ,rule, rule.is_specialization_of(line.rule))
    return line.rule in self.rules and rule.is_specialization_of(line.rule)

Proof.is_line_valid = is_line_valid

最后检查每条 line 是否有效，并且检查最后一条 line 的结论是否和证明的 statment 一样：

def is_valid(self) -> bool:
    # Task 4.6c
    if not self.lines:
        return False
    for i in range(len(self.lines)):
        if not self.is_line_valid(i):
            #print(f"{i} line {self.lines[i]} is not valid")
            return False
    return self.lines[-1].formula == self.statement.conclusion
Proof.is_valid = is_valid

T4.7 证明 ‘(p&q)’ 可以推出 ‘(q&p)’

首先这个结果看上去很"显然", 这种显然实际来自于语义层面，因为我们定义过 p&q 的真值表，容易发现 q&p 真值表和它一样。

但从语法的角度，却并不"显然"，这里我们要识别的是一种符号组合上的相似关系，以下引入了三条推理规则，这些规则的形式和我们要证明的结果是比较相似的，因此从语法上的证明也比较容易。

#: Conjunction introduction inference rule
A_RULE = InferenceRule([Formula.parse('x'), Formula.parse('y')],
                       Formula.parse('(x&y)'))
#: Conjunction elimination (right) inference rule
AE1_RULE = InferenceRule([Formula.parse('(x&y)')],Formula.parse('y'))
#: Conjunction elimination (left) inference rule
AE2_RULE = InferenceRule([Formula.parse('(x&y)')],Formula.parse('x'))

这里没有引入任何公理，一般来说，公理是没有 assumptions 的 InferenceRule, 是类似无中生有的推理规则，它的结论是恒真的。

def prove_and_commutativity() -> Proof:
    # Task 4.7
    assumptions = (Formula.parse('(p&q)'), )
    conclusion = Formula.parse('(q&p)')
    statement = InferenceRule(assumptions, conclusion)
    rules = [A_RULE, AE1_RULE, AE2_RULE]
    line0 = Proof.Line(assumptions[0], None, None)
    line1 = Proof.Line(Formula.parse("q"), AE1_RULE, [0])
    line2 = Proof.Line(Formula.parse("p"), AE2_RULE, [0])
    line3 = Proof.Line(Formula.parse("(q&p)"), A_RULE, [1, 2])
    lines = [line0, line1, line2, line3]
    return Proof(statement, rules, lines)

可以验证其是否有效

print(prove_and_commutativity())

Proof of ['(p&q)'] ==> '(q&p)' via inference rules:
  ['(x&y)'] ==> 'x'
  ['x', 'y'] ==> '(x&y)'
  ['(x&y)'] ==> 'y'
Lines:
  0) (p&q)
  1) q    (Inference Rule ['(x&y)'] ==> 'y' on line 0)
  2) p    (Inference Rule ['(x&y)'] ==> 'x' on line 0)
  3) (q&p)    (Inference Rule ['x', 'y'] ==> '(x&y)' on lines 1,2)
QED

prove_and_commutativity().is_valid()

self, general: ['(p&q)'] ==> 'q' ['(x&y)'] ==> 'y'
1 ['(p&q)'] ==> 'q' True
self, general: ['(p&q)'] ==> 'q' ['(x&y)'] ==> 'y'
self, general: ['(p&q)'] ==> 'p' ['(x&y)'] ==> 'x'
2 ['(p&q)'] ==> 'p' True
self, general: ['(p&q)'] ==> 'p' ['(x&y)'] ==> 'x'
self, general: ['q', 'p'] ==> '(q&p)' ['x', 'y'] ==> '(x&y)'
3 ['q', 'p'] ==> '(q&p)' True
self, general: ['q', 'p'] ==> '(q&p)' ['x', 'y'] ==> '(x&y)'
True

T4.9 替换规则在推理规则中的 soundness

本节实际说明的是替换规则是保真的（可靠的），只要规则是可靠的，那么规则经过替换规则实例化之后的结果也是可靠的。这里用的是逆否命题来说明，给定一个会令实例化的推理规则失效的模型，那么一定对应了一个让该推理规则失效的模型，实际是一个变量替换问题。

def rule_nonsoundness_from_specialization_nonsoundness(
        general: InferenceRule, specialization: InferenceRule, model: Model) \
        -> Model:
    assert specialization.is_specialization_of(general)
    assert not evaluate_inference(specialization, model)
    # Task 4.9
    smap = general.specialization_map(specialization)
    gmodel = {}
    for var, formula in smap.items():
        gmodel[var] = evaluate(formula, model)
    return gmodel

Every specialization of a sound inference rule is itself sound as well.

lemma 4.1 (Specialization Soundness)

这里看到，替换规则是更”元“的操作，推理规则可以让公式（命题）生成更多命题，替换规则可以让推理规则生成更多推理规则。

T4.10 命题逻辑的 soundness

上节证明了实例化（替换）操作的可靠性，这相当于解决了证明过程中垂直方向（宏）的可靠性，本节把证明的水平方向（函数执行）的可靠性也补充上

def nonsound_rule_of_nonsound_proof(proof: Proof, model: Model) -> \
        Tuple[InferenceRule, Model]:
    assert proof.is_valid()
    assert not evaluate_inference(proof.statement, model)
    # Task 4.10
    for i in range(len(proof.lines)):
        specialization = proof.rule_for_line(i)
        if specialization:
            if not evaluate_inference(specialization, model):
                general = proof.lines[i].rule
                gmodel = rule_nonsoundness_from_specialization_nonsoundness(general, specialization, model)
                return (general, gmodel)
    return None

以上函数中，参数 proof 是 valid 的，但结论相对 model 来说是错的，那么必然某个（些）推理规则是不可靠的

相当于用反证法证明以下定理：

Any inference rule that is provable via (only) sound inference rules is itself sound as well. That is, if R contains only sound inference rules, and if A |-R φ, then A |= φ.

theorem 4.1 (The Soundness Theorem for Propositional Logic)

不用反证法要证明 soundness 的话，要用类似递归（递推，数学归纳法）的方式，给定一个使得 assumption 为 true 的 model, 对于证明的一行，由于当前行使用的 inference rule 是 soundness, 因此本行的结论就是 True。

对比 valid(有效性) 和 sound(可靠性) 两个概念：

valid 是纯语法上的，它检查的是证明中每一步是否符合语法，即是否符合推理规则中的生成机制。如果证明中每个步骤都是 valid 的，那么整个证明对象 Proof 也是 valid 的。
sound 是纯语义上的，它检查的是推理规则中前提和结论与模型可满足性的关系。
如果证明中每一步使用的都是 sound 的推理规则，并且证明步骤是 valid 的，那么整个证明也是 sound 的。这是 soundness 定理，可以看到该定理实际有内在的 valid 要求。
由于逻辑系统包括语法和语义的定义，以及一组初始的推理规则（公理），因此如果公理都是 sound 的，那么整个逻辑系统也是 sound 的。
所以说，valid 可以修饰证明或者证明步骤，是纯语法的；sound 可以修饰推理规则、证明以及整个逻辑系统。 sound 修饰推理规则时，只涉及到语义描述，但修饰证明以及逻辑系统时，需要 valid 性质作为条件支持。

公式、公理和推理规则的异同

虽然大部分逻辑书或者数学书一般会把公理、定理看作是自明或被证明为真的公式，本书中，公理，定理，引理都属于推理规则 (InferenceRule 对象)，而不属于公式 (Formula)。

比如说 "(p->p)" 是一个 Formula，但如果要把它作为公理，那么应该包装成 InferenceRule 对象，这在书本里称为 I0 公理

I0 = InferenceRule([], Formula.parse('(p->p)'))

变成推理规则后，它实际不再是原来的"静态"的公式，而是一种接近函数的动态对象。在本文里，我有时候会用 "无条件地生成 p->p" 来描述这个推理规则。

推理规则还可以用符号替换（类比编程中宏替换）来转换成其他推理规则，比如以上 I0 还可以变成：

InferenceRule([], Formula.parse('(r->r)'))

这样，相当于我们又得到了一个新的公式生成机制，即 ”无条件地生成 r->r”，也就是说，推理规则即有函数的能力又像是个模版（宏）。

另外，通过这种生成规则生成的直接结果虽然是一个公式（字符串），但我们想得到的某些结论实际是通过推理获得引理或定理，它们仍然属于推理规则对象（InferenceRule）而不是 Formula，因为任何有意义的推理结果都是有前提假设的，公理也是 InferenceRule, 只是它们一般都是没有前提的推理规则（也可以有前提）。

比如说，有一个公式 q 作为假设, 同时有公理 I1, "可以从 q 产生 (p->q) ", 通过该规则，结合假设公式 q 我们能够得到公式 (p->q), 但实际真正得到的是： "可以从 q 产生 (p->q)" 这条新的推理规则，称为 theorem1, 如下：

assumption1 = Formula("q")

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

theorem1 = InferenceRule([assumption1], Formula.parse('(p->q)'))

为什么？这实际上是从逻辑设计者的视角下更合理地对公理或定理的解释。用一个例子来说明：

假设 A 是一个知识系统的设计者，现在 A 有了一套带有 MP 推理规则的命题系统，A 想要把外部世界的知识编码成命题逻辑，以实现自动推理。在 A 的世界里，有一条普遍规律，即如果下雨那么河水一定会上涨。那么 A 可以把它写成下雨->河水上涨，也可以用 p,q 分别表示两个事件，因此得到公式 p->q

从 A 的角度来看，这条规律可以看作这个世界的公理，因为它就是"公认的道理"
但如果 A 要把这个知识加入到命题逻辑系统，实际上，它无法将其写成无条件的 InferenceRule, 因为在逻辑的视角下，公理一定都是 sound 的，而 p->q 这个命题只有在 p q 为真，或 p 为假的模型下才正确，而不是在所有模型下都正确，因此它不是 sound.
所以 p->q 只能作为假设引入到这个系统，如果只有该假设，命题系统推导不出太多有意义的东西，但也能得到无数其他结论，比如
- (p->q|~(p->q)) 这种恒真公式（不需要 p->q 作为假设）。
- ~p|q 这不是一个很真的公式，但以下推理规则是 sound 的
```
InferenceRule([Formula.parse('(p->q)')], Formula.parse('(~p|q)'))
```
  这是一条逻辑上普世的定理，在任何承认 -> ~ | 的语义定义的世界都是 sound 的，而该系统之所以要列出这条定理，是因为 A 提供了 p->q 这个假设，逻辑系统以此说出了一条和它有关的定理， A 拿着这条定理可以在他的世界里去说一些所谓真理的东西。
现在假设 A 继续往这个系统里加入另外一条知识， p, 因为它观察到今天下雨了，它想看看下雨会导致什么，从而做一些提前预备工作。那么这个系统里有了 p 和 p->q 两个假设。命题逻辑系统可以以此给出另外一条恒真的定理（但仍然是推理规则，而不是命题）：
```
InferenceRule([Formula.parse('p'), Formula.parse('(p->q)')], Formula.parse('q'))
```
这仍然是一条逻辑上的普世定理，但对于 A 来说，在他的世界里，q 才是真正关心的一个命题，因此他可以将其称为（今天的）定理或引理等等。

这里例子实际展示了设计逻辑和运用逻辑的差别，设计逻辑时真正关心的是命题之间的关系的合理性，其设计的对象也就是这些关系，比如 ~,|,&,-> 都是用来表示关系的符号，逻辑设计者给这些符号设计了内在的语义，它们来自外部世界里抽象的真假性（不是具体事实发生的真假，而是根据排中律这种直觉写出 ~p|p 然后赋予这个公式为真，再根据矛盾律直觉写出 ~p&p, 然后赋予这个公式假，之后再细化出 ~,|,& 的内部语义），之后它们不断检查这些语义在更复杂的情况下是否仍然合理，比如是同时推导出 p 和 ~p （后文一致性的证明）。对于任何外部世界的事实或真理，它都是以假设的形式收纳进来，然后给出一些与这些假设相关的逻辑上 sound 的定理（推理规则），运用逻辑的人则拿这些定理去获得具体的公式，以此来更新它们对现实世界的认识。

radioLinkPopups

#rethink

如对本文有任何疑问，欢迎通过 github issue 或进行反馈

数理逻辑及其 python 实现:4

四、命题逻辑的演绎证明

T4.1 从推理规则中取出变量