数理逻辑及其 python 实现:5

Notes on 「Mathematical logic through python」

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

五、对"证明"的处理

T5.1 替换规则在证明中的 soundness

T4.9 中证明经过替换规则变换的推理规则是 sound 的，这里证明它对整个 proof 也是 sound 的。

以下函数给定一个证明，以及这个证明的结论命题的一个实例。比如原本证明的是 p|~p, 但我希望把结论拿过来改成 q|~q, 由于已经有了前者的证明，因此应用一次替换规则就可以得到后者而不需要重新手动证明，这里我们希望能够自动生成对 q|~q 的证明（Proof）对象，思路就是先构造出替换表 smap, 然后对每一行证明的公式都进行替换（不需要替换推理规则）。

def prove_specialization(proof: Proof, specialization: InferenceRule) -> Proof:
    assert proof.is_valid()
    assert specialization.is_specialization_of(proof.statement)
    # Task 5.1
    smap = proof.statement.specialization_map(specialization)
    lines = []
    for line in proof.lines:
        formula = line.formula.substitute_variables(smap)
        if line.rule:
            lines.append(Proof.Line(formula, line.rule, line.assumptions))
        else:
            lines.append(Proof.Line(formula))

    return Proof(specialization, proof.rules, lines)

Let R be a set of inference rules. Every specialization of every lemma that is provable via R is itself provable via R as well.

lemma 5.1 (Specialization Provability)

本节研究的是命题逻辑中 "证明" 对象的性质，也就是证明 "证明" 的性质，当用 python 去研究 Proof 时，实际就是操作 Proof 中的变量，例如 lines, statement 等，或者合并两个 proof 等等。

T5.2 Lemma theorem

第三章 T3.4 替换树中介绍到，可以把某个公式中的子公式替换成另外的公式，对应的就是在语法结构树 Formula 对象中对子树进行替换。

同样的，在证明中，如果已经有某人证明了某个定理，那么可以直接用这个定理来作为推理规则（称为引理）进行证明，本节就是证明这种引用是合法操作。

类比到编程语言中，本节实际是在实现编程中的"函数"机制，即一段代码可以被函数（函数名对应的就是引理名）封装起来，当其他人需要类似功能的时候，不需要复制整段代码，而只需要调用函数接口，而编译器或者解释器的实现中可能涉及到了入栈出栈操作来支持函数调用，本节就是实现这种背后的机制。

最终要实现 inline_proof(main_proof, lemma_proof) 函数。这个过程稍微复杂一点，因此画出以下示意图：

假设当前逻辑系统中有 A,C,R1,R2 四条规则（其中 A,C 是无条件的规则，因此看作为公理）

左上图对应的是 main_proof, 它证明的是，可以从当前逻辑系统里得到重言式 d, 或者说得到一个前提为空，结论为 d 的推理规则，它的 lines[2] 一行用到了引理 R3, 该行的结果是：
- rule = R3
- formula=d
- assumptions=[1]
右上图是对推理规则 R3 的证明，它说的是，在当前逻辑系统里，给定前提 b 可以推导出 d. 由于这个结论只用到了公理 C 和推理规则 R2, 因此 R3 可以认为是冗余的，被称为引理。
下图是把引理 R3 去掉后的证明，它实际只是替换了左上图中 line id 为 2 的行。

这里要注意的是引理实际是作为推理规则加入到 Proof 中的，另外，如果我们只考虑替换规则（并且考虑操作符的替换规则），那么本节的例子就好比 or 可以用 nand 来实现，因此在当前系统中可以不需要 or 操作。

本题拆分成两个了任务： 5.2a 实现 _inline_proof_once，这和上图是一样的，因为上图只替换了一次 R3, 对于更大的证明，其中可能有更多的 R3 结构，因此要依次替换，这是 5.2b 的任务。

从高层来看，引理替换某一行需要做哪些事情：

