数理逻辑及其 python 实现:8

replace_functions_with_relations_in_model(model)

model 中的函数关系非常直接，实现上它就是一个字典：

function_interpretations = {
            "f": {("a",): "b", ("b",): "b"},
            "gg": {
                ("a", "a"): "b",
                ("a", "b"): "a",
                ("b", "a"): "a",
                ("b", "b"): "b",
            },
        },

以上表示 f(a)=b, f(b)=b, gg(a,a)=b, gg(a,b)=a, gg(b,a)=a, gg(b,b)=b 。

而关系则是集合，以下是把 gg 函数专为 Gg 关系后的写法：

relation_interpretations["Gg"] == {
        ("b", "a", "a"),
        ("a", "a", "b"),
        ("a", "b", "a"),
        ("b", "b", "b"),
    }

具体方法就是把函数里的 key value 合并。这里可以看到，关系是用集合来表示的，它的有效性来自于集合论的支撑。

如果一个模型没有函数，那么它的组成部分中 – 对象集合、常量映射、关系中，除了常量还是一种字典或者类似函数的形式（或许也能写成关系或集合形式），其他都可以用集合来表示，因此集合论是构建模型的更底层理论。

model = Model(
    {"a", "b"},
    {"a": "a"},
    {"GT": {("b", "a")}},
)

replace_relations_with_functions_in_model(model, original_functions)

现在考虑相反的问题，把关系转为函数，该函数可能没有具体的应用场景，但它至少可以引发一点思考：

• 关系是一个比函数更一般的概念，比如可以描述一对多，因此如果要进行无损转换，至少原始模型中不会出类似以下形式的关系

  F={(1,2),(2,2)}
  

  因为强行将其转换后，根据转换顺序，结果可以是

  f ={2:1}
  

  也可以是

  f ={2:2}
  

• 此外，由于是集合，那么它可以不对模型中的某些元素声明关系。正如以上例子，即便强行转换成了函数 f, 我们发现 f 中没有 1 作为输入的情况，这导致 f 是一个偏函数，而一旦出现 A(x)[f(x)=1] 的语句，它将会变成在语义上未定义，就好比 1/0 一样。
• 我们为什么要把关系又转为函数呢？彻底消除关系是不可能的，因为关系是把 Term 变成真值表达式的桥梁。

_compile_term

文中给出的例子是：

f(g1(g2(0)),h(x))’, 转成一系列公式： ‘z1=g2(0)’, ‘z2=g1(z1)’, ‘z3=h(x)’, and ‘z4=f(z2,z3)’

这与编译过程类似， 比如说，以下 C 语言的函数求值语句：

int result = func1(func2(5, func3(3)), 4);

编译器可能会将其拆分为：

int temp1 = func3(3);
int temp2 = func2(5, temp1);
int result = func1(temp2, 4);

这使得每个语句变得简单，转成机器码更加容易。而之所以二者会类似，是因为一阶逻辑里引入的函数关系和编程中的函数几乎就是同样的东西。

replace_functions_with_relations_in_formula  

现在将某个公式中的关系进行替换，先考虑相对简单的例子： A(x)f(x)=1

注意这里之所以说它是简单的，是因为 "=" 符号是作为语法糖预设好的，它是模型提供的，因此以上表达中，真正由模型提供的只有 f 和 1 两个符号（都是字符串），它比较的是两组符号，而不是对象本身，但 = 的语义规定了如果两个符号相等，它意味着在 model 空间中，这两个符号所映射的对象是同一个对象。我们在后文还会讨论 = 关系。

回到 A(x)f(x)=1, 它的语义是，对于所有 x, f(x) 都等于 1 。 我们假设其模型中只有两个对象，因此原本模型里有函数 f(o1)=1, f(o2)=1, 之后的模型中 f 被替换成了关系 F={(1,o1),(1,o2)} ，那么我们在语义层面应该如何等价地描述？

我们可以说，对于所有 x, F(1,x) 都成立，也就是说 A(x)F(1,x), 注意这是通过语义直接获得的结果。我们根本没有引入一个中间变量 z. 同时我们还顺带消除了 = 关系。

如果原始命题是存在命题， E(x)f(x)=1, 那么等价的翻译就是 E(x)F(1,x), 这也完全没有用到中间变量 z. 如果命题是 f(o1)=1, 那么可以转为 F(1, o1) 。

以上过程的启示和延伸：

