无参数二阶逻辑的 MacNeille 完备化与 Buchholz Omega 规则

Buchholz 的 Omega 规则是一种为二阶算术的各种子系统给出切消的语法（可能是无序数）证明的方法。我们的目标是从代数观点来理解它。在高阶逻辑的众多切消证明中，Maehara 和 Okada 的代数证明尤为引人关注，因为其论证的本质可以在代数上描述为（Dedekind-）MacNeille 完备化结合 Girard 的可约性候选者。有趣的是，结果表明，作为逻辑推理规则表述的 $\Omega$-规则在 MacNeille 完备化中找到了其代数基础。在本文中，我们考虑二阶直觉主义逻辑的无参数片段 LIP0、LIP1、LIP2、...，它们对应于直至 omega 的迭代归纳定义的算术理论 ID0、ID1、ID2、...。在此设定下，我们观察到 Omega 规则与 MacNeille 完备化之间的形式联系，这引出了一种在 Heyting 值语义中以一阶方式解释二阶量词的方法，称为 Omega 解释。基于此，我们给出了对每个 n<omega 的 LIPn 的切消代数证明，该证明可在 IDn 中局部形式化。作为推论，我们得到了在弱算术理论中成立的 LIPn 切消与 IDn 的 1-一致性之间的等价性。