数理逻辑及其 python 实现:5

T4.9 中提到，一个推理规则要在证明中被应用，往往需要先实例化，将其中的“形参”变成“实参”。

而另一方面，当我们从前提比如 ‘(p|q)’ 和 ‘(~p|r)’ 根据可靠的规则 R 证明出 ‘(q|r)’ 之后，我们其实得到了一个新的可靠的推理规则，即 InferenceRule(['(p|q)','(~p|r)'], '(q|r)'), 这条规则也能支持实例化，比如变成 InferenceRule([‘(x|p)’, ‘(~x|(y&z))’]， ‘(p|(y&z))') 这在日常证明中已经习以为常。

工程实现中，一种把引理变成推理规则的方法是对 class Line 中的 self.rule 类型放宽，它不单输入 InferenceRule ，也可以引用 Proof 中其他的 line 的编号，而 is_line_valid 函数需要能根据 line_number 把 line 解释成 InferenceRule 。

不过本文中并不是采用这种方式，而是一旦得到一个证明之后，可以把生成一个新的证明对象，该对象中的变量都替换成目标表达式。这种方式虽然低效，但实现上更简单，先根据前提和结论构造出替换表 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)

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

同样的，在证明中，如果已经证明了某个定理，那么可以直接用这个定理来作为推理规则（称为引理）进行证明，上节证明任何证明可以通过变量替换转成其他同构的证明，本节则证明引用这些同构证明是合法的（即可靠的）。

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

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

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

• 左上图 main_proof 的目标是通过前提 A 得到结论 d, 在证明的过程中，先得到了公式 b, 于是证明者心想，如果有 “由 b 能得到 d” 这条规则的话，就能直接得到 d 了，于是作者在证明中第二行 lines[2] 先引用一个假设存在的引理 R3, 该行内容为：

  rule = R3; formula=d; assumptions=[1]
  

• 然后证明者去证明引理 R3: “从 b 能得到 d”，右上图显示从当前逻辑系统里，可以从规则 C 和 R2，从 b 推导出 d 。由于 b 不是在前提假设 A 中的，因此它不是一个合法的从 A 得到 d 的证明，但它是一个合法的从前提 b 得到 d 的证明，我们将其记为 R3 。
• 下方图是把主证明中引理 R3 的虚拟使用替换成逐步证明的结果，它合并了两个证明

本题拆分成两个了任务： 5.2a 实现 _inline_proof_once，原理和上图是一样的。

对于更复杂的证明，可能有更多的 R3 结构，因此要依次替换，这是 5.2b 的任务。

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

• 根据 line_number 找到被替换行之前的行, 保持它们不被修改
• 对齐 lemma 证明和 main 证明过程中 specialization 的符号（需要把 lemma 证明里符号替换成主证明里符号）
• 对 line_number 之后的证明中引用到的编号加上偏置。

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)

这可以被翻译为合取三段论

前文就提到过 p->q 和推理的定义非常近似， 本节终于要认真讨论公式 p->q 和推理的关系了。

Let R be a set of inference rules that includes MP, let A be an arbitrary set of formulas, and let φ and ψ be two additional formulas. If A |-R ‘(φ→ψ)’, then A ∪ {φ} |-R ψ.

lemma 5.2

以上引理表明，由于 MP 推理规则的引入（用真值表方式很容易验证它是 sound 的），如果当前已经得到 "p->q" 这个公式，那么可以写出"给定 p 能推导出 q" 这个推理规则的证明

MP 推理规则像一个跨层次的连接者，它使得 p->q 静态公式可以当作推理规则来用。

下一节中的公理集中有许多带 -> 的公式，就是因为 MP 规则可以把推理规则编码成 -> 公式，比如我们不用说给定 p|q 可以推导 q|p 推理规则, ️而只要有一个无条件的 ((p|q)->(q|p)) 公式即可，结合 MP 自然能得到这条推理规则。