• 量词是否存在或者量词是什么可能并不影响量词所修饰的词项内的替换，原本是什么量词，替换后还应该是什么。
• 这种直接通过语义进行转换的思想，对于简单例子是可行的，但考虑更复杂情况： f(g(x))=1, 直接根据语义去消除函数和等号是比较复杂的。

• 可以顺带消除等号，但这可能过于激进，会导致混乱，我们可以引入额外变量 z, 把 f(o1)=1 写成 z=1&F(z,o1) 之所以前文消除了等号，是默认用上了 = 的可替换性，如果 a=b, 且有 F(a, x) 那么也会有 F(b,x).

  z=1&F(z,o1) 并不是一个有真值的公式，因为其中 z 是自由变量，为了将其变成有真值形态，需要加上量词，这里只有 A 和 E 可选，但是 A 会导致明显的语义错误，因为并不是所有对象都满足 F(z,o1) 或者 z=1, 而只有 1 满足。 因此继续检查存在量词 E(z)[z=1&F(z,o1)] ，它说的是存在某个对象，它等于 1 ，并且满足 F(z,o1), 这看上去是合理的。

现在回到更为复杂的例子 f(g(x))=1,这里先抛弃量词，之后再考虑各种量词下的语义，假设我们只消除最外层函数：

• 先引入 z1 满足 f(g(x))=z1, 然后写成 E(z1)[F(z1,g(x))&z1=1]
• 现在考虑把量词加回到 f(g(x))=1, 如果是 A(x)[f(g(x))=1], 那么以上转换结果是写成：
  • A(x)[E(z1)[F(z1,g(x))&z1=1]] 还是

  • E(z1)[A(x)[F(z1,g(x))&z1=1]] ？

    注意交换 A 和 E 的语义很可能是不同的，第一个公式的解释是，对于所有 x 都存在一个 z1, 满足 f(g(x))=z1=1 第二个公式的解释是，存在一个 z1 使得所有 x 都满足 f(g(x))=z1=1 在等于的场景下似乎没有区别，但如果把 f(g(x))>1, 那么两个解释变成

    • 对于所有 x 都存在一个 z1, 满足 f(g(x))=z1>1

      这里有可能 o1 对应了 2, o2 对应了 3, 因此 f(g(o1))=2>1, f(g(o2))=3>1

    • 存在一个 z1 使得所有 x 都满足 f(g(x))=z1>1

      这里 z1 是唯一的，比如都是 2，因此 f(g(o1))=2>1, f(g(o2))=2>1

    因此场景一在语义上是覆盖场景二的，它的内涵更广，而原始的语义是对所有 x, f(g(x))>1, 那么它没有约束不同 f(g(x)) 的值是否一样，因此 A(x)[E(z1)[F(z1,g(x))&z1=1]] 是符合语义的，这表明我们应该把量词抽出来只对词项进行变换。

• 接着，再引入 z2 满足 g(x)=z2, 这意味着在 E(z1)[F(z1,g(x))&z1=1] 的基础上，继续加入新变量和存在量词的组合，但由于存在量词之间的交换不会影响语义，因此加在内部和外部都是等价的：
  • 加到内部： E(z1)[E(z2)[(F(z1,z2)&z1=1)&G(z2,x)]]
  • 加到外部： E(z2)[E(z1)[(F(z1,z2)&z1=1)]&G(z2,x)]

这样的话，我们的算法可以是这样的：

• 如果当前识别到的是词项，那么我们知道其中解析树里也不可能包括关系和量词了，而将其中的函数消除的顺序并不重要（因为存在量词的可交换性），于是要做就是调用 _compile_term 把所有的变量替换中间步骤抽取出来。 然后把将形如 z1=g(x) 中的 g(x) 替换成 G(z1,x), 并联合拼接起来，

  核心实现部分如下：

  if is_equality(formula.root) or is_relation(formula.root):
      top_terms = []
      rel_list = []
      for term in formula.arguments:
          if not is_function(term.root):  # consant of variable
              top_terms.append(term)
          else:
              eqs = _compile_term(term)
              top_terms.append(eqs[-1].arguments[0])
              for eq in eqs:
                  rel_name = function_name_to_relation_name(
                      eq.arguments[1].root
                  )
                  left = eq.arguments[0]
                  right = eq.arguments[1]
                  rel = Formula(rel_name, [left, *right.arguments])
                  rel_list.append(rel)
      res = Formula(formula.root, top_terms)
      for rel in reversed(rel_list):
          var = rel.arguments[0]
          res = Formula("E", var.root, Formula("&", rel, res))
      return res
  

