标题： 论诱导在膨胀上的应用与巴赫曼-霍尔维茨不动点 显示英文标题

标题： Induction on Dilators and Bachmann-Howard Fixed Points

摘要： J.-Y. Girard的$\Pi^1_2$-逻辑中最重要的一条原理是关于膨胀的归纳法。特别是，Girard利用这一原理构造了他著名的函子$\Lambda$。他声称$\Lambda$的全体性等价于反向数学中$\Pi^1_1$-可定义性的集合存在公理。虽然Girard在1980年左右提供了一个合理的证明描述，但似乎直到今天，这些非常技术性的细节仍未被完全解决。几年前，一种松散相关的途径导致了$\Pi^1_1$-可定义性与某种Bachmann-Howard原理之间的等价性。本文解决了这个循环。我们将Bachmann-Howard原理与关于膨胀的归纳法联系起来。 这使我们能够证明$\Pi^1_1$-可读性与 P. Päppinghaus 提出的函子$\mathbb J$的整体性是等价的，这可以看作是$\Lambda$的简化版本。 显示英文摘要

摘要： One of the most important principles of J.-Y. Girard's $\Pi^1_2$-logic is induction on dilators. In particular, Girard used this principle to construct his famous functor $\Lambda$. He claimed that the totality of $\Lambda$ is equivalent to the set existence axiom of $\Pi^1_1$-comprehension from reverse mathematics. While Girard provided a plausible description of a proof around 1980, it seems that the very technical details have not been worked out to this day. A few years ago, a loosely related approach led to an equivalence between $\Pi^1_1$-comprehension and a certain Bachmann-Howard principle. The present paper closes the circle. We relate the Bachmann-Howard principle to induction on dilators. This allows us to show that $\Pi^1_1$-comprehension is equivalent to the totality of a functor $\mathbb J$ due to P. P\"appinghaus, which can be seen as a streamlined version of $\Lambda$.