此外，由于第三章证明 ~ 和 -> 就已经可以构成完备的逻辑运算符集合了，因此 p|q 可以替换成 ~p->q，因此后文提到的某些公理集合（比如下一节里的）只包括 ~ 和 -> 符号。

本任务拆分成 prove_corollary 和 combine_proofs 两个函数

• prove_corollary 是通过 MP 规则来证明，如果我们已经证明了给定 z 可以得到 p, 同时又有一个无条件的推理规则 "p->q", 那么可以证明给定 z 可以得到 q

def prove_corollary(
    antecedent_proof: Proof, consequent: Formula, conditional: InferenceRule
) -> Proof:
    assert antecedent_proof.is_valid()
    assert InferenceRule(
        [], Formula("->", antecedent_proof.statement.conclusion, consequent)
    ).is_specialization_of(conditional)
    # Task 5.3a
    rules = antecedent_proof.rules | set([MP, conditional])
    assumptions = antecedent_proof.statement.assumptions
    statement = InferenceRule(assumptions, consequent)
    lines = list(antecedent_proof.lines)
    formula = Formula("->", antecedent_proof.statement.conclusion, consequent)
    lines.append(Proof.Line(formula, conditional, []))
    lines.append(Proof.Line(consequent, MP, [len(lines) - 2, len(lines) - 1]))
    return Proof(statement, rules, lines)

• combine_proofs 是通过 MP 规则来证明如果有一个无条件的 (a->(b->c)) 规则，以及对 a 和 b 的证明，那么可以得到对 c 的证明

def combine_proofs(
    antecedent1_proof: Proof,
    antecedent2_proof: Proof,
    consequent: Formula,
    double_conditional: InferenceRule,
) -> Proof:
    assert antecedent1_proof.is_valid()
    assert antecedent2_proof.is_valid()
    assert (
        antecedent1_proof.statement.assumptions
        == antecedent2_proof.statement.assumptions
    )
    assert antecedent1_proof.rules == antecedent2_proof.rules
    assert InferenceRule(
        [],
        Formula(
            "->",
            antecedent1_proof.statement.conclusion,
            Formula("->", antecedent2_proof.statement.conclusion, consequent),
        ),
    ).is_specialization_of(double_conditional)
    # Task 5.3b

    tmp_consequent = Formula(
        "->", antecedent2_proof.statement.conclusion, consequent
    )

    tmp_proof = prove_corollary(
        antecedent1_proof, tmp_consequent, double_conditional
    )

    assumptions = tmp_proof.statement.assumptions
    statement = InferenceRule(assumptions, consequent)
    lines = list(tmp_proof.lines)
    offset = len(lines)
    for line in antecedent2_proof.lines:
        if hasattr(line, "assumptions"):
            a = [i + offset for i in line.assumptions]
            lines.append(Proof.Line(line.formula, line.rule, a))
        else:
            lines.append(line)

    lines.append(Proof.Line(consequent, MP, [len(lines) - 1, offset - 1]))
    return Proof(statement, tmp_proof.rules, lines)

这些证明都是应用 MP 规则一次或多次而得到的。

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 的。

有了以上公理，证明思路如下：

• 由于我们不知道原始的根据 p 证明 q 过程中 p 是从哪一步才真正引入的，比如有可能证明第一步就用到了前提 p，而之后所有的证明都基于前一条, 那么 p 对所有公式都有影响。另一方面，有可能 p 只对最后结论有影响，因此只要替换最后一步，但识别 p 从哪一步开始有影响的是一个复杂的实践性工作，对于理论上的证明，宁可错杀也不放过，因此为了要消除前提 p 的影响，从证明第一行开始对每一行的结论公式 x 都转成 p->x 的形式，确保替换到第 i 步的时候，前 i 步都是不依赖前提 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)

2

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

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

func = lambda x:x+1\n

另一种角度看，这是目标语言和元描述语言的重叠，推理规则是在进行证明的人所使用的，而命题是逻辑系统里的元素，但 MP 使得这两个层次可以互相转换。