• 其他情况下如果是 ~ 或者 and/or/量词，则把这些算子提取出来，只对其中子公式递归调用。

R(f(g(x)),h(2,y),3) 转换结果为：

∃z1[
    (G(z1,x)
     &
     ∃z2[
         (F(z2,z1)
          &
          ∃z3[
              (H(z3,2,y)
               &
               R(z2, z3, 3))
          ])
     ])
]

下一节讨论公式和模型转换后等价性的问题

replace_functions_with_relations_in_formulas

T8.2 已经分析过，由于关系比函数拥有跟强大的描述能力，因此 T8.4 转换的公式能够捕捉到更多的 model.

本节再用额外的例子来强调：

• 偏函数带来的问题：

A(x)[f(x)=1] 如果对应模型只有一对象 1, 其中函数为 f(1)=1, 那么转换成 A(x)[E(z)[F(z,x)&z=1]] 之后，可以有更多满足该公式的模型，例如可以包括额外的对象 2,3, 且 F 的关系是 {(1,2),(1,3),(1,1)}, 之所以出现这种情况，是因为对于函数来说，不能是偏函数，即函数的定义域一定是在整个模型的所有对象上，否则会出现无意义语句。

• 一对多带来的问题：

E(x)[f(x)=1] 如果对应模型只有一对象 1, 其中函数为 f(1)=1, 转换成 E(x)[E(z)[F(z,x)&z=1]] 后，模型中 F 可以出现一对多 {(2,1),(1,1)}

因此根据 T8.4 把公式中所有函数替换成关系之后，公式的内涵更广了，类似把 p 转换成 p|q, 原本只有 {p=True} 这个 model 能够满足前者, 但 {p=True},{q=True} 都能满足后者了。

为了解决这种转换后的语义扩充，对于从函数转换得到的任何一个新的关系 F 都要加上额外的两条限制：

• ∀x[∃z[F(z,x)]]
• (∀x[(∀z1[(∀z2[((F(z1,x)&F(z2,x))→z1=z2)])])])’.

这是什么意思？我们用额外的两条语言规则"消灭了" 模型里的某种对象，也就是说，这个语言是对模型中的某一小部分关系进行约束，将其约束成和”函数“ 等价。 这告诉我们，当要用某种语法取代另一一种语法，同时对应了模型中某个对象被另外一个对象取代，我们要引入额外的限制， 而前提是：

• 作为替代物的对象（比如关系）的能力本身要能够覆盖住被替代物的能力
• 同时我们能够用现有的语言体系描述出这种替代的能力。

我们可以把语言上额外的描述称为是"函数公理", 它引入了函数这种概念，但没有定义函数的符号。另外这里还体现出， 我们可以预定义一个相对宽泛的模型（对象空间），然后在逻辑描述层面增加公理，来限制雕琢出一个新的（对象空间），比如我们先定义所有整数，然后在公理中添加 A(x)Greater(x,0), 那么就把空间限制到了自然数。（尽管一般是先定义自然数然后通过扩展模型，添加新的关系或函数来扩充到整数）

这些努力最终验证的了以下定理：

For every set F of formulas (which may contain function invocations), there exists a set F0 of function-free formulas obtainable from F via an efficient syntactic procedure, such that F has a model if and only if F0 has a model. Moreover, given a model of F0 there is a simple natural way to convert it into a model of F and vice versa.

theorem 8.1 (Redundance of Functions)

该定理表明函数在一阶逻辑中是冗余的，注意这种冗余有两个层面：

• 逻辑符号层面：Term 中不需要有嵌套的函数，只需要嵌套的（也可以是扁平的） Exist 和 & 公式链。

  这个层面我们在算法上就直接实现了，这是一个递归的局部修改算法，因此它是高效的。

• 模型层面：模型里可以不需要定义函数，完全用关系来取代。

  这个层面我们尽管我们也在算法上实现了，并且看上去也是高效的（只需要把 f 字典变成 F 集合或者反过来），但实际上这只是我们对模型的有限表达，例如我们无法用离散的代码来实现整个自然数上的函数和关系，因此这种转换并不是如以上 T8.1, T8.2 算法中所展现的那样简单直接，不过它总体还是 "simple natural way" 的，但它的深入讨论实际是在模型论中，涉及到包含无限元素的模型之间同构的定义

replace_equality_with_SAME_in_formulas

前文中提到，到目前为止 "=" 是在数理逻辑语言内部定义的，它是一个语法糖，也就是可以被其他东西所取代，本节就是证明 它是语法糖。

