这意味着如果有3+5=8的证明和8=2的证明，那么把它们合起来可以形成等式3+5=23 的证明。横线上面的公式叫做证明规则的前提，横线下面的公式叫做结论。 形式地讲，一个证明可以定义为一个公式序列，该序列中的每个公式都是公理或者是由 先前的公式通过一条推理规则得到的结论。证明的这种形式定义是非常有用的，它使得可以 基于证明的长度（也就是该序列的长度），用自然数归纳法来讨论证明的性质。另一种观点 显得更有见识：由于推理规则通常由一组前提和一个结论组成，因此很容易把证明看成是某 种形式的树，其叶结点和内部结点由公式标记。也就是把证明所用的公理看成叶结点，把所 用的推理规则 A...An B 看成树的内部结点，其子树必须是A,,A的证明。为了和推理规则通常的图示方向一致， 画证明树时一般把树根放在底部。这样，如果从41，，An的证明构造B的证明，其证明树 的形式见图11。在图11中，在横线上的每个尖角图形代表一棵证明树，它的结论是本证 明规则的一个前提。把证明看成树的一个好处是，它提示了一种归纳形式，这种归纳形式本 质上同树的结构归纳是一样的。 B 图1.1证明树示意图 如果基于证明树的高度进行归纳，那么归纳基础是：每个公理具备某性质：归纳步骤是： 假定任何较短的证明都有这个性质，然后证明，结束于各个推理规则的证明也都具有这个性 质。这就形成了证明上的结构归纳，其形式如下： 证明上的结构归纳在某个证明系统中，为了证明对每个证明π，P(π)为真，只要完成下 面两步就足够了： (1)对该证明系统中的每个公理，证明P成立： (2)假定对证明π1，，元k,P都成立，证明P(π)也成立。π是这样的证明，它结束于使 用一个推理规则，并且是从证明π1，，元k延伸出来的一个证明。 例11本例用一个简单的证明系统来介绍证明结构上的归纳，它是表达式小于等于关系 (e≤e')的一个简单证明系统，其中e和e由下面的文法产生： e::=01ve+ee*e 该证明系统有两个公理，其一是说≤是自反的： e≤e (e0 另一个是说0小于等于任何表达式： 0≤e (0≤) 该系统有一个传递性推理规则，另有两条规则表示加和乘的单调性。 e≤e'e'se" (trans） ese" e≤e2e3≤e4 (+mon) e1+e3≤e2+e4 99 这意味着如果有 3 + 5 = 8 的证明和 8 = 23 的证明，那么把它们合起来可以形成等式 3 + 5 =23 的证明。横线上面的公式叫做证明规则的前提，横线下面的公式叫做结论。 形式地讲，一个证明可以定义为一个公式序列，该序列中的每个公式都是公理或者是由 先前的公式通过一条推理规则得到的结论。证明的这种形式定义是非常有用的，它使得可以 基于证明的长度（也就是该序列的长度），用自然数归纳法来讨论证明的性质。另一种观点 显得更有见识：由于推理规则通常由一组前提和一个结论组成，因此很容易把证明看成是某 种形式的树，其叶结点和内部结点由公式标记。也就是把证明所用的公理看成叶结点，把所 用的推理规则 B A An ... 1 看成树的内部结点，其子树必须是 A1, …, An 的证明。为了和推理规则通常的图示方向一致， 画证明树时一般把树根放在底部。这样，如果从 A1, …, An的证明构造 B 的证明，其证明树 的形式见图 1.1。在图 1.1 中，在横线上的每个尖角图形代表一棵证明树，它的结论是本证 明规则的一个前提。把证明看成树的一个好处是，它提示了一种归纳形式，这种归纳形式本 质上同树的结构归纳是一样的。 如果基于证明树的高度进行归纳，那么归纳基础是：每个公理具备某性质；归纳步骤是： 假定任何较短的证明都有这个性质，然后证明，结束于各个推理规则的证明也都具有这个性 质。这就形成了证明上的结构归纳，其形式如下： 证明上的结构归纳 在某个证明系统中，为了证明对每个证明π，P(π)为真，只要完成下 面两步就足够了： （1）对该证明系统中的每个公理，证明 P 成立； （2）假定对证明π1, …, πk，P 都成立，证明 P(π)也成立。π是这样的证明，它结束于使 用一个推理规则，并且是从证明π1, …, πk延伸出来的一个证明。 例 1.1 本例用一个简单的证明系统来介绍证明结构上的归纳，它是表达式小于等于关系 （e ≤ e′）的一个简单证明系统，其中 e 和 e′由下面的文法产生： e ::= 0 | 1 | v | e + e | e ∗ e 该证明系统有两个公理，其一是说≤是自反的： e ≤ e (ref) 另一个是说 0 小于等于任何表达式： 0 ≤ e (0 ≤) 该系统有一个传递性推理规则，另有两条规则表示加和乘的单调性。 e e e e e e ≤ ′′ ≤ ′ ′ ≤ ′′ (trans) 1 3 2 4 1 2 3 4 e e e e e e e e + ≤ + ≤ ≤ (+mon) B An - - - A1 图 1.1 证明树示意图