数理逻辑及其 python 实现:7
Notes on 「Mathematical logic through python」
七、谓词逻辑的语法和语义
命题逻辑对应的外部世界（的意义）只有真和假两种对象，每个命题只能是真或者是假。谓词逻辑在形式符号和真假模型之间加了新的东西：
- Term: 可以是常量，变量和函数调用形式（不是函数名 f，而是 f(x,y), 它本质是函数产生的一个结果），这里的常量对应的是命题逻辑中的变量， Term 和量词一起组合成 Formula, formula 再和外部的真假世界关联
Term 本身的组合是递归的，它的递归依靠的函数，例如如果 t 是 term ，那么 f(t) 也是 term
- Term 只能通过"关系" 变成带有真值的公式（也可能暂时没有真值，比如 g(x)=1）。
- 变量的引入使得某些 formula 可以没有真值，是 partial 状态
谓词逻辑可以对所有数学进行形式化
而变量实际是与量词对应的
Formula 是通过以下操作符连接 term 的结果：
- equality
- logic negation 和 binary operation: 命题逻辑中的一元和二元连接符
- relation invocation: 与函数的区别在于 relation 只能是真值函数 实际上 equality 和逻辑连接符号都是 relation invocation 的语法糖
- quantification 函数和量词是谓词逻辑的关键（函数覆盖了谓词）。
T7.1 - 7.2 谓词逻辑树的序列化
Term.__repr__; Formula.__repr__
是实现对 Term 和 Formula 的 repr 函数，都是用树的遍历算法进行序列化，主要是理解清楚打印的格式。
T7.3: 谓词项的 parsing
Term._parse_prefix; Term.parse
利用谓词逻辑的 prefix-free 性质来对 term 进行 parse, 与 T1.4 是类似的。
由于有这种性质，可以用类似贪心的方式，找到第一个合法的 term 就进行递归。
T7.5-6: 语法树遍历
T7.5 找出 term 中所有 constants, variables 和 function, 这里是一个 dfs 遍历算法。
T7.6 找出 formula 中所有 constants, variables, free_variable， function 和 relation 形式都是 dfs，只是搜集的时候判断条件不同。
这里找 free_variable 需要用集合的差，也就是如果某个公式是带有量词的，那么肯定有 bound variable, 那么进入该公式主体部分搜集所有变量，然后减去量词后面的变量就是自由变量。
T7.7: 计算词项的语义
Model.evaluate_term
这部分是理解谓词逻辑的又一个关键。谓词逻辑的语义模型中，除了真和假之外，还包括：常量、函数、关系以及对它们的解释，这些词汇以及它们的语义是通过外部模型所提供的。
这实际让我感到失望，我原本以为数理逻辑符号本身可以是第一性的，但对于数学领域，它们本身就有模型，有意义，根本不需要建立在数理逻辑的基础之上，数理逻辑只是一个符号系统的引用，比如 ‘1' 这个常量符号对应了模型中 1 这个对象。数理逻辑本身完全是一个次级的系统，去描述某个本身已经有的东西。
它的作用在于统一描述数学的语言，人类做数学推理的时候基本还是基于模型本身的，比如所谓的数学直觉，但只不过为了能够精确交流分享成果，才给数学定义了一套语法规则，以便在公共平台上进行表达。
在本题中，模型里的对象也都是字符串，而不用 python 原生的对象来表示。
T7.8 计算公式的语义
Model.evaluate_formula
这里有几个注意点：
- 需要额外提供给 free variable 的赋值表
- 对于 "=", 这是本文里谓词逻辑系统里预订的一个符号，它的解释是系统自身提供的（就像命题逻辑中， and,or 都是系统内定的），但我们还可以在模型内定义 Equal 关系
变量绑定和作用域问题，只有嵌套最内部的 term 中仍然是自由的变量的情况下才能把外部的变量赋值带进去，例如 公式 x=0 | (E(x)[IsPrimitive(x)→A(x)[times(x,x)=1]])) 中由于有 x=0, 因此哦我们需要一个外部的 x 赋值，但 times(x,x) 中的 x 的值不应该接受外部赋值，而是 A(x) 里展开的值，因此用要以下方式去扩充赋值字典
if formula.root == "E": return any( self.evaluate_formula(formula.statement, {**assignment, formula.variable: x}) for x in self.universe)
这个步骤和编程语言解释器里，解释函数调用时的 environment 很相似，它可以看作是一个级联的向上查询的链表结构（级联查询）
T7.9 判断公式和模型的相容性
Model.is_model_of(formulas):
这个函数目的是检查该模型是否满足给定的所有 formula ，如果这个 formula 不是封闭的，有自由变量的话，默认为 universal 量词，因此实现思路就找到 formula 中所有自由变量，并给公式加上 forall, 组成新的公式然后 evaluate, 一旦有一个公式解释为 False 则直接返回 False, 如果所有公式都解释为 True, 才能最终返回 True.
有哪些特点呢：
- 实际上，and ，or 只是一种预定义的关系， ~ 也是预定义的，但它们只作用在真值上，或者作用在 partial 真值上
- 关系之间可以嵌套，function 之间也可以嵌套，但是一旦关系里出现了一个 term, 那么 term 内部只有关系嵌套
- 把函数专为关系，实际是一种打破 Term 嵌套的手段