由于 "=" 的意义实际是内嵌在一阶逻辑内部的，就像 & | 这些符号的语义不是外部模型所赋予的一样。a=b 表示的是，a 和 b 两个符号所指代的是同一个对象。这个描述实际横跨了语法和语义两个世界，它相对数理逻辑来说是元层面的（尽管数理逻辑相对模型来说又是元层面的），因此本节用 SAME 来表示 =, 意味着，我们希望把这种元层面的描述降维到梳理逻辑语言本身中。

这里引入了四条公理来约束 SAME 关系：

• 自反性： reflexivity (SAME(x,x))
• 对称性： symmetry (SAME(x,y) iff SAME(y,x))

• 传递性： transitivity (SAME(x,y) and SAME(y,z) imply SAME(x,z)).

  以上三条公理实际仍然是逻辑语言内部的，因为它没用到模型提供的任何额外信息（如果此时我们不认为 SAME 必须加到模型中去的话），这就像我们在 &,| 的基础上又定义了一个二元逻辑算子一样，这些都是语法上的， 还没有向外部的模型去建立意义关系。如果只有这三个关系，一般只能称为是等价关系。

  要成为真正的相等关系，还需要添加一条公理：

• 替换性：对任何模型中提供的一元关系，都满足： ∀x[∀y[(SAME(x,y)→(R(x)→R(y)))]], 二元关系都满足：

  ∀x1[∀x2[∀y1[∀y2[((SAME(x1,y1)&SAME(x2,y2))→(R(x1,x2)→R(y1,y2)))]]]] 依次类推，需要遍历模型中所有关系的可替换性。

为什么要替换性？一个例子是，等价关系是更为宽泛的，比如在几何里，三角形的相似是一种等价关系，但在几何的模型中，我们会有面积这种函数，但三角形 A B 相似 A~B 并不能得到 A B 面积相等（函数相等被替换性覆盖了，即如果 x=y 那么对于任何模型里的 f, f(x)=f(y)）。

add_SAME_as_equality_in_model

T8.7 在 model 中添加 SAME 关系，这里只要说明自反性（其他性质也无法通过模型中的关系来说明），因为目的就是从模型引入 SAME 这种关系，然后在语法层面进行约束。

实现非常直接

for var in universe:
      relation_interpretations["SAME"].add((var, var))

make_equality_as_SAME_in_model

8.6 尽管加上了对相等的四个性质的限制，但是仍然无法精确描述 =, 原因在于 以上四个性质会对 universe 划分出不同的等价类（注意不是对公式里的 constant 划分，而是对模型这个语义世界进行划分），SAME 的内涵更广。

一个例子是，∀x[∀y[x=y]]，由于 = 中包含 "指向的唯一性" 性质，因此该公式对应的模型中只能有一个元素，假设是 1, 并且假设它可以对应一个关系 P 表示的是 x<3. 那么如果将公式替换成 ∀x[∀y[SAME(x,y)]], 刚才描述的模型也会是替换后公式的模型，但我可以构造另一个模型，它的元素包括 1,2,3, 并且在其中添加 SAME 关系, 这个时候会发现，该模型是满足 ∀x[∀y[SAME(x,y)]] 的，因为：

• 自反性由模型提供
• 对称性： 以 SAME(1,2) iff SAME(2,1) 为例，由于这是一个 <-> 关系，它没有描述一个事实 所以即便 SAME(1,2) 和 SAME(2,1) 都是 False, 也是成立的。
• 传递性： 同样， SAME(1,2) and SAME(2,3) imply SAME(1,3) 描述的也是关系，如果前提是 False, 整体也是成立的
• 替换性：如果 SAME(1,2), 那么 P(1) 和 P(2) 等价。这里有两种解释，如果 SAME(1,2) 成立，那么 P(1) 和 P(2) 也都是 True, 因为 1<3, 2<3; 但如果 SAME(1,2) 不成立替换性本身也是 True.

这里的核心在于， = 所表示的 "指向的唯一性" 是一种元函数，它要求公式里某个符号到实体的映射是一个函数性质的映射，但我们的一阶逻辑语言无法描述"指代"本身

该函数的实现是一个并查集的思路，找出同一个集合中的根元素，把等价类消除成单元素。

所有努力一定程度证明如下定理：

For every set F of formulas (which may contain equality), there exists a set F0 of equality-free formulas obtainable from F via an efficient syntactic procedure, such that F has a model if and only if F0 has a model. Moreover, given a model of F0 there is a simple natural way to convert it into a model of F and vice versa.

theorem 8.2 (Redundance of Equality)