数理逻辑及其 python 实现:12

Notes on 「Mathematical logic through python」

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

十二、谓词逻辑的语义完备性

完备性本身有两个方向，soundness 是其中的较为简单的方向，T9.9 重言命题有效性以及谓词逻辑的可靠性 已经给出了证明，另一个方向是从可蕴含可以推出可证明。在命题逻辑中，给定任何一个 sound 的推理规则，也就是假设命题集和结论命题，通过演绎定理构造出一个重言公式，如果该公式有 n 个变量（命题逻辑中的变量指的是不同的原子命题），那么可以构造出 k=2^n 个捕获集（前提集合），并且给出 k 条证明，尽管这些证明来自不同的前提集，但根据公理 R '((q->p)->((~q->p)->p))', 我们可以把互为否定的命题消除掉，由于重言命题中一定包含了每个命题的所有组合形态，因此所有捕获集里的命题都可以被消除，最终得到从空前提到该重言命题的证明。 这是一种 NP 复杂度的自动证明算法。

之所以可行，是因为命题逻辑的几个特点：

  • 假设集里包含了一切有限的基本命题，可以从这些命题里提取出所有变量
  • 命题逻辑的模型只是对这些原子命题的真值分配，因此模型是有限的，每个模型下都可以得到一个证明

然而，对于谓词逻辑：

  • 可能有无限多个对象，比如涉及自然数的命题，或者涉及所有直角
  • 假设集中有 R(c1,c2) 这种关系命题，也有 A(x)[P(x)] 这种带量词的命题

  • 尽管前文把函数和 = 关系消除了，模型里还是要用集合的形式对命题里出现的所有关系进行解释， 这种解释是真值的最终来源，比如关系 R 的解释如下： 

    {"R": (c1,c2),(c2,c3)}

    那么这意味着 R(c1,c2) 和 R(c2,c3) 这两个原子命题是真的，其他如 R(c1,c3) 则是假的， 我们通过某个对象是否存在于集合中来判断其真假。而对于不带量词的复合命题，比如 R(c1,c2)->R(c1,c3) 则可以根据逻辑运算规则来决定其真值，这与命题逻辑一样。不同之处在于， 谓词逻辑还可以用量词以及变量来对一些事实进行概括，例如 E(x)A(y)[R(x,y)] 是假的，因为并不存在一个对象 c ，使得所有 (c,y) 的组合都是真，但如果模型是： 

    {"R": (c1,c2),(c1,c3),(c1,c1)}

    那么 E(x)A(y)[R(x,y)] 就是真的，和命题逻辑类似，这里需要假设 R 中提及的所有对象就是整个模型里所存在的所有对象。

因此要能够模仿证明命题逻辑完备性的方式去证明谓词逻辑完备性，我们关注的对象首先应该是最"底层" 的原子性关系命题，如 R(c1,c2), 而量词的语义解释来自于这些命题。

尽管我们用 python 字典的方式去谈论模型，但对于命题逻辑系统来说，它看到的只有句子，所有关于模型的事实都被编码在句子中， 例如它看到的假设集是 {E(x)A(y)R(x,y)} ，结论命题是 R(c1,c2), 那么逻辑系统如何知道这个句子所对应的模型是什么？

命题逻辑中，如果给定前提 p, p->q 和结论 q, 我们限定其对应的模型只包含 p 、 q 两个变量。 对于谓词逻辑，我们也需要这种限制，比如由于以上句子只有一个二元关系 R，且只出现常量 c1,c2, 那么这些命题对应的模型应该只包括关系 R 以及 c1,c2, 从这个视角来看，我们也可以遍历所有的模型： 

def generate_relations():
    constants = ['c1', 'c2']
    possible_tuples = [(x, y) for x in constants for y in constants]

    # 总共有2^(2*2) = 16种可能的关系集合
    num_models = 2 ** (len(constants) ** 2)
    models = []

    for i in range(num_models):
        model = set()
        # 通过二进制数确定元组是否在关系中
        for j in range(len(possible_tuples)):
            if i & (1 << j):
                model.add(possible_tuples[j])
        models.append(model)
    
    return models

