Schema(Formula.parse('(times(x,0)=0&Ax[Ey[plus(x,y)=0]])'), {'x'})
注意这里可能会遇到作用领的问题，比如 E(x)[P(c)] 中 c 替换成 g(x) 的会把自由的 x 变成非自由的。
这种也是主场冲突，因为 x 是直接由模板提供的量词所限制的。
替换某个关系
关系是公式层面的词汇，P(x) 或者 R(x,y) 是一个带有真值（也可能因为有自由变量而未定义真值）的公式，
因此对关系的替换实际上要覆盖命题逻辑中的实例化，比如命题逻辑里 p->p 能够实例化为 ((a&b)->(a&b))
但谓词逻辑里是没有 p 这种简单公式的，谓词逻辑公式只能是量词修饰的公式或者关系所构造的公式，本文选择的是
用无参数的关系来表示某个任意的公式 p 。
Schema(Formula.parse('(Q()|~Q())'), {'Q'})
先把 x 替换成 z, 于是整个模板要变成 '(Az[R(z)]−>R(c))'
将 R 替换成 _>0 ，这时候 R 的是 z, 需要对于 _>0 来说，实际是要把 _ 替换成 z 得到 z>0, 再把该式子替换掉 R(z)
同时对于 R(c), 相当于要把 _>0 中下划线替换成 1 得到 1>0 ，用后者替换掉关系 R(c)
要注意的是，R 可以替换成一个带自由变量的公式，比如 >x, 这时候由于原 Schema 中本身就包含一个受限的变量 x, 因此不能替换成  (Ax[x>x]−>1>x), 这和变量替换中禁止替换成已有的非自由变量是类似的，也是主场冲突。
另外 ">0" 这实际也可以看作一种模板，写成 "_>0"，书中称为参数化公式，它替换了 R(x), 替换后下划线 _ 又要被 R(x) 中的 x 替换，因此算法实现上，先要获得关系模板里的参数，把参数替换到参数公式里，再把参数公式替换到模板里去（三次交互）。
现在假设参数公式里包含量词，比如 E[x][_=7], 那么把 R(x) 中 x 换进来后 x 直接受限了，这种受限是在参数公式里受限的，称为客场冲突。
再以数学归纳法为例，这是一个公理模板，说的是，对于任何单变量性质 P(x), 如果 P(0) 成立，并且 P(n)->P(n+1)
, 那么 A(x)[P(x)], 但也可以写成 P(c), 因此如下：
Schema(Formula.parse('((R(0)&(R(x)->R(x+1))-> P(c))'), {'R', 'c', 'x'})
变量替换中： A(x)[x=y], 受限的"模板变量" x 不能替换成公式里出现过的自由变量，因为这会改变原本自由的 y 变成不自由的 A(y)[y=y], 也就是改变了非模板变量的性质，这是主场冲突。
常量替换中： Ex[R(c)]−>R(c) 里的 "模板常量" c 可以替换成任意词项（带有自由变量）或具体常量，但任意词项中的变量不能是模板里的非自由变量，比如 c 替换成 x, 就会得到 Ex[R(x)]−>R(x) 这个逻辑上不成立的命题。这里的核心是，作为替代的词项中的变量原本是自由的，
但替换后变成不自由了，同样是主场冲突。
关系替换中：对于 R(x) 我们先要把 x 替换到 R 对应的特定参数化公式 F 中，如果 F 中已经限制了量词 x, 那么会遇到客场冲突问题。克服该问题后，再把消除参数（placeholder）后的公式 F(x) 去替换 R(x), 如果 F(x) 中有自由变量 y, 而 R(x) 所在环境中 y 是受限的，比如 Ay[R(x)], 那么还会遇到主场冲突问题。
总的来说，尽管 constant 可以替换成任何 term, 关系可以替换成任何 formula ，但不允许公式或者 term 中出现的变量被原公式中的量词所限定。
有两种方式避免出现变量作用于冲突问题：
在解释器设计上用宏展开的语法检查去避免，这在之后的代码实现中会体现出来。
本书并不是构造逻辑语言来实现自动化推理的，而是通过语言设计展示逻辑和数学的某些基础方面，
因此在本文展示的公理系统都是数学领域里经典的系统，比如自然数、集合论，因此这些公理模板一般都是 sound 的，
而 sound 的公理模板替换后一般也不会出现矛盾的命题。以上例举的 Ex[R(x)]−>R(x) 或者 A(x)[x=y] 这类公理模板，即便将其看作命题，本身就不是重言式。
任何替换都会产生新的 instance of this axiom schema
T9.1 替换 term 中的预留参数
Term.substitute(substitution_map, forbidden_variables)
前文说到过，当要把某个公理模板中的关系 R(x) 替换成 ">0" 关系时，实际上 ">0" 也是一种模板，书中称为参数方程，写作 "_>0"。
在替换 R(x) 前，先要获得其中的变量 x，把 x 替换 "_>0" 中的下划线得到 x>0 这个具体的关系公式，再将其到公理模板中。
因此我们首先要允许一些词项中包含 "_" 这个占位符号，接着要在词项或者 formula 中实现一个替换算法，使得算法能够遍历解析树，找到包含 _ 的叶子节点，然后将给定的变量或者词项替换掉 _. 
当然对于通用的替换算法，我们不要求只能替换 _, 可以在给定一个替换字典的情况下对任何符号进行替换，比如根据
substitution_map = {"x": "x->y"}
替换成变量好理解：比如刚才提到的 R(x) 替换成 ">0" 关系的场景
但 _ 还可以被替换成任意词项，比如存在一个公理模板 ~R(c), 其中 R 是关系模板， c 是常量模板，由于常量模板可以替换成任意词项，比如 s(1), R 又继续替换成关系，比如 "_>0"，那么整个替换过程是：
先把 c 替换成 s(1)
再把 s(1) 替换到 "_>0" 得到 s(1)>0. 因此这里 _ 可以被任意复杂的词项替换。
再 s(1)>0 替换 R(c), 最终得到 ~s(1)>0
此外这个过程说明了替换的优先级，一般先替换常量，再替换关系，如果有变量，则变量替换比常量还早
而在这个实现过程中，我们要引入错误检查，即如果在替换对象中出现了某个变量在给定的禁止替换变量名单中，那么抛出异常：
for formula in substitution_map.values():
    for var in formula.variables():
        if var in forbidden_variables:
             raise ForbiddenVariableError(var)