演绎定理带来的实践中的好处是，当我们要证明一个形式为 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 定理所认证的想象规则是人类更自然的思维方式，我们往往会先假设某个命题 p 成立，然后推导得到结论 q，于是我们说 p->q 这个命题本身是可以被证明的。

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

• 矛盾是根据语义定义的：某个公式如果在所有可能模型下的值都是 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. 系统能推导出 p 和 ~p 。
  2. 系统可以推导出无条件推理规则中结论部分的否定命题，例如 I1 的否定命题 ~(q->(p->q)), I0 的否定 ~(p->p)
  3. 系统可以推导出任意命题

它们都是一种语法上的现象。其中第 2 条是最强的，它实际包含了 1 2 两条，第 2 条也蕴含了第 1 条， 但 1 是否能推出 3 呢？ 这个问题的解答并不明显，以下函数就是为了证明 1 可以推导出 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
    )

X 系统：
I0: [] => ‘(p→p)’
I1: [] => ‘(q→(p→q))’
I2: [] => ‘(~p→(p→q))’
D:  [] =>  ‘((p→(q→r))→((p→q)→(p→r)))’
MP: [p, 'p->q'] => ‘q’

在没有任何假设情况下，由 MP,I0,I1, I2,D 四条推理规则组成的命题逻辑系统（简称 X 系统）是无矛盾的， 因为这些规则本身是可靠的，I0 I1 I2 和 D 是无条件推理规则，也可以看作公理，它们实例化出的任何命题语义上都是恒为真，而 MP 又是可靠的，因此继续推导出的任何命题也是真的，根据这种 soundness 就可以得到无矛盾的结论。

但如何证明 X 系统的一致性呢？ 在 哥德尔证明 (豆瓣) 第五章给出了命题逻辑系统一致性的绝对证明，其思路是把真假语义看作公式的标签，对于 X 系统，除了 MP 规则，无条件的推理规则 I0, I1, I2, D 的结论部分都是重言式，因此给它们打上“真”的标签。 根据 soundness 定理，所有根据这些规则得到的定理都是可靠的，因此所有推导出的公式都能打上 "真" 标签, 如果系统不一致，根据 I2 规则，不一致的三条性质是等价的，于是我们选择其中一个现象，即 X 系统能推导出任意公式，比如 (p&~p) ，它不是重言的因而不能打上 "真" 标签，这就和刚才的论证矛盾了，所以 X 系统是一致的。

以上我们用到了反证法，这是元层面的，而不是形式系统里的（下一节证明），这里的反证法必须是先验、绝对 的，或者经验上被大量使用但一直没被推翻，它无法被证明，否则会陷入不断递归地元证明困境中。

如果目前的公理集只有 I0: (p->p) 这一条推理规则，那么我们能得到的也就是诸如 p->p 、 q->q, (p->q)->(p->q) 等形式的公式，其多样性完全是替换规则在背后起作用的， 这些公式都是重言的，推导出的命题都可以打上“真”标签，这时假设它不一致，由于缺乏 I3, 我们不能说前文提到的不一致现象是等价，但无论选择任何一种定义不一致，都能得到一个不能打上 "真" 标签的命题，因此它还是一致的，然而我们会觉得这样的系统似乎没什么用。

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

上节我们用元层面的绝对反证法证明了装备 X 推理规则集合的命题逻辑的一致性，本节则证明反证法在命题逻辑系统内部是合理的。 有了这个结论就可以使用反证法这种快捷证明方式，就像 deduction 定理使得我们可以用更符合直觉的想象规则去先假设再证明一样。

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

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

1. A 本身就与公理集不一致，那么根据定义我们知道这个半挂系统本身就可以推导出任意命题，那么 f 也是其中之一，于是把 ~f 加入 A 之后，只要不去使用 ~f 就仍然能够推导出 f 。
2. 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 无法被证明。但这个论述的合法性需要在下一章中被论证。