# 生成所有模型
models = generate_relations()

# 打印所有模型
for idx, model in enumerate(models):
    print(f"R in Model {idx + 1}: {model}")

R in Model 1: set()
R in Model 2: {('c1', 'c1')}
R in Model 3: {('c1', 'c2')}
R in Model 4: {('c1', 'c1'), ('c1', 'c2')}
R in Model 5: {('c2', 'c1')}
R in Model 6: {('c2', 'c1'), ('c1', 'c1')}
R in Model 7: {('c2', 'c1'), ('c1', 'c2')}
R in Model 8: {('c2', 'c1'), ('c1', 'c1'), ('c1', 'c2')}
R in Model 9: {('c2', 'c2')}
R in Model 10: {('c2', 'c2'), ('c1', 'c1')}
R in Model 11: {('c2', 'c2'), ('c1', 'c2')}
R in Model 12: {('c2', 'c2'), ('c1', 'c1'), ('c1', 'c2')}
R in Model 13: {('c2', 'c1'), ('c2', 'c2')}
R in Model 14: {('c2', 'c2'), ('c2', 'c1'), ('c1', 'c1')}
R in Model 15: {('c2', 'c1'), ('c2', 'c2'), ('c1', 'c2')}
R in Model 16: {('c2', 'c2'), ('c2', 'c1'), ('c1', 'c1'), ('c1', 'c2')}

根据这些模型，我们也可以构造出类似捕获集的命题集合： 

def generate_capturing_set(model):
    constants = ['c1', 'c2']
    possible_tuples = [(x, y) for x in constants for y in constants]
    
    # 初始化捕获集
    capturing_set = []
    
    # 检查每个可能的元组，确定是添加正命题还是负命题
    for tup in possible_tuples:
        if tup in model:
            capturing_set.append(f"R({tup[0]}, {tup[1]})")
        else:
            capturing_set.append(f"~R({tup[0]}, {tup[1]})")
    
    return capturing_set

# 示例：使用一个模型
R_example = {('c1', 'c2')}
capturing_set = generate_capturing_set(R_example)

# 打印捕获集合
print("Capturing Set for the model:\n", capturing_set)

Capturing Set for the model:
 ['~R(c1, c1)', 'R(c1, c2)', '~R(c2, c1)', '~R(c2, c2)']

那么我们是否可以根据任意的以上形式的捕获集去证明其他在该模型上为真的命题？比如 E(x)[R(c1,x)].

这看上去是可行的，因为捕获集已经描述了这个模型的所有信息，而结论命题只是对这些信息的一些筛选或者组合：

  • 筛选的例子是：证明 ~R(c2,c1)
  • 筛选加组合的例子是：证明 ~R(c2,c1)&R(c1,c2)
  • 或用量词这种更高的概括性组合：证明 E(x)[~R(c2,c1)&R(c1,x)]; 但在这种有限对象的语境下，量词实际只是对大量 & 和 | 的概括，就像是数学中 \( \sum,\prod \) 是对大量加法（对应 or）和乘法（对应 &）的概括一样。

但由于我们已经有了命题逻辑的重言定理，因此不需要用这种方式去构造捕获集，而只要能够根据前提命题，消除量词和变量，并写出足够完整的假设集合，只要结论能够被假设集所蕴含，那么直接就可以用重言定理一步得到证明。

比如说，给定 A(x)[~R(c2,x)] 以及 R(c1,c2), 要求证明 E(x)[R(x,c1)->R(x,c2)].

我们要做的更多是展开量词，对于全称命题，得到 ~R(c2,c1), ~R(c2,c1), 对于存在量词呢？一种做法是用 or 的形式展开，R(c1,c1)->R(c1,c2)|R(c2,c1)->R(c2,c2)

然后由于我们可以遍历所有模型，于是可以检查满足前提的模型是否也都满足结论，如果是，我们还需要对前提补充上所有出现过的关系，将其从 A(x)[~R(c2,x)] 以及 R(c1,c2) 变成： 