注意以上的检查过于宽泛了，它把替换表中所有可能被替换的公式里的变量都去和 forbidden_variables 比较，如果替换表里有 {"x":"y"} 且 forbidden_variables 中有 "y" 就会抛出异常。
但如果当前词项里压根没有 "x" 变量，那么 y 就不会出现在最终词项里，因此不会导致变量混淆，因此不应该抛出异常。
处理方式是，应该在最后真的要替换之前去检查：
if is_constant(self.root) or is_variable(self.root):
       if self.root in substitution_map:
           formula = substitution_map[self.root]
           # # check here
           for var in formula.variables():
               if var in forbidden_variables:
                   raise ForbiddenVariableError(var)
           return formula
       return self
比如 R(c) 中 c 要替换成 g(x), 而 R 要替换成 E(x)[_>x], 这时候会对后者构造替换表 {"_"：g(x)},  强行替换的结果是 E(x)[g(x)>x], 这导致了客场冲突应该抛出异常，算法实现上是把当前量词变量加入到 forbidden_variables 中（在已经处理上一步的情况下）。
注意区分这和公理模板替换的相似和区别，对于公理模式 Ex[R(c)]−>R(c) 里的 "模板常量" c ，不能替换成带有 x 的词项，比如 g(x) ，这是主场冲突问题。两种冲突产生原因是一样的，但一个是针对公理模板（主场），一个是针对公式（客场）。
if is_quantifier(self.root):
    if self.variable in substitution_map:
        substitution_map = {
            x: y
            for x, y in substitution_map.items()
            if x != self.variable
        statement = self.statement.substitute(
            substitution_map, forbidden_variables
        return Formula(self.root, self.variable, statement)
    forbidden_variables_extra = forbidden_variables | {self.variable}
    statement = self.statement.substitute(
        substitution_map, forbidden_variables_extra
    return Formula(self.root, self.variable, statement)
可以看到，公理模板内部还是一个公式，因此其替换本质上还是对公式进行替换，但相比于 T9.2 替换公式中变量和常量, 这里还出现了关系模板，也就是在遍历解析树的时候，还要额外去看整个子树，
这实际类似命题逻辑里的算子替换，即把 p->q 替换成 ~p|q。
我们先把关系模板之外的替换和上两节替换函数对应起来
本函数中参数 constants_and_variables_instantiation_map 实际就是 T9.2 中的 substitution_map 。因此如果当前公式是一个
思路就是，先调用 formula.substitute 替换掉常量和变量，这部分如果报错则捕获异常返回 Schema.BoundVariableError. 
相比于 T9.2 的另一个差别是， T9.2 中不会替换量词变量，但是当对参数化的关系，例如 \( \forall x R(x) \) ，可以把 R(x) 替换成 _=y
接着替换 nullary 关系，这里仍然需要用递归，去找到 nullary 关系，如果遇到是量词公式，那么需要把量词带入到
主要参考课本中给出的 guideline ，避免了 T9.2 不对量词进行替换所导致的差别:
由于 formula 只有 unary, binary 逻辑连接，equal 关系以及其他关系，那么对于逻辑连接直接分解递归即可，
如果当前是 equal, 由于不处理对等于的替换（已经在 chap 8 中实现了消解方法），因此和逻辑连接一样直接递归
以以下为例，
Q: Ax[(Greek(x)->Human(x))]
R: (Greek(_)->Mortal(_))
(Ax[(Ax[(Greek(x)->Human(x))]->(Greek(x)->Mortal(x)))]->(Ax[(Greek(x)->Human(x))]->Ax[(Greek(x)->Mortal(x))]))
Schema: (Ax[(Q()->R(x))]->(Q()->Ax[R(x)])) [templates: Q, R, x]
主要就是调用 T9.3, 为了调用 T9.3 需要准备 constants_and_variables_instantiation_map
和 relations_instantiation_map 两个字典。
Schema 的替换规则实现之后，就可以讨论这种规则是否保真了，也就是 schema 的 soundness ，其定义如下：
We say that a predicate-logic formula
is sound if it holds in every model that has interpretations for all its constant, function, and relation names, under any assignment to its free variable names. We say that a schema is sound if every instance of it (an instance is a predicate-logic formula) is sound.
definition 9.1 (Sound Formula; Sound Schema) 
一个公理模板是保真的，意味着它的所有实例后的公式都是保真，而公式保真意味着，对于所有包含公式中常量、关系、函数的模型，这个公式都是真的。注意这里定义的保真性是非常广的概念，它其实是想说明的是推理规则的保真性（正如命题逻辑里 sound 是用来描述 InferenceRule 的一样）。
当我们谈论某个命题具体的真和假时，和谈论以上公式的 sound 很不一样，比如用一阶逻辑来描述 Peano 公理时，整个公理系统会锚定到特定的模型，比如自然数的数学结构。当我们谈论 "4 是 2 的倍数"这个公式是真的时，有两个看待该问题的视角：
这个公式能够被公理根据 sound 的推理规则一步步推导出来，由于我们假定公理是真，所以它是真。
这种描述是大部分人对 "某个数学命题是真" 的理解。
但从逻辑系统构造者的角度看，逻辑系统的假设实际不包括 Peano 公理系统，而只包括内部的对 &,|,-> 的语义定义（来自最基础的语言和物理直觉）以及对后文会提到的谓词逻辑里新增的一些 sound 公理如 A(x)p(x) 那么 p(c) 的语义的假设。我们是在这个假设之上，得到了一个推理过程，这个推理过程描述了，从 Peano 公理可以推导出 "4 是 2 的倍数" 这一命题，这整个过程，如果去掉中间过程，得到就是一个推理规则，即如果 Peano 那么 "4 是 2 的倍数“，这条公式是 sound 是可以通过哪些最基础假设所得到的。
这就像即便 p 不是真的，"如果 p, 那么 p|~q" 这条推理规则也是 sound 的。
此外，由于一个谓词逻辑公式对应的模型实际是无穷的，这不同于命题逻辑，一个命题逻辑命题如果有 n 个变量，其对应的模型就有 2^n 个，这是有限的，可以用 model checking 的方式遍历所有可能模型去检查某个命题逻辑公式是否恒真，但无法遍历所有谓词逻辑对应模型去验证，因此我们一般能说出的谓词逻辑公理可能都是很通用的符合直觉的，比如后文会介绍的如果 A(x)p(x) 那么 p(c)，注意这个是无法证明的，它更像是对全称量词语义的定义，就像对命题逻辑里 & | 等连接词语义的定义一样；或者是从命题逻辑里延伸出来的，比如 A(x)(p(x)|~p(x)) 。
而公理模板的保真性实际来自于替换规则本身，更具体的，来自于两条处理变量作用域混淆的替换禁令：
we however restrict this to only be allowed for free variable names that
do not get bound by a quantifier in the resulting instance of the schema
we do not allow quantifications that bound any variable name in any instantiated
argument of that parametrized template relation name
这里值得说明的是，谓词逻辑只需要引入了两条推理规则 – MP 和 UG ，是因为其他规则实际可以被
编码到公理（假设）中， 例如与 UG 推理规则相对的是根据 A(x)[P(x)] 得到 p(c) ，它没有被描述成推理规则，但可以写成 
A(x)[P(x)]->p(c) 放到公理中。
在命题逻辑里，通过 deduction theorem 已经证明了类似的结论，而这同样适用于谓词逻辑。
We say that a set of assumptions A entails a conclusion φ if every model that satisfies each of the assumptions in A (under any assignment to its free variable names) also satisfies φ (under any assignment to its free variable names). We denote this by A |H φ.
We say that the inference of φ from A is sound if A |H φ. If A is the empty set then we simply write |H φ, which is equivalent to saying that φ is sound (as defined on in Definition 9.1).
definition 9.2 (Entailment; Sound Inference) 
Any inference that is provable via (only) sound assumptions/axioms is sound. That is, if X contains only sound schemas, and if A ∪ X ` φ, then A |H φ.
theorem 9.1 (The Soundness Theorem for Predicate Logic)
把一个命题逻辑根据 substitution_map 替换成谓词逻辑公式，这里纯粹是图遍历然后替换相应结点
substitution_map 的形式如下：
{'z1': Formula.parse('Ax[x=7]'), 'z2': Formula.parse('x=7'),'z3': Formula.parse('Q(y)')})
For every predicate logic tautology φ, there exists a valid proof of φ that uses only assumption/axiom and MP line justifications (and not tautology or UG line justifications), from the schema equivalents of H (or from the schema equivalents of Hˆ if the propositional skeleton of φ contains any operators beyond implication and negation).
theorem 9.2 (The Tautology Theorem: Predicate-Logic Version) 
If a predicate-logic formula φ is provable from a set of assumptions/axioms A, then it is provable without tautology line justifications from A as well as the schema equivalents of H'
corollary 9.1
以上提到的 H 是命题逻辑中希尔伯特公理，H' 则是希尔伯特公理对应的
这里核心在于理解谓词逻辑里的重言公式其实和命题逻辑的重言公式是 "同构" 的，这是因为某个谓词逻辑公式要满足所有模型，那么如果该公式中包括外部模型提供的关系 R, 由于 “满足所有模型” 这个条件实际没有对 R 提供任何有意义信息，因此我们无法对 R 获得任何真值性质，也就是 R 只能看作一个类似命题逻辑中 p 的对象，这种对象能够组合出很真表达式，不是因为 p 本身的值，而是来自于命题联结词内部的语义，比如 (p|~p) 是恒真的，完全是 | 和 ~ 的语义所决定。
那么对于命题逻辑， R(x)|~R(x) 的语义也完全是逻辑联结词提供的，外部模型不可能提供任何带有偏向的语义信息。
因此谓词逻辑里所有的重言公式实际都来自命题逻辑，要证明谓词逻辑的重言定理实际就是一个纸面上的转译操作，
给定任何谓词逻辑重言命题 tautology, 先抽取成命题逻辑形式，然后证明命题逻辑，再把命题逻辑证明转成谓词逻辑证明，因此我先给出 T9.12, 这是高层的代码实现：
def prove_tautology(tautology: Formula) -> Proof:
    propositional_tautology, substitution_map = (
        tautology.propositional_skeleton()
    skeleton_proof = prove_propositional_tautology(propositional_tautology)
    return _prove_from_skeleton_proof(
        tautology, skeleton_proof, substitution_map
要清楚这个函数想做什么，当要把一个命题逻辑的证明转成谓词逻辑的时候，很重要的一点是把命题逻辑的 rule 转成谓词逻辑 schema, rule 中包括 assumptions: Tuple[Formula, …] 和 conclusion: Formula, 命题逻辑的公理就是通过 rule 表示的， schema 则包括 formula: Formula 和 templates: FrozenSet[str]
因此这里的一个问题是把 InferenceRule 转成 Schema, 给定一个命题逻辑的公理，例如 q->(p->q)
如何转成以下公理 Schema(Formula.parse('(Q()->(P()->Q()))'), {'P', 'Q'})
这里采用的方法是比较直接的，由于两个逻辑语言的公理系统已经建立的一一对应关系，如下，因此直接查表即可：
PROPOSITIONAL_AXIOM_TO_SCHEMA = {
  I0: I0_SCHEMA, I1: I1_SCHEMA, D: D_SCHEMA, I2: I2_SCHEMA, N: N_SCHEMA,
  NI: NI_SCHEMA, NN: NN_SCHEMA, R: R_SCHEMA}
... {'p': PropositionalFormula.parse('(z1->z2)')
... 'q': PropositionalFormula.parse('~z1')},
... {'z1': Formula.parse('Ax[(x=5&M())]'),
... 'z2': Formula.parse('R(f(8,9))')})
{'P': (Ax[(x=5&M())]->R(f(8,9))), 'Q': ~Ax[(x=5&M())]}
T9.11b _prove_from_skeleton_proof
更难的问题是，给定一行命题逻辑的证明行，例如 z1->(z2->z1) 如何转成以下公式的的一个 instance 呢？
Schema(Formula.parse('(Q()->(P()->Q()))'), {'P', 'Q'})
首先要计算出 q->(p->q) 到 z1->(z2->z1) 的映射表（通过 T4.5c 实现的 InferenceRule.specialization_map 获得），它对应的就是 propositional_specialization_map, 再计算出 z1 到谓词逻辑公式的映射，这是通过以下等式对齐的
 Formula.from_propositional_skeleton(
skeleton_proof.statement.conclusion, substitution_map) == formula
substitution_map 在本题（T9.11b）中都是现成提供的，但在下一题中需要手动提取
有了以上 map 调用 T9.11a 的方法得到类似以下的映射表：
{'P': (Ax[(x=5&M())]->R(f(8,9))), 'Q': ~Ax[(x=5&M())]}
然后调用 scheme 中的 map 即可
方法就是先把 p,q 这些命题逻辑变量转成 P,Q 这样的关系名，然后根据
_axiom_specialization_map_to_schema_instantiation_map 
返回的结果，给 T9.4 的 Formula.instantiate
函数进行实例化（这里返回结果中可能还缺少 _ 占位符）
在谓词逻辑中， Proof 是没有 rules 属性的，其结构如下，它最基本的推理规则 MP rule 已经 hardcore 编码成了 MPLine 了，同时 UG 规则也被 hardcode 了
谓词逻辑的 proof:
class Proof:
    assumptions: FrozenSet[Schema]
    conclusion: Formula
    lines: Tuple[Proof.Line, ...]
命题逻辑的 proof:
class Proof:
    statement: InferenceRule
    rules: FrozenSet[InferenceRule]
    lines: Tuple[Proof.Line, ...]
而命题逻辑中 MP 是一条规则单独放在 Proof.rules 中的，如下：
MP = InferenceRule([Formula.parse('p'), Formula.parse('(p->q)')],
                   Formula.parse('q'))
转换的结果中只包含 MP 和 assumption Line