根据 line_number 找到被替换行之前的行 before, 这部分是不会变化的
对齐 lemma 证明和 main 证明过程中 specialization 的符号（需要把 lemma 证明里符号替换成主证明里符号）
对 line_number 后引用到的编号加上偏置。（类似汇编里 link 对地址进行处理）

def _inline_proof_once(main_proof: Proof, line_number: int,
                       lemma_proof: Proof) -> Proof:
    assert main_proof.is_valid()
    assert line_number < len(main_proof.lines)
    assert main_proof.lines[line_number].rule == lemma_proof.statement
    assert lemma_proof.is_valid()
    # Task 5.2a
    rules = main_proof.rules | lemma_proof.rules
    
    specified_rule = main_proof.rule_for_line(line_number)

    lemma_proof = prove_specialization(lemma_proof, specified_rule)

    before = list(main_proof.lines[:line_number])

    after = []
    offset = len(lemma_proof.lines) - 1
    for line in main_proof.lines[line_number + 1:]:
        if hasattr(line, "assumptions"):
            new_lines = []
            for i in line.assumptions:
                new_lines.append(offset + i if i >= line_number else i)
            after.append(Proof.Line(line.formula, line.rule, new_lines))
                                       
        else:
            after.append(line)

    replace = []
    for line in lemma_proof.lines:
        if hasattr(line, "assumptions"):
            replace.append(Proof.Line(line.formula, line.rule, 
                                       [line_number + i for i in line.assumptions]))
        elif line.formula in main_proof.statement.assumptions:
            replace.append(line)
        else:
            for i in main_proof.lines[line_number].assumptions:
                if main_proof.lines[i].formula == line.formula:
                    replace.append(main_proof.lines[i])

    return Proof(main_proof.statement, rules, before + replace + after)

有了以上替换一次，那么可以循环去发现整个证明中可替换的结构（需要从）：

def inline_proof(main_proof: Proof, lemma_proof: Proof) -> Proof:
    assert main_proof.is_valid()
    assert lemma_proof.is_valid()
    # Task 5.2b
    while True:
        line_number = len(main_proof.lines)
        for i in range(len(main_proof.lines)):
            if main_proof.lines[i].rule == lemma_proof.statement:
                line_number = i
                break
        if line_number < len(main_proof.lines):
            main_proof = _inline_proof_once(main_proof, i, lemma_proof)
        else:
            break
    return Proof(main_proof.statement,
                 main_proof.rules - {lemma_proof.statement},
                 main_proof.lines)

本题证明了"引理定理":

If an inference rule ρ is provable via a set of inference rules R ∪ {λ}, and if λ is provable via R, then ρ is provable via only the set R.

theorem 5.1 (The Lemma Theorem)

T5.4 公式和推理的统一： Deduction Theorem

remove_assumption

上一节 T5.3 说到，如果我们有 "p->q" 这个公式（或者无条件推理规则），只需要在假设里添加命题 p ，然后引用一次 MP 规则就可以得到命题 q, 这相当于获得了一个新的定理： "给定 p 能得到 q"。

本节实现的 remove_assumption 则是证明 T5.3 的反方向，即如果给定 p 能得到 q ，那么该系统可以（除原始公理外）无条件地得到公式 "p->q".

这里的核心在于 "无条件" 这个修饰词, 即证明 "p->q" 的时候，在假设或者公理集合中，不需要用到公式 p.

如果不是“无条件”的话，那么这个证明是很简单的，只需要在 MP 基础上引入一条新公理即可：

[] => ‘(q→(p→q))’

此时如果我们已经有了从 p 到 q 的证明，那么说明已经有了公式 q, 于是根据以上公理加 MP 就有了 (p->q), 证明就结束了。

问题就在于以上证明的前提里 p 必须存在, 因此以上得到的实际是推理规则： "给定 p 和 q 能得到 (p->q)"

这说明仅凭借以上一条公理还不够，需要引入更多公理。上一节提到，只需要 ~ 和 -> 符号就可以表示所有命题，而由于 -> 符号连接的命题可以根据 MP 直接转为推理规则，所以本节的公理中只包括 ~ 和 ->

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