{~R(c2,c1), ~R(c2,c1), R(c1,c2), ~R(c1,c1)}

这些命题是没有量词和变量的，相当于回到了谓词逻辑 p,q,~r 的形式，然后用重言定理就得到了证明。

这种将带量词的前提命题以及不完整的关系解释命题展开并扩展成包括所有元素之间的所有关系描述的集合的思路是本章证明谓词逻辑完备性思路的一种不精确的概括，但总体上我们需要回答两个问题：

  • 要扩展成什么样的集合，才能够形成一个能够支持证明的尽可能完整的逻辑描述？ 这是 12.1 和 12.2 所回答的
  • 是否所有前提和结论组成的命题（我们可以通过演绎定理将其组合成一个命题）都能够扩展成这样的由大量 的类似命题逻辑中原子事实组成的命题集合？ 这是 12.4 到 12.7 所回答的
  • 如果模型中对象有无限多个，如何处理？这是紧致性定理所回答的。

后文的证明中，我们也不是去证明可蕴含意味着可证明，而是通过完备性的另外一个等价关系来证明： 

证明出 ~(p->p) <--> S 系统是不一致的 <--> S 系统没有模型

即，对于给定的公式集合，先检查它是否一致，如果一致，则返回一个模型，否则给出对 ~(p->p) 的证明。 但在 T5.6 命题逻辑的一致性 中我们谈到，一致性的证明并不简单，因为要证明一致性，就要说明从该系统出发 无法证明出 ~(p->p), 这种否定性描述很可能使得证明机器陷入不停机状态， 所以我们才要通过语义矛盾和形式矛盾的等价性来获得对一致性更好的检查方法，给定一个公式集合，我们只需要检查这个公式集合不是恒为假就知道该公式集合是一致的，对于谓词逻辑中完全展开成基础关系命题的假设集，命题逻辑的完备性是可以直接拿来使用的，因此我们可以直接用命题逻辑的方式来检查集合里基础命题的语义，从而判断其是否 一致。如果一致，我们就去构造一个谓词逻辑的模型，如果不一致，则用命题逻辑的演绎定理构造出 ~(p->p) 形式矛盾语句（只不过这里的 p 是类似 R(c1,c2) 的基础关系命题）

因此这里我们核心要说明的就是，谓词逻辑里的量词命题和那个展开的基础命题集是等价的（或者是一致的）

T12.1 句子集合的封闭性

is_closed

前文说到，在一个原子命题（或称为基本命题）足够完善的集合下，，我们是

Let S be a (possibly infinite) set of sentences in prenex normal form. We say that S is closed if all of the following hold:

  • S is primitively closed: For every relation name R that appears somewhere in S and for every tuple of (not necessarily distinct) constant names (c1, . . . , cn) where n is the arity of R and each ci appears somewhere in S, either the primitive sentence ‘R(c1,. . . ,cn)’ or its negation ‘~R(c1,. . . ,cn)’ (or both) is in S.•
  • S is universally closed: For every universally quantified sentence ‘∀x[φ(x)]’ in S and every constant name c that appears somewhere in S, the universal instantiation ‘φ(c)’ is also in S.
  • S is existentially closed: For every existentially quantified sentence ‘∃x[φ(x)]’ in S, there exists a constant name c such that the existential witness ‘φ(c)’ is also in S.

definition 12.1 (Closed Set of Sentences; Primitively Closed Set of Sentences; Universally Closed Set of Sentences; Existentially Closed Set of Sentences)

这里描述的封闭性在代码实现上只适用于有限对象的模型。对于自然数，模型中如果不使用后继函数而只有关系的话，只能用无限的常量来表示所有自然数对象，理论上可以存在一个包含无限可数的句子的集合，其中描述了所有自然数之间的一元关系和二元关系（就像有理数对一样）等等。

T12.2 封闭集下矛盾的精确可追溯性

find_unsatisfied_quantifier_free_sentence

本节以及 T12.3 一同证明如下引理：

Let S be a (possibly infinite) closed set of sentences in prenex normal form. If S is consistent, then S has a model.

