21.3.4

2025-11-14

题目

Is there a pair of types that is related by , but not by ? What about a pair of types that is related by , but not by ?

解答

只写前半部分，这一部分书中给出的解答是错误的，errata 指出了这一点

只需证明形如 ， 为无穷类型的关系都在 中且不在 中

，考虑集合

容易验证，，根据 the principle of coinduction，，故

现在，考虑集合 ，下面验证

由于 ，只需证明

而 ，反证法：若存在无穷类型 ，，则由 的定义，以下三种情况必有至少一个满足：

Case 1:

但是这说明 ，不可能

Case 2:

但是这说明 ，且 中至少一个是无穷类型（否则 均有穷， 有穷，矛盾），不妨设为 ，那么 ，与 的定义矛盾

Case 3:

这也不可能，与 Case 2 同理

综上，以上三种情况均导出矛盾， 得证

现在，根据 the principle of induction，，故对于任意无穷类型 ，

证毕