注意以上设计的公理集合完全是人为选出来用于证明命题逻辑系统自身能力的（也就是 deduction Theorem 的），而不是用来方便做自动定理证明系统的，可以根据不同的目标选择不同的公理，只要这些公理是 sound 的。

可以把以上四条公理看作函数，但他们和编程语言里函数有区别，因为还需要替换字符串机制（类似宏），不过我们还是可以以以下形式写出

def I0():
    return sub("(p→p)")
def I1():
    return sub("(q→(p→q))")
def D():
    return sub("((p→(q→r))→((p→q)→(p→r)))")
def MP(p: "p", pq: "p->q"):
    return q

通过以上伪代码，想说明两点：

I0, I1, D 都是无参数函数，MP 是双参数函数，因此对于研究证明中每条公式的性质的时候，只需要考虑两种情况：该公式要么来自无参数公理（或者前提假设），要么依赖之前的两条公式。这和递归性质是相似的：要么来自没有前提的 basecase, 要么当前为题分解成更小的几个部分。
以上代码中 sub() 函数是一个模式识别的过程，它需要根据证明的上下文来决定替换规则，比如如果我们要证明 x->x, 那么调用 I0() 后应该能自动识别到关注的结果是与变量 x 相关的，因此将 "p->p" 替换成 "x->x" 后返回。

对于 MP 函数里 p: "p" 也是类似的，它表示的是变量 p 应该和输入的命题变量使用一样的符号。这个过程是没有"严肃地"形式化的，很多定理证明系统需要启发式地搜索如何替换，另外变量的替换也是一种 "类比" 能力。

接着考虑最终证明，其实现是一个类似递推型动态规划的算法，思路是：

由于我们不知道原始的根据 p 证明 q 过程中， p 是从哪一步才真正引入的，因此为了要消除前提 p 的影响，我们需要从证明第一行开始逐条进行转换，每条都保证把 p 彻底消除。比如有可能证明第一步就用到了前提 p，而之后所有的证明都基于前一条, 那么 p 对所有公式都有影响。另一方面，有可能 p 只对最后结论有影响，因此只要替换最后一步，但识别 p 从哪一步开始有影响的是一个复杂的实践性工作，对于理论上的证明，宁可错杀也不放过，对证明中每一行的结论公式 x 都转成 p->x 的形式，确保替换到第 i 步的时候，前 i 步都是不依赖前提 p 的，这样最后一次替换一定是我们想要的结果。
由于对推理规则参数的限制，证明每一行公式的来源只有以下几种，并列出各个来源下对 p 的消除方式：
- 要消除的假设 p 的实例化： p 是要删除的假设，因此我们必须处理掉它，用 I0 就可以直接得到 p->p, 这样就不依赖 p 了
- 除去 p 以外的假设的实例化公式 x：我们不能改变除 p 以外其他假设，因此我们至少要保留这份假设（的实例），但同时，由于当前的推理规则都是 -> 形式的，因此我们可以根据 I1 获得 p->x 形式的公式。
- I0,I1,D 结论的实例化公式 y：它们不依赖假设 p, 我们也不能随意改变公理，因此保持不变，但和上一种情况一样，我们需要 p->y 形式的公式作为之后推理可能需要的前提。
- 根据 MP 和其他两个前提公式 x 和 x->z 所推出来的结果公式 z: 注意由于我们已经按以上规则处理了当前行以前的所有公式，因此 MP 所依赖的两个公式的转换结果 p->x 和 p->(x->z) 是不依赖前提 p 的，这时候我们要做的是矫正当前行所以来的前提的下标，同时根据 p->x 和 p->(x->z) 来推出 p->z 借助规则 D 和两次 MP 可以证明。

实现示意图如下，每一行有三种可能情况，上方是转换前，下方是转换后

代码实现如下：