lemma 12.1 (Completeness for Closed Sets)

回顾命题逻辑里类似定理是如何证明的，即如果命题逻辑里某个假设集合 A 和逻辑公理系统是一致的，那么 A 会有一个模型。这个证明来自于其反面等价性的证明，即 A 不一致和 A 没有模型两者是等价的，这实际是命题逻辑的完备性定理， 我们没有直接证明一致性到可满足性这个方向，但我们证明了其题否命题，即如果 A 没有对应模型，那么 A 是不一致的。

T12.2 是整个证明的第一步，它证明的是如下引理：

Let S be a (possibly infinite) universally and existentially closed set of sentences in prenex normal form. If S is not satisfied by some model M, then there exists a quantifier-free sentence in S that is not satisfied by M.

lemma 12.2

这里我们只针对全称封闭和存在封闭， 而暂时不考虑原子封闭, 这两种封闭意味着，对于集合中的任何全称量化句子 \( \forall x[\phi(x)] \)，集合 S 中也包含所有形如 \( \phi(c) \) 的实例，其中 \( c \) 是任意出现在 \( S \) 中的常数。对于存在量化句子 \( \exists x[\phi(x)] \)，则存在某个常数 \( c \)，使得 \( \phi(c) \) 也在 \( S \) 中。

如果模型 M 不满足 S ，意味着至少有一个句子在 M 下为假。由于 \( S \) 的封闭性，所有的量化已经被展开为对所有可能常数的具体断言（即量化语句在这里是多余的）。因此，如果 S 有任何量化句子不被满足，一定可以 具体追溯到某个无量词句子。这个句子直接表达了某个关系在模型 M 中是不成立的。

本题实现中，给定一个句子集合 S, 一个不满足 S 的模型以及不满足模型的句子 f （可能是包含量词的） ，要求找到句子 S 中哪个具体的导致模型不满足的无量词句子 \( \phi(c) \) 。

由于 f 可能包含量词，于是我们不能直接返回 f, 也就是说，如果 f 不是带有量词的，直接返回它就可以了，因为它在前提中已经说了是来自集合 S 中。但题目要求是我们不能用 for 循环去遍历句子集合，否则每次调用 model.evaluate_formula(sentence) 检查哪个不符合然后删除就可以了

而如果 f 是一个 E(x)[P(x)] 形式的句子, 那么根据存在封闭性，其中一定包含一个表示个例的句子 P(c) ，显然这个存在性命题是不满足模型的，但我们不知道具体是哪个常量 c, 一种做法就是直接遍历所有常量，构造出 P(c), 然后去检查 P(c) 是否满足模型。

如果是 A(x)[P(x)] 形式的句子，那么根据全称封闭性，所有常量 c 构成的 P(c) 语句都存在于其中。 可能其中有某些是不符合的，这时候和检查存在量词类似，构造出所有 P(c) 句子，但不需要去判断它是否在 S 中，而是直接检查句子是否满足模型，如果不满足直接返回。

f 是否有可能是 A(x)A(y)[P(x,y)] 形式？这是显然的，对于二元关系就必须有这种语句。

f 是否会出现 E(x)A(y)[P(x,y)] 情况？也是可能的，因此这里算法的核心就是去不断消解掉 f 的量词塔，注意拿掉一层量词后可能变成 A(y)[P(c,y)], 根据存在封闭性，这个命题也必须出现在 S 集合中。因此具体算法是：

  • 如果 f 是 A(x) 量词开头，例如 A(x)A(y)[P(x,y)]，那么遍历所有常量构造出 A(y)P(c,y) 形式的命题，这些命题都会在 S 中，用它们分别计算模型的结果，如果不满足，则递归调用，将 A(y)P(c,y) 作为 f
  • 如果 f 是 E(x) 量词开头，例如 E(x)A(y)[P(x,y)]，那么遍历所有常量构造出 A(y)P(c,y) 形式的命题，这些命题只有部分在 S 中，找出在 S 中并不满足模型的句子，则递归调用，将 A(y)P(c,y) 作为 f.

