Δ₀分离公理与小分离公理的相对强度及Δ₀公式的非语法刻画技术问询

在直觉主义、构造性集合论的框架里，一个核心的公理模式是Δ₀分离公理，它的形式化表述为：

$$
\forall x\exists y\forall z(z\in y\leftrightarrow z\in x\wedge\phi(x, z))\text{ 其中$\phi$是$\Delta_0$公式}
$$

选择Δ₀公式作为限制的原因很直观：Δ₀集合是完全直谓定义的，而无限制的完全分离公理已知会被**排中律（LEM）**推导出来，这体现了它的非直觉主义本质。不过Aczel从类型论角度为另一种分离原则提供了辩护——小分离公理，它的形式是：

$$
\forall x\exists y\forall z(z\in y\leftrightarrow\exists w(w\in x\wedge\phi(x, w)\wedge w = z))
$$

这个公理对公式$\phi$没有任何语法限制。值得注意的是，如果$\phi$在$w$上是（内部）外延的（即可以证明$w = z\rightarrow \phi(x, w)\leftrightarrow\phi(x, z)$），那么小分离公理就等价于去掉Δ₀限制的通用分离公理；而所有Δ₀公式都能通过常规的语法归纳法证明是外延的，因此小分离公理可以推导出所有Δ₀分离公理的实例。

我现在有几个核心问题想探讨：

• Δ₀分离公理能否反过来推导出小分离公理？
• 如果不能的话，Δ₀分离公理有没有非语法层面的刻画方式？
• 这两个公理的相对强度应该如何准确比较？

补充一些已知的背景信息：在经典的$\mathsf{KP}$（克里普克-普拉特克集合论）中，Δ₀分离公理可以推导出更强的分离原则——所有绝对公式的分离。但在直觉主义$\mathsf{KP}$里，这一点目前还没有定论。不过我们知道$\mathsf{KP}$和$\mathsf{CZF}$（构造性策梅洛-弗兰克尔集合论）是可以互相解释的，这意味着至少相对于$\mathsf{CZF}$，绝对分离应该是成立的，但我不确定绝对性是否能用来证明小分离公理的所有实例。

从直觉层面来看，要利用小分离公理证明某个元素属于集合$y$，必须给出$w$的具体见证。这似乎会把$\phi$中的所有量词都限制在“当前可构造”的集合范围内，从而恢复直谓性——看起来每一次小分离的应用都能等价转化为Δ₀分离的应用，但我怀疑这里可能暗藏了非直谓性，没法从这个直觉论证里提取出元理论层面的严格证明。

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