def remove_assumption(proof: Proof) -> Proof:
    assert proof.is_valid()
    assert len(proof.statement.assumptions) > 0
    for rule in proof.rules:
        assert rule == MP or len(rule.assumptions) == 0
    # Task 5.4
    lines = []
    start = proof.statement.assumptions[-1]

    rules = proof.rules | set([MP, I0, I1, D])
    assumptions = proof.statement.assumptions[:-1]
    line_num = 0
    old2new = {}
    for i, line in enumerate(proof.lines):
        new_formula = Formula("->", start, line.formula)
        if line.formula == start:
            lines.append(Proof.Line(new_formula, rule=I0, assumptions=[]))
            line_num += 1
        elif line.rule == MP:
            j, k = [old2new[x] for x in line.assumptions]
            pq, pqr = lines[j].formula, lines[k].formula
            pqpr = Formula("->", pq, new_formula)
            d_spec = Formula("->", pqr, pqpr)
            lines.append(Proof.Line(d_spec, rule=D, assumptions=[]))  # 0
            lines.append(
                Proof.Line(pqpr, rule=MP, assumptions=[k, line_num])
            )  # 1
            lines.append(
                Proof.Line(new_formula, rule=MP, assumptions=[j, line_num + 1])
            )  # 2
            line_num += 3
        else:  # line.formula in assumptions/specialization of assumptions:
            lines.append(line)
            i1_spec = Formula("->", line.formula, new_formula)
            lines.append(Proof.Line(i1_spec, rule=I1, assumptions=[]))
            lines.append(
                Proof.Line(
                    new_formula, rule=MP, assumptions=[line_num, line_num + 1]
                )
            )
            line_num += 3

        old2new[i] = line_num - 1
    statement = InferenceRule(assumptions, lines[-1].formula)
    return Proof(statement, rules, lines)

T5.3 和 T5.4 合起来证明了 Deduction Theorem for Propositional Logic, 它表明在某些 sound 的推理规则（MP,I1, D 等）的帮助下， p->q 这个公式与 p 到 q 的证明是等价的。

Let R be a set of inference rules that includes MP, I1, and D, and may additionally include only inference rules with no assumptions. Let A be an arbitrary set of formulas, and let φ and ψ be two additional formulas. Then A ∪ {φ} |-R ψ if and only if A |-R ‘(φ→ψ)’.

theorem 5.2 (The Deduction Theorem for Propositional Logic)

这有什么意义呢？一种角度是，它体现了静态和动态的转换，推理规则可以看作是函数是动态的，而命题则是静态的，本定理说明某些静态的公式和函数功能是类似的，只要背后还有一个非常"通用" 的解释规则 – MP.

从 "p->q" 命题可以推出推理规则 “由 p 能得到 q" 相当于编程语言中的以下代码，eval 对应了 MP 规则

func = eval("lambda x: x+1")
func(1)

反过来，从推理规则 “由 p 能得到 q" 可以推出 "p->q" 命题相当于自省：

import inspect
func = lambda x:x+1
inspect.getsource(func)

func = lambda x:x+1\n

最后思考：以上定理来自 I0, I1, D, MP, 如果没有这些公理，比如没有 MP, 似乎一切都做不了了，在没有 MP 和 I1 的情况下，如果 q 那么 p->q 可以被编码成 "(q→(p→q))" 吗？

T5.5 想象规则： Deduction Theorem 的快速应用

演绎定理带来的实践中的好处是，当我们要证明一个形式为 p->q 的公式时，可以先去假设 p, 然后给出 p 到 q 的证明，接着通过演绎定理就可以说已经证明了 p->q 。 T5.5 就给出了一个这样的例子

Assumptions: ‘(p→q)’, ‘(q→r)’;
Conclusion: ‘(p→r)’;

有了 deduction 规则，证明以上推理规则就方便很多了，只需要证明，给定 p 且 p->q ，q->r 那么可以得到 r, 这通过两次 MP 就够了，接着调用 remove_assumption 消除掉前提中的 p 就会得到结论 p->r ，且保留了前提 p->q 和 q->r.