因此本节总体就是说明，在某种封闭的句子集合下，如果假设不符合某个模型，就一定能精确追溯到具体的 导致模型失效的某个命题。

在命题逻辑中，如果有一个假设句子集合，例如 p,q 违背了某个模型，比如 {p:True, q:False}, 那么我们同样能找到一个具体违反该模型的句子，这里是 q.

这是因为实际句子集里的每个句子之间是一种并列关系，类似 p&q, 如果 p&q 在模型上为假，那么一定是某个 & 的分支为假，从而可以去各个分支里定位，谓词逻辑中，额外的就是假设里会出现如 E(x)A(y)[P(x,y)] 形式的带量词的句子，这些句子更像是对 and 和 or 的概括（A 对应 and, E 对应 or），但由于封闭性，这种句子已经被拆分到了具体的无量词命题上，于是我们同样能定位到具体的导致错误的简单无量词句子。

T12.3 封闭假设集下的完备性

model_or_inconsistency

Let S be a (possibly infinite) closed set of sentences in prenex normal form. If S is consistent, then S has a model.

lemma 12.1 (Completeness for Closed Sets)

这里最终证明在满足封闭性条件下的假设集合的完备性，即如果这个假设集合存在一个模型，那么就构造出一个模型，如果不存在模型，我们可以通过无量词的基本命题集合推导出一个形式矛盾的句子，从而说明它们是不一致的。

这和 T6.5 一致性（语法上）与完备性（语义到语法）的关系 要实现的函数名是一样的。

之所以能够构造谓词逻辑模型，是因为假设集中包含了所有基本关系命题，如果句子中包括 R(c1,c2)，那么模型的关系 R 中就会有 (c1,c2), 如果句子中有 ~R(c1,c1), 模型的关系 R 中就不能出现 (c1,c1) ， 假设集已经刻画出了模型的面貌。

如果通过这种方式构造出来的模型仍然不满足句子集合，那么句子中肯定有类似 ~R(c1,c2) 或者 R(c1,c1) 或者基于它的复合句子，通过 T12.2 我们可以精确追溯到不满足模型的无量词句子，记为 C， 这个句子（可能是复合也可能是基本句子）一定会与那些基本句子不一致（因为模型是依靠基本句子构造的）， 所以只要把基本句子都选出来与 C 组合，那么它一定能推导出某个基本句子的矛盾形式，比如 ~R(c1,c2). 由于这些基本句子以及无量词句子 C 实际都是命题逻辑句子，因此可以直接引用重言推理公理。

这段话解释了以下引理：

Let φ be a quantifier-free sentence, let p1, . . . , pn be its primitive subformulas, and let S be a set of formulas that for every i = 1, . . . , n contains either the primitive sentence pi or its negation ‘~ pi’. Denote by S' the set of these primitive or negated-primitive sentences that are in S. If φ evaluates to False in some model of S' , then S' ∪ {φ} is inconsistent.

lemma 12.3

对所有谓词逻辑命题集进行封闭

前三节已经证明封闭假设集下谓词逻辑的完备性，目前我们要说明的就是，所有的谓词逻辑句子集都可以转换为封闭 集。

对于给定的任意句子集 S, 要转换成封闭句子集 C, 根据定义，封闭句子集一定是 S 的超集，因为它是在 S 的基础上选出 S 中的量词并且展开后去扩充集合 S.

但除此之外，我们要说明，转换过后 S 和 C 是一致的，也就是是说 A 如果是一致的，那么扩充后的 C 也是一致的，从 T12.4 到 T12.7 将用证明以下引理：

For every (possibly infinite) consistent set of sentences in prenex normal form S, there exists a closed consistent superset of sentences in prenex normal form S¯ ⊇ S.

lemma 12.4 (Consistency-Preserving Closure)

T12.4 将一般假设集转为原始命题封闭集

combine_contradictions

本节目标是用代码证明，向 S 中加入所有的原始关系句子，即形如 R(c1,c2) 或 ~R(c1,c1) 的所有关系和模型对象的组合的句子后，得到的第一个扩展集合 C1 与原始集合 S 是一致的。

