e≤e2es≤e4 (×mon) e,xe3≤e,xea 对于自然数上通常的序，这是一个相对弱的证明系统，但是对于举例说明基本概念来讲是足 够了。 对一个证明系统来说，需要确立的一个重要性质是，在公式的某种特定解释下，每个可 证的公式都为真。这叫做证明系统的可靠性(soundness)。现在以证明本例的证明系统对≤ 可靠为例，来说明证明结构上的归纳，本例文法的算术表达式按通常的方式在自然数集合上 解释。具体说，需要证明下面的性质对任何证明π都成立： P(π)如果π是e≤e'的一个证明，那么e的值≤e的值，不管其中的变量怎样取值。 归纳基础是为所有的公理证明该性质。这是非常容易的，不管e中的变量怎样取值，e 都是解释到某个自然数n,因此总有n≤n和0≤n。 本证明的归纳有三步，这里证明(+mon)和(×mon)两种情况，而把(trans)情况留给读者。 假定可以证明e1≤e2和e3≤e4。任意选择e1,,e4中变量的值，并把这四个表达式的值叫做 n,,4。由归纳假设，有n≤2和n3≤n4。很容易看出m+n仍≤m2+4,同样有n1×3≤2 ×4。该推理可用于变量所有可能的取值，因此该性质对终止于(+mon)和(xmon)的证明都成 立。(trans)的情况由读者自己给出，该归纳证明结束。 ◇ 1.4.3良基归纳 前面所介绍的归纳都是更一般的基于良基关系的归纳的实例。良基关系在计算机科学中 是重要的，在很多地方要用到它，例如它和程序终止的证明方法有联系。 集合A的良基关系(wel-founded relation)是A上的一个二元关系<，它具有这样的性 质：A上不存在无穷递减序列ao>a1>a2>..(在此定义b>a当且仅当a<b)。例如，若j= i+1,则i<j,那么这是自然数上的一个良基关系。从该例得知，良基关系不一定有传递性。 也很容易看出，每个良基关系都是非自反的，即对任何aEA,a<a不成立。其理由是，如 果a<a,那么存在无穷递减序列a>a>a>..。 一个等价的定义是，A上的二元关系<是良基的，当且仅当A的每个非空子集B有一个 极小元(aeB是极小元，如果不存在d∈B使得d<a)。它的证明在下面的引理中。 引理1.1如果<是集合A上的二元关系，那么<是良基的当且仅当A的每个非空子集都 有一个极小元。 证明首先，假定<是集合A上的良基关系，令BCA是任意非空子集。用反证法证明B 有极小元。如果B无极小元，那么对每个aeB,可以找到某个d∈B使得d<a。这样，可 以从任意的aoeB开始，构造一个无穷递减序列ao>a1>a2>.,。这就证明了该引理的前一 半。 反过来，假定每个子集有一个极小元，那么不可能存在无穷递减序列ao>4>2>., 因为这样的序列给出了无极小元的集合{ao,a1,a2,…}。这就完成了整个证明。 命题12（良基归纳）令<是集合A上的一个良基关系，令P是A上的某个性质。若每 当所有的P(b)(b<a)为真则P(a为真，则对所有的a∈A,P(a为真。 证明假定对每个a∈A有，若所有的P(b)(b<a)为真则P(a)为真（用符号表示的话，即 假定Va.(b.(b<a一P(b)一P(a)。用反证法来证明对所有的a∈A,P(a)为真。 如果存在某个x∈A使得Px)成立，那么集合 B={a∈A|-Pa)} 非空。由引理1.1，B一定有极小元a∈B。但是，对所有的b<a,P(b)一定成立（否则a不 是B的极小元)，这就和假定Vb.(b<a一P(b)一P(a)矛盾。所以该命题成立。 口 1010 1 3 2 4 1 2 3 4 e e e e e e e e × ≤ × ≤ ≤ (×mon) 对于自然数上通常的序，这是一个相对弱的证明系统，但是对于举例说明基本概念来讲是足 够了。 对一个证明系统来说，需要确立的一个重要性质是，在公式的某种特定解释下，每个可 证的公式都为真。这叫做证明系统的可靠性（soundness）。现在以证明本例的证明系统对≤ 可靠为例，来说明证明结构上的归纳，本例文法的算术表达式按通常的方式在自然数集合上 解释。具体说，需要证明下面的性质对任何证明π都成立： P(π) 如果π是 e ≤ e′的一个证明，那么 e 的值≤ e′的值，不管其中的变量怎样取值。 归纳基础是为所有的公理证明该性质。这是非常容易的，不管 e 中的变量怎样取值，e 都是解释到某个自然数 n，因此总有 n ≤ n 和 0 ≤ n。 本证明的归纳有三步，这里证明(+mon)和(×mon)两种情况，而把(trans)情况留给读者。 假定可以证明 e1 ≤ e2和 e3 ≤ e4。任意选择 e1, …, e4 中变量的值，并把这四个表达式的值叫做 n1, …, n4。由归纳假设，有 n1 ≤ n2和 n3 ≤ n4。很容易看出 n1 + n3 ≤ n2 + n4，同样有 n1 × n3 ≤ n2 × n4。该推理可用于变量所有可能的取值，因此该性质对终止于(+mon)和(×mon)的证明都成 立。(trans)的情况由读者自己给出，该归纳证明结束。 ￾ 1.4.3 良基归纳 前面所介绍的归纳都是更一般的基于良基关系的归纳的实例。良基关系在计算机科学中 是重要的，在很多地方要用到它，例如它和程序终止的证明方法有联系。 集合 A 的良基关系（well-founded relation）是 A 上的一个二元关系≺，它具有这样的性 质：A 上不存在无穷递减序列 a0 ; a1 ; a2 ; …（在此定义 b ; a 当且仅当 a≺ b）。例如，若 j = i +1，则 i ≺ j，那么这是自然数上的一个良基关系。从该例得知，良基关系不一定有传递性。 也很容易看出，每个良基关系都是非自反的，即对任何 a∈A，a ≺ a 不成立。其理由是，如 果 a ≺ a，那么存在无穷递减序列 a ; a ; a ; …。 一个等价的定义是，A 上的二元关系≺是良基的，当且仅当 A 的每个非空子集 B 有一个 极小元（a∈B 是极小元，如果不存在 a′∈B 使得 a′≺ a）。它的证明在下面的引理中。 引理 1.1 如果≺是集合 A 上的二元关系，那么≺是良基的当且仅当 A 的每个非空子集都 有一个极小元。 证明 首先，假定≺是集合 A 上的良基关系，令 B⊆A 是任意非空子集。用反证法证明 B 有极小元。如果 B 无极小元，那么对每个 a∈B，可以找到某个 a′∈B 使得 a′≺ a。这样，可 以从任意的 a0∈B 开始，构造一个无穷递减序列 a0 ; a1 ; a2 ; …。这就证明了该引理的前一 半。 反过来，假定每个子集有一个极小元，那么不可能存在无穷递减序列 a0 ; a1 ; a2 ; …， 因为这样的序列给出了无极小元的集合{a0, a1, a2, …}。这就完成了整个证明。 ￾ 命题 1.2（良基归纳） 令≺是集合 A 上的一个良基关系，令 P 是 A 上的某个性质。若每 当所有的 P(b) (b ≺ a)为真则 P(a)为真，则对所有的 a∈A，P(a)为真。 证明 假定对每个 a∈A 有，若所有的 P(b) (b ≺ a)为真则 P(a)为真（用符号表示的话，即 假定∀a. (∀b.( b ≺ a ⇒ P(b)) ⇒ P(a))）。用反证法来证明对所有的 a∈A，P(a)为真。 如果存在某个 x∈A 使得¬ P(x)成立，那么集合 B = { a∈A | ¬ P(a)} 非空。由引理 1.1，B 一定有极小元 a ∈B。但是，对所有的 b ≺ a，P(b)一定成立（否则 a 不 是 B 的极小元），这就和假定∀b.( b ≺ a ⇒ P(b)) ⇒ P(a)矛盾。所以该命题成立。 ￾