def prove_hypothetical_syllogism() -> Proof:
    # Task 5.5
    p, q, r = Formula("p"), Formula("q"),  Formula("r")
    statement = InferenceRule(list(HS.assumptions) + [p], r)
    rules = set([MP, I0, I1, D])
    lines = [
        Proof.Line(p),
        Proof.Line(Formula.parse('(p->q)')),
        Proof.Line(q, rule=MP, assumptions=[0, 1]),
        Proof.Line(Formula.parse('(q->r)')),
        Proof.Line(r, rule=MP, assumptions=[2, 3])
    ]
    res = remove_assumption(Proof(statement, rules, lines))
    return res

这里我们先把 p 加入到假设中，在假设空间里，推理变得很简单，然后调用 remove_assumption 把 p 从假设去掉，得到 p->q, 有点像先进入复数空间旋转计算然后再回到实数的。有些地方把这种先假设再证明，最后得到一个 p->q 形式的重言命题的手段称为想象规则。

注意，deduction 定理以及想象规则使得我们更倾向于去讨论"假设" 以及 "假设空间", 假设空间是推理规则 InferenceRule 里的第一个属性，是一个 list, 其中每个元素都是一个 Formula 对象。尽管我们讨论的推理规则（包括公理、定理）都是 sound 的，或者无条件的公理中的 conlusion 都是恒真的，但假设（Formula）并不一定是恒真或者恒假，它是一个公式，比如 p 或者 p->q, 只有假设连通结论放在一起组成推理规则才要保持恒真。但可以把假设和公理放在一起讨论一种新的性质 – 一致性，这是下节要讨论的。

T5.6 命题逻辑的一致性

本节开始区分矛盾和一致性两个概念：

矛盾是根据语义定义的：某个公式如果在所有可能模型下的值都是 False, 那么它就是矛盾的，比如 p&q&r 不是矛盾的，因为存在一个使得该句子为真的模型 {p:True,q:True,r:True} 我们可以通过遍历指数级别的语义空间方式来判断是否矛盾，也就是判断命题是否是可满足的，但这是 NP 问题。

矛盾可以用来描述一个公式也可以描述一个形式系统（不单逻辑系统），因为对于一个没有任何假设的公理集，可以认为它拥有无数个模型，因为任何模型下这些公理都是 sound 的，我们正是以这个标准选出公理的，比如 I1 公理是 InferenceRule([], Formula.parse('(q->(p->q))')), 考虑只包括 p 和 q 的两个符号所组成的四个有限模型，这个公理的 conclusion 部分恒为真。

而向该逻辑系统加入某个假设句子，比如 p 时，可以认为系统不再是对所有模型都为真了，但它至少还有一个可满足的模型 {p:True}, 如果放宽对模型的的限制，可以包括更多不相关的符号，那么该系统在 {p:True, q:False, r: True}, 模型上也为真。

因此在 p 假设加入到命题逻辑系统后，这个系统并没有矛盾，它还是拥有一个（求值后为真的）模型。
一致性是通过语法词汇来定义的，它一般只描述整个（带有假设集的）逻辑系统。它可以有很多等价的定义：
1. 任何无条件公理中结论部分的否定命题，例如 I1 的否定命题 ~(q->(p->q)), I0 的否定 ~(p->p)
2. 可以同时推出某个命题 p 以及其否定 ~p
3. 可以推导出任意命题

它们都是一种语法上的现象。其中第三条是最强的，它实际包含了 1 2 两条，并且第 1 条实际也蕴含了第二条，但 2 是否能推出 3 呢？这个问题的解答并不明显，以下函数就是为了证明 2 可以推导出 3, 从而证明以上三条对于不一致的现象描述都是等价的。

如果光依靠前文提供的 MP,I0,I1,D 四条公理，实际不容易证明，因此作者给出了以下新的公理：

