巴赫曼-霍华德不动点的范畴构造

Peter Aczel 给出了正规函子（即保持初始段的扩张子）不动点的范畴构造。对于一般的扩张子 $X\mapsto T_X$，我们不能期望得到一个良基的不动点，因为 $T_X$ 的序型可能总是超过 $X$ 的序型。在本文中，我们展示了如何构造 $T$ 的巴赫曼-霍华德不动点，即一个序 $\operatorname{BH}(T)$，并带有一个“几乎”保序的坍缩 $\vartheta:T_{\operatorname{BH}(T)}\rightarrow\operatorname{BH}(T)$。基于先前的工作，我们证明了 $\Pi^1_1$-理解公理等价于如下断言：对任意扩张子 $T$，$\operatorname{BH}(T)$ 都是良基的。