论文标题
井订单原理和$π^1_4 $ - 陈述：试点研究
Well ordering principles and $Π^1_4$-statements: a pilot study
论文作者
论文摘要
在以前的工作中，作者表明$π^1_1 $ - 沿$ \ mathbb n $引导等同于对序列上的每个正常函数的适当形式化，即列表都有一个固定点。更确切地说，这是用J.-Y.表示正常功能的表示证明的。吉拉德（Girard）的扩张器，这是井订单的尤其统一的转变。本文在下一个类型的水平上起作用，并考虑扩张器的统一转换，称为$ 2 $ -PTYKES。我们表明，$π^1_2 $ - 沿$ \ mathbb n $沿着$ \ mathbb n $诱导等同于所有满足特定正态条件的$ 2 $ -ptykes的固定点。除了这一具体结果之外，论文为分析$π^1_4 $陈述的进一步分析铺平了道路。
In previous work, the author has shown that $Π^1_1$-induction along $\mathbb N$ is equivalent to a suitable formalization of the statement that every normal function on the ordinals has a fixed point. More precisely, this was proved for a representation of normal functions in terms of J.-Y. Girard's dilators, which are particularly uniform transformations of well orders. The present paper works on the next type level and considers uniform transformations of dilators, which are called $2$-ptykes. We show that $Π^1_2$-induction along $\mathbb N$ is equivalent to the existence of fixed points for all $2$-ptykes that satisfy a certain normality condition. Beyond this specific result, the paper paves the way for the analysis of further $Π^1_4$-statements in terms of well ordering principles.