I2: [] => ‘(~p→(p→q))’

有了它之后，证明变得很简单，给定对 p 和对 ~p 的证明（假设相同，公理相同），在 ~p 和 I2 上应用 MP 可以得到 p->q, 再结合 p 应用一次 MP 就得到了 q, 而 q 可以是任意命题，使用 T5.3 里实现的 combine_proofs 可以一步到位

def prove_from_opposites(
    proof_of_affirmation: Proof, proof_of_negation: Proof, conclusion: Formula
) -> Proof:
    assert proof_of_affirmation.is_valid()
    assert proof_of_negation.is_valid()
    assert (
        proof_of_affirmation.statement.assumptions
        == proof_of_negation.statement.assumptions
    )
    assert (
        Formula("~", proof_of_affirmation.statement.conclusion)
        == proof_of_negation.statement.conclusion
    )
    assert proof_of_affirmation.rules == proof_of_negation.rules
    # Task 5.6
    return combine_proofs(
        proof_of_negation, proof_of_affirmation, conclusion, I2
    )

注意，我们还是在谈论语法的问题，但语法的变换规则–那些作为推理规则的公理–是通过语义筛选出来的，它们必须是可靠的，而在没有任何假设情况下，如果只有 MP,I0,I1,D 四条公理（简称 X 集），这个逻辑系统是无矛盾的，这通过语义上的可靠性检查就可以得到。

但它的一致性并没有那么明显，本书并没有给出 X 公理下命题逻辑系统的一致性证明，但在哥德尔证明 (豆瓣) 第五章给出了命题逻辑系统一致性的绝对证明，它思路其实是把语义看作符号的一种附带属性，真和假只是一种对当前命题（字符串）的类别标签，而对于希尔伯特公理（和 X 公理集等价的另一个公理集）下的逻辑系统，除了 MP 规则（这条规则是比较特殊的），那些无条件的推理规则的结论部分都是重言式（都会被划分到”真”这个类别）也就是在所有模型下都为 True, 而根据 soundness 定理，所有根据这些规则得到的定理都是可靠的，因此对于定理的结论部分，也就是推导得到的公式，在所有模型下也都是 True, 因此从该公理集合出发推导出的所有公式都是重言形式，如果这个系统本身不一致，那么根据 I2 规则，我们就能推导出任意公式，那么所有公式都应该是重言的，但我们能写出 p|q 就不是重言的，所以这个系统是一致的。

注意我们用到了反证法，而形式逻辑里反证法的有效性是下一节才证明的，这说明我们用的反证法必须是绝对的（或者经验上被大量使用但一直没被推翻），它无法被证明，否则会陷入不断递归地元证明困境中。

以上证明本质上是 soundness 的另外一种体现，它说明能被证明的都是重言公式，但它没有说所有重言公式都可以被证明。如果目前的公理集只有 (p->p) 这一条公理，那么我们能得到的也就是诸如 p->p 、 q->q, (p->q)->(p->q) 等形式的公式，其多样性完全是替换规则在背后起作用的，而这些公式都是重言的，在此公理集下的逻辑系统是一致的，然而我们会觉得这样的公理集似乎没什么用。

这就引出了完备性问题，我们希望这个公理集合足够强大，使得所有重言公式都可以被证明，这是第 6 章所讨论的问题。

然而我们要注意的是，在本书中，公理集包含的是一些推理规则，它们本质上操作字符串的规则，和替换规则是类似的，只不过替换规则被硬编码到了逻辑系统（或者一个逻辑机器）中，没有给用户多少可以定制的空间，而公理集的选择则是目前正在讨论的。

但在在其他逻辑书本里，公理集更多是以命题的形式来表述（本书里除了 MP 基本也都是无前提的规则，基本等同于命题，只不过可以进行变量替换），而推理规则则直接硬编码到了逻辑系统中（比如 MP 规则），此外，替换规则也是可以被讨论的，但这也许是在更深入的话题下，很可能涉及哲学。

当我们选定了一组一致的公理集合之后，基本就组装成了一个逻辑推理机器，如下图所示，

这时候我们关心的是输入某些关于外部事实的命题，比如关于下雨的自然规律的命题： ”下雨->河水上涨", 关于相关性的命题 "游泳人数增多->冰激凌销量增加", 这些知识作为假设集以半挂的形式添加到逻辑系统中，构成一个特定领域的推理系统。

现在有人想知道下雨会带来哪些潜在后果，于是输入了 "下雨" 这个事实，机器要能够解析该命题并应用推理规则得到结论，如 "河水上涨" ，假设集实际是关于某个外部世界的知识库。

一致性的证明里表达的是：即便假设集为空，这台逻辑机器运转起来也能输出大量的重言命题（在语义规则下的属于某个分类里的命题，这与现实真假无关）。

但之后的章节会更多去关注假设集中命题参与的情况下整个逻辑系统的性质。

T5.7 反证法的合理性

当我们想知道某个命题 f 是否能从逻辑系统生成时，可以将它的否定形式 ~f 加入到假设集中，然后看这个系统是否可能推导出某个已有命题的反面，如果是，这就导致 p 和 ~p 同时出现，即出现了不一致，这时候我们就可以声称命题 f 能够被系统所证明。

可以对以上条件进行放宽，即除了公理集外，假设集合 A 本身是非空的现在要证明 f 能够从公理集以及假设集 A 所证明，就可以把 ~f 放入集合 A 中得到扩充后假设集 A+，并说明 A+ 与公理系统不一致。注意这里包含两重情况：

A 本身就与公理集不一致，那么根据定义我们知道这个半挂系统本身就可以推导出任意命题，那么 f 也是其中之一，于是把 ~f 加入 A 之后，只要不去使用 ~f 就仍然能够推导出 f 。
A 与公理集是一致的，加入 ~f 后导致了系统不一致，这是本节所关心的问题。

本节要回答，为什么通过把命题的反面加入假设集从而构造不一致就可以下定论说 f 能够被证明？

代码实现的思路是，给定一个体现 A+ 系统下不一致的证明，我们能返回一个从 A 出发到 f 的证明。具体来说，由于上节已经用到了公理 I0, 并且知道各种一致性定义是等价的，因此可以把该公理结论公式的反面 ~(p->p) 作为反证法的终点，这样的话，只要给出一个从 A+ 集合作为前提的对 ~(p->p) 的证明，我们就能够返回从 A 出发到 f 的证明。

实现思路是：

~f 的加入导致 A 集合不一致，那么根据定义，我们就会有从 A+{~f} 到 ~(p->p) 的证明
根据演绎定理，可以直接得到在 A 假设集(去掉 ~f) 到 (~f->~(p->p)) 命题的证明
在逆否公理 N 的加持下可以得到 (p->p)->f 的证明，再利用一次 MP 就得到了 f 的证明。

也就是说，如 A+{~f} 是不一致的，那么我们能够从 A 证明出 f.

以下是具体实现，用到的公理有：

#: Modus ponens / implication elimination
MP = InferenceRule([Formula.parse('p'), Formula.parse('(p->q)')],
                   Formula.parse('q'))
#: Self implication
I0 = InferenceRule([], Formula.parse('(p->p)'))
#: Implication introduction (right)
I1 = InferenceRule([], Formula.parse('(q->(p->q))'))
#: Self-distribution of implication
D = InferenceRule([], Formula.parse('((p->(q->r))->((p->q)->(p->r)))'))

# Axiomatic inference rules for not (and implies)

#: Implication introduction (left)
I2 = InferenceRule([], Formula.parse('(~p->(p->q))'))
#: Converse contraposition
N = InferenceRule([], Formula.parse('((~q->~p)->(p->q))'))

函数参数 proof 是从任意公式的否定 ~x 到 ~(p->p) 的证明，要求函数返回对公式 x 的证明

如和 , 思路是：

既然有 ~x 到 ~(p->p) 的证明，根据演绎（deduction）定理，调用 remove_assumption 可以得到去掉 ~x 前提后对 (~x->~(p->p)) 命题的证明。
调用 prove_corollary 根据公理 N 和 MP 可以得到 (p->p)->x, 也就是 I0->x
根据 I0 和 MP 就得到了 x

def prove_by_way_of_contradiction(proof: Proof) -> Proof:
    assert proof.is_valid()
    assert proof.statement.conclusion == Formula.parse("~(p->p)")
    assert len(proof.statement.assumptions) > 0
    assert proof.statement.assumptions[-1].root == "~"
    for rule in proof.rules:
        assert rule == MP or len(rule.assumptions) == 0
    # Task 5.7
    f = proof.statement.assumptions[-1]  # ~formula
    proof = remove_assumption(proof)  # ~f->~(p->p)
    proof = prove_corollary(
        proof, Formula("->", Formula.parse("(p->p)"), f.first), N
    )

    n = len(proof.lines)
    lines = list(proof.lines)
    lines.append(Proof.Line(Formula.parse("(p->p)"), I0, []))
    lines.append(Proof.Line(f.first, MP, [n, n - 1]))
    statement = InferenceRule(proof.statement.assumptions, f.first)
    return Proof(statement, proof.rules, lines)

因此以上函数不单单证明了反证法的可靠性，还直接给出了完整证明过程，这来自于 deduction 定理和公理 N 的支持。

它回答了最初的问题：为什么通过把命题的反面加入假设集从而构造不一致就可以下定论说 f 能够被证明？

因此这里说明： A+ 的不一致性蕴含了命题 f 的可证明性的：

Let R be a set of inference rules that includes MP, I1, D, and N,4 and may additionally include only inference rules with no assumptions. Let A be an arbitrary set of formulas, and let φ be an additional formula. Then A ∪ {‘~φ’} is inconsistent with respect to R if and only if A |-R φ.

theorem 5.3 (Soundness of Proofs by Way of Contradiction)

注意以上是一个双向的等价性：

A+{~f} 系统是不一致的 <--> 能从 A 证明出 f

而以上代码证明只说明了从左到右这个方向，以下是从右到左的说明：

如果我们能从 A 证明到 f, 那么我们也能够用 A+{~f} 证明到 f （只要在证明中不使用 ~f 前提即可）
同样我们还能从 A+{~f} 证明到 ~f
因此我们同时证明了某个命题以及该命题的反面，根据一致性定义， A+ 假设集是不一致的。

这样我们就确立了双向的等价，而对于双向等价关系，对两边取反的话，也是双向等价：

A+{~f} 系统是一致的 <--> 不能从 A 证明出 f

这里论述了一个不可证明的性质，比如假设 A 是空集，我们知道纯逻辑公理下的系统只能证明出重言命题，因此 p|q 是无法被证明的，这时候我们就知道把 {~(p|q)} 作为假设集挂载到逻辑系统中后系统仍然是一致的。

但问题是，我们能否去检查某个假设集的一致性从而说明某个命题是不可证的呢？理论上是可行的，但前文中 X 公理集下的命题系统的一致性是通过重言性质来证明的，重言是一种非常强的全称性质的语义特点（在所有模型下，这个句子都被分类到了 "True" 这一类中），而某个非重言命题加入到假设集后，该逻辑系统推导的命题并非都是重言的，因此全称性失效了，这促使我们要去寻找另外的（也是语义相关的）特性 – 模型的存在性。我们想达到的是，加入 ~(p|q) 命题到假设集后，通过语义检查发现存在一个满足 ~(p|q) 为真的模型，那么我们就能声称 {~(p|q)} 不会导致不一致。从而可以声称 p|q 无法被证明。但这个论述的合法性需要在下一章中被论证。

radioLinkPopups

#rethink

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