注意还要重复一遍，一致性的语法检查是比较困难的，因为它是否定性描述，如果对于任何命题我们能有简单的方法检查它是否一致，那么给定任何一个新的数学公式，加入到现有数学公理中，就能知道这个数学公式是真是假了。

因此我们先证明一个理论上的论述：

Let S be a (possibly infinite) consistent set of sentences. For every sentence φ, either S ∪ {φ} is consistent or S ∪ {‘~ φ’} is consistent (or both).

lemma 12.5

也就是说对于任何命题 f, 如果 f 加入原始命题集合 S 导致命题不一致，那么 ~f 加入 S 一定是一致的，反之亦如此。不可能出现 f 或者 ~f 加入到 S 都会导致不一致的情况（但同时把 f 和 ~f 加入到 S 肯定导致不一致，因为 f 和 ~f 本身就是不一致）。这说明，从理论上，对于给定任何原始命题 p, 在保持一致的情况下，我们要么可以把 p 加入到 S, 要么可以把 ~p 加入到 S, 最终所有原始命题或其否定都可以加入到 S 从而达到原始命题封闭集 C.

combine_contradictions 是给定对同一个矛盾命题 X 的两个证明，第一个证明的前提是 S+{p}, 第二个证明前提是 S+{~p} 要求合并成一个从 S 到 X 的证明。这说明的是，如果 S+{p} 和 S+{~p} 都不一致，那么只有可能 S 是不一致的。

实现思路是：根据演绎定理，可以得到从 S 到 (~p->X) 的证明，也可以得到 S 到 (p->X) 的证明，根据重言蕴含， (~p->X) 和 (p->X) 可以证明出 X

因此本文我们没有实现如何扩充原始命题封闭集的算法，但我们说明了对任何集合 S 存在一个包含它的更大的与之保持一致的原始命题封闭集。

T12.5 假设集转为全称封闭集的理论证明

eliminate_universal_instantiation_assumption

上节说明了扩充原始命题集的可行性，本节是扩充全称封闭集，这实际更为简单，例如给定 A(x)[R(x)], 我们只需要遍历所有对象 c 构造出 R(c) 即可，并且很容易说明 R(c) 不会与 A(x)[R(x)] 不一致，因为有 UI 公理。

和 T12.4 类似，我们先说明其理论上的可行性，即如果 R(c) 与 A(x)[R(x)] 的组合导致了不一致，那么说明 A(x)[R(x)] 已经导致了不一致

Let S be a (possibly infinite) consistent set of sentences. For every uni- versally quantified sentence ‘∀x[φ(x)]’ ∈ S and every constant name c, we have that S ∪ {‘φ(c)’} is consistent.

lemma 12.6

T12.6 一般假设集转为全称封闭集的实现

universal_closure_step

但和 T12.4 不同，我们可以直接给出扩充算法，我们需要对所有的量词命题不断地去量词化， 注意这里尤其要处理嵌套量词，比如 A(x)A(y)[P(x,y)] 需要进行多次展开

不过我们目前只实现最外层的展开： universal_closure_step, 之后只要调用该函数不断迭代直到没有量词即可（尽管这很低效）。

T12.7 一般假设集转为存在封闭集的可行性

eliminate_existential_witness_assumption

为了将 E(x)[R(x)] 无量词化，我们需要选择一个假想的使得 E(x)[R(x)] 存在的常量 c, 并将 R(c) 加入到假设集中，这个 c 一般称为证人常量 (witnessing constant), 或者 Henkin 常项，而这种从存在量词到 Henkin 常量的操作叫作 Skolemization ，但本书的公理系统中没有引入该变换规则。

另外，哥德尔是第一个证明谓词逻辑完备性的人，但由于 Hekin 给出了更简洁的证明， 因此本书介绍的是 Henkin 的证明方法。

和前文一样，我们先证明其可行性，也就是说，一定能找到一个这样的 c 使得 R(c) 加入之后 E(x)[R(x)] 仍然一致，反过来如果出现不一致，那么就是原本 E(x)[R(x)] 已经不一致。

