Skip to main content
MathOverflow

Return to Answer

added 227 characters in body
Source Link
Fedor Pakhomov
Fedor Pakhomov
  • 5.8k
  • 1
  • 21
  • 26

One way is to allow recursion on ordinals for ptykes for all finite types. Then the supremum of all ordinals describable in this way will be exactly B-H ordinal. See outline of ptyx interpretation of modified Gödel's system $T$ in the draft of Girard's book about ptykes [Section 12.A;1]. I believe that the details of computations that this leadleads to B-H ordinal had been carried out by Päppinghaus, but I never looked into this details myself [2]. In a sense this approach is just a generalization of "predicative" ordinal notation systems to finite types.

In our recent paper [3] Juan Aguilera, Andreas Weiermann and I defined a functor $B\colon \mathsf{Dil}\to\mathsf{Dil}$ that is very similar to $\Lambda$, but I think that our definition is considerably more compact. For $B$ we have two equivalent definitions. One definition basically is that $B(D)$ is a natural extension of a function $B_{D(\omega)}\colon \omega\to \omega$ from a version of binary fast-growing hierarchy up to $D(\omega)$ to the type $\mathsf{Ord}\to\mathsf{Ord}$. Which demonstrates the functor $B$ to be a variant of recursion along dilators. The other definition of $B$ is in the terms of a term system for certain version of an ordinal collapsing function $\psi$. Thus making aan explicit connection between Girard's idea of tame type 2 bar-recursion and ordinal collapsing. B-H ordinal is $B(\varepsilon^+,0)$, where $\varepsilon^+$ is a naturally defined dilator mapping an ordinal $\alpha$ to the smallest $\varepsilon$-number strictly above $\alpha$.

With regards to what are the limits of the approaches. The limit of the approaches based on recursion on ordinals is B-H ordinal (at least as long as we limit ourselves to finite types). Recursion on dilators seems to be closely connected to collapsing functions and although it have been studied much less than the latter, probably it will have similar limitations (the notation systems for systems that are not too much stronger than $\Pi^1_1\textsf{-CA}_0$ are fairly simple, but the extensions of the approach to $\Pi^1_2\textsf{-CA}_0$ and even weaker systems become quite complicated). I don't know about any works that extend ptyx-based approach beyond recursion on dilators. I have been working on this, but haven't yet published anything about it. There are some indications that it might be possible to reach the ordinal of full second-order arithmetic.

[4] A. Freund. $\Pi^1_2$$\Pi^1_1$-comprehension as a well-ordering principle. Adv. Math., 355, 2019

One way is to allow recursion on ordinals for ptykes for all finite types. Then the supremum of all ordinals describable in this way will be exactly B-H ordinal. See outline of ptyx interpretation of modified Gödel's system $T$ in the draft of Girard's book about ptykes [Section 12.A;1]. I believe that the details of computations that this lead to B-H ordinal had been carried out by Päppinghaus, but I never looked into this details myself [2]. In a sense this approach is just a generalization of "predicative" ordinal notation systems to finite types.

In our recent paper [3] Juan Aguilera, Andreas Weiermann and I defined a functor $B\colon \mathsf{Dil}\to\mathsf{Dil}$ that is very similar to $\Lambda$, but I think that our definition is considerably more compact. For $B$ we have two equivalent definitions. One definition basically is that $B(D)$ is a natural extension of a function $B_{D(\omega)}\colon \omega\to \omega$ from a version of binary fast-growing hierarchy up to $D(\omega)$ to the type $\mathsf{Ord}\to\mathsf{Ord}$. Which demonstrates the functor $B$ to be a variant of recursion along dilators. The other definition of $B$ is in the terms of a term system for certain version of an ordinal collapsing function $\psi$. Thus making a explicit connection between Girard's idea of tame type 2 bar-recursion and ordinal collapsing. B-H ordinal is $B(\varepsilon^+,0)$, where $\varepsilon^+$ is a naturally defined dilator mapping an ordinal $\alpha$ to the smallest $\varepsilon$-number strictly above $\alpha$.

With regards to what are the limits of the approaches. The limit of the approaches based on recursion on ordinals is B-H ordinal (at least as long as we limit ourselves to finite types). Recursion on dilators seems to be closely connected to collapsing functions and although it have been studied much less than the latter, probably it will have similar limitations. I don't know about any works that extend ptyx-based approach beyond recursion on dilators. I have been working on this, but haven't yet published anything about it. There are some indications that it might be possible to reach the ordinal of full second-order arithmetic.

[4] A. Freund. $\Pi^1_2$-comprehension as a well-ordering principle. Adv. Math., 355, 2019

One way is to allow recursion on ordinals for ptykes for all finite types. Then the supremum of all ordinals describable in this way will be exactly B-H ordinal. See outline of ptyx interpretation of modified Gödel's system $T$ in the draft of Girard's book about ptykes [Section 12.A;1]. I believe that the details of computations that this leads to B-H ordinal had been carried out by Päppinghaus, but I never looked into this details myself [2]. In a sense this approach is just a generalization of "predicative" ordinal notation systems to finite types.

In our recent paper [3] Juan Aguilera, Andreas Weiermann and I defined a functor $B\colon \mathsf{Dil}\to\mathsf{Dil}$ that is very similar to $\Lambda$, but I think that our definition is considerably more compact. For $B$ we have two equivalent definitions. One definition basically is that $B(D)$ is a natural extension of a function $B_{D(\omega)}\colon \omega\to \omega$ from a version of binary fast-growing hierarchy up to $D(\omega)$ to the type $\mathsf{Ord}\to\mathsf{Ord}$. Which demonstrates the functor $B$ to be a variant of recursion along dilators. The other definition of $B$ is in the terms of a term system for certain version of an ordinal collapsing function $\psi$. Thus making an explicit connection between Girard's idea of tame type 2 bar-recursion and ordinal collapsing. B-H ordinal is $B(\varepsilon^+,0)$, where $\varepsilon^+$ is a naturally defined dilator mapping an ordinal $\alpha$ to the smallest $\varepsilon$-number strictly above $\alpha$.

With regards to what are the limits of the approaches. The limit of the approaches based on recursion on ordinals is B-H ordinal (at least as long as we limit ourselves to finite types). Recursion on dilators seems to be closely connected to collapsing functions and although it have been studied much less than the latter, probably it will have similar limitations (the notation systems for systems that are not too much stronger than $\Pi^1_1\textsf{-CA}_0$ are fairly simple, but the extensions of the approach to $\Pi^1_2\textsf{-CA}_0$ and even weaker systems become quite complicated). I don't know about any works that extend ptyx-based approach beyond recursion on dilators. I have been working on this, but haven't yet published anything about it. There are some indications that it might be possible to reach the ordinal of full second-order arithmetic.

[4] A. Freund. $\Pi^1_1$-comprehension as a well-ordering principle. Adv. Math., 355, 2019

Source Link
Fedor Pakhomov
Fedor Pakhomov
  • 5.8k
  • 1
  • 21
  • 26

There are at least two fundamentally different ways how one could reach Bachmann-Howard ordinal using dilator and ptykes.

One way is to allow recursion on ordinals for ptykes for all finite types. Then the supremum of all ordinals describable in this way will be exactly B-H ordinal. See outline of ptyx interpretation of modified Gödel's system $T$ in the draft of Girard's book about ptykes [Section 12.A;1]. I believe that the details of computations that this lead to B-H ordinal had been carried out by Päppinghaus, but I never looked into this details myself [2]. In a sense this approach is just a generalization of "predicative" ordinal notation systems to finite types.

The other way is via the recursion on dilators. The intuition is that we want to effectively define set-sized objects, e.g. dilators, by a recursion along a class-sized well-ordering $D(\mathsf{Ord})$, where $D$ is some dilator. This is basically what Girard's functor $\Lambda\colon \mathsf{Dil}\to \mathsf{Dil}$ [Section 9.6,1] does. It is possible to reach B-H ordinal by applying $\Lambda$ to a certain fairly tame dilator. Girard in [1] is proving that the fact that $\Lambda$ maps dilators to dilators is equivalent to $\Pi^1_1\textsf{-}\mathsf{CA}_0$. And he is using $\Lambda$-like functors to perform cut elimination in certain functorial proofs for systems of positive inductive definitions.

In our recent paper [3] Juan Aguilera, Andreas Weiermann and I defined a functor $B\colon \mathsf{Dil}\to\mathsf{Dil}$ that is very similar to $\Lambda$, but I think that our definition is considerably more compact. For $B$ we have two equivalent definitions. One definition basically is that $B(D)$ is a natural extension of a function $B_{D(\omega)}\colon \omega\to \omega$ from a version of binary fast-growing hierarchy up to $D(\omega)$ to the type $\mathsf{Ord}\to\mathsf{Ord}$. Which demonstrates the functor $B$ to be a variant of recursion along dilators. The other definition of $B$ is in the terms of a term system for certain version of an ordinal collapsing function $\psi$. Thus making a explicit connection between Girard's idea of tame type 2 bar-recursion and ordinal collapsing. B-H ordinal is $B(\varepsilon^+,0)$, where $\varepsilon^+$ is a naturally defined dilator mapping an ordinal $\alpha$ to the smallest $\varepsilon$-number strictly above $\alpha$.

There is a number of recent works of Anton Freund on dilators and ptykes, see for example [4]. But the approach that he mostly pursuing is to apply a more traditional proof-theoretic techniques to dilators and ptykes rather than using them directly to define ordinal notation systems.

With regards to what are the limits of the approaches. The limit of the approaches based on recursion on ordinals is B-H ordinal (at least as long as we limit ourselves to finite types). Recursion on dilators seems to be closely connected to collapsing functions and although it have been studied much less than the latter, probably it will have similar limitations. I don't know about any works that extend ptyx-based approach beyond recursion on dilators. I have been working on this, but haven't yet published anything about it. There are some indications that it might be possible to reach the ordinal of full second-order arithmetic.

[1] J.-Y. Girard. Proof Theory and logical complexity, II. Book Draft. https://girard.perso.math.cnrs.fr/ptlc2.pdf

[2] Päppinghaus, Peter. "Ptykes in GödelsT und Definierbarkeit von Ordinalzahlen." Archive for Mathematical Logic 28.2 (1989): 119-141.

[3] Aguilera, J. P., F. Pakhomov, and A. Weiermann. "Functorial Fast-Growing Hierarchies." arXiv preprint arXiv:2201.04536 (2022).

[4] A. Freund. $\Pi^1_2$-comprehension as a well-ordering principle. Adv. Math., 355, 2019