咱们先从基础概念聊起：
莫斯托夫斯基坍缩引理指出：对所有集合$S$，以及$S$上的外延性、良基关系$R$，存在一个传递集$T$，使得$(S, R)$与$(T, \in_T)$同构。它的典型应用之一，就是把ZFC的良基模型坍缩为一个同构的传递模型。

其实我们可以把这个引理稍作强化，得到“广义坍缩引理”：对所有集合$S$和$S$上的良基关系$R$，存在一个（必然唯一的）函数$f$，其定义域为$S$，且对所有$s \in S$，有$f(s) = {f(r) \mid r R s}$。这里的$f$被称为$(S, R)$的坍缩函数。

用∈-归纳很容易验证：如果$R$是外延的，那么$f$是单射；这样一来，$f : S \to f(S)$就是$(S, R)$到$(T, \in_T)$的同构，莫斯托夫斯基坍缩引理也就成立了。

广义坍缩引理的常规证明其实是良基递归的直接应用，而良基递归本身需要完全分离公理和替换公理才能证明。但问题在于，构造性ZF（CZF）并没有完全分离公理，只有Δ₀分离公理。

这就引出了我们的核心问题：

• 广义坍缩引理能在CZF中证明吗？
• 莫斯托夫斯基坍缩引理能在CZF中证明吗？

有意思的是，广义坍缩引理等价于完全良基归纳，而莫斯托夫斯基坍缩引理等价于针对外延关系的完全良基归纳。所以我们的问题也可以转化为：

• CZF能证明完全良基归纳吗？
• CZF能证明针对外延关系的完全良基归纳吗？

补充说明：如果我们给CZF加上W-类型的存在性公理，上述结论就都能成立了。具体来说，这个公理是：对所有集合族${B_a}{a \in A}$，存在最小的集合$W{a \in A} B_a$，满足对所有$a \in A$、所有函数$f : B_a \to W_{a \in A} B_a$，都有$(a, f) \in W_{a \in A} B_a$。

我们可以在$W_{a \in A} B_a$上定义一个关系$\prec = {(f(b), (a, f)) \mid a \in A, f : B_a \to W_{a \in A} B_a, b \in B_a}$，不难验证$\prec$是良基的。更关键的是，我们可以用∈-归纳证明$\prec$的所有良基归纳实例——这里的技巧是，$\prec$是∈的传递闭包的子关系，这一点可以从CZF中函数和有序对的精确定义推导出来。

现在考虑任意集合$C$以及$C$上的良基关系$\prec$，定义$B_c = {x \in C \mid x \prec c}$。我们可以用Δ₀良基递归定义一个显然的函数$f : C \to W_{c \in C} B_c$，即$f(c) = (c, f|_{B_c})$。这个$f$是单射，并且对所有$x, y \in C$，$x \prec y$当且仅当$f(x) \prec f(y)$。这样一来，我们就能证明$(C, \prec)$的完全良基归纳了。

不过很遗憾，我相当确定CZF本身并不证明W-类型的存在性。

备注：内容来源于stack exchange，提问作者Mark Saving