因此给定 {R(c), E(x)[R(x)]} 到一个矛盾命题的证明，返回从 E(x)[R(x)] 到矛盾命题的证明。

现在我们假定 R(c) 中 c 就是那个使得 R(c) 为真的常量，如何只通过句法操作从证明中"删除"掉 R(c) 以证明没有 R(c), 只要 E(x)[R(x)] 就能够证明到矛盾结论？

这里的做法是直接把 R(c) 中常量替换成证明中没有出现过的变量，比如替换成 R(zz), 然后会发现，这个证明中没有了 R(c), 但整个证明还是合理的，这是因为：

  • 替换后，证明中的命题逻辑结构不变，即每一行的命题骨架保持不变。因此，如果原证明中的某行是重言式（tautology），则替换后仍然是重言式，比如 R(c)->R(c)|P(c1) 替换后变成 R(zz)->R(zz)|P(c1)。
  • 任何使用肯定前件法（Modus Ponens, MP）的推理步骤仍然有效，因为在涉及的三个公式（两个前提和一个结论）中都进行了相同的替换。
  • 所有使用全称量词引入（Universal Generalization, UG）的步骤也保持有效，因为替换操作没有改变变量的性质，且在相关公式中执行了相同的替换。
  • 任何由假设或公理直接支持的公式仍然是合法的实例，因为替换也在这些假设/公理及其实例化中执行。

因此我们把 R(c) 这个具体命题变成全称命题 R(zz) 后还是能证明出矛盾命题，这说明不是 R(c) 导致的问题

这个证明一眼看上去不太合理，然而检查每一步似乎无话可说，这很大程度是公理集设计导致，如果公理集中有 Skolemization 变换，那么就要用另外的方式来证明了。

技术上，这里涉及一个修改 Proof.Line 对象的问题，但是 Line 对象是 frozen 的，因此需要理清如何把 Line 对象中涉及 R(c) 的变成一个新的 R(zz)

要考虑对以下四种 line 分别进行重建 

AssumptionLine, MPLine, UGLine, TautologyLine

AssumptionLine 包括

  • formula: Formula
  • assumption: Schema
  • instantiation_map: InstantiationMap

MPLine 包括

  • formula: Formula
  • antecedent_line_number: int
  • conditional_line_number: int

UGLine 包括

  • formula: Formula
  • nonquantified_line_number: int

TautologyLine 包括

  • formula: Formula

对于后三个，都是取出原 Line 对象中 formula 替换或重新组装，其他属性不变。 对于 AssumptionLine, 需要替换其中 InstantiationMap, 将其中出现的变量 Term 替换成 Term("zz")

如何判断 Line 的类型呢？在第 11 章证明演绎定理时同样要判断类型，判断方式为： 

isinstance(line, Proof.AssumptionLine)

返回的 Proof 前提里的 R(c) 与需要替换

本题证明了以下引理：

Let S be a (possibly infinite) consistent set of sentences. For every existen- tially quantified sentence ‘∃x[φ(x)]’ ∈ S and new constant name c that does not appear anywhere in S, we have that S ∪ {‘φ(c)’} is consistent.

lemma 12.7

注意这个结论里引入的是不在 S 中的常量，它可以是一个假想的扩充模型的对象。

这里的核心在于，存在命题在证明中本身无法定位到任何真实的 witness, 即便句子集合里中已经有了 某个具体的 R(c) 或 R(a) 命题，但 E(x)[R(x)] 仍然无法对 R(c) R(a) 提供什么新的信息（反过来也一样）， 它只能用来证明一些"宽泛"的命题。因此我们可以用宽泛的某个常量来替代它。

我们引入的新的 witness, 比如 R(cc), 它永远也不会出现在证明结论中。

T12.8 一般假设集转为存在封闭集的实现

接着我们实现通向存在封闭集的扩展算法，这里我们只需要找到存在量词语句，然后用一个不在句子中的常量去替换该量词变量

radioLinkPopups
#rethink
如对本文有任何疑问，欢迎通过 github issue 或邮件 metaescape at foxmail dot com 进行反馈