I've only recently learned about Girard's theory of Dilators and Ptykes, and I find this theory very elegant, but it is not clear at all to me whether/how it can be used to produce ordinal notations for all the large recursive ordinals used in proof theory and ordinal analysis. The introduction of several papers on the topic seems to claim it is possible - but I can't find it done anywhere...


I think I can see how Dilators alone can be used to construct (something very similar to) the Veblen functions in (possibly infinitely) many variables and how to get ordinal notations up to maybe the large Veblen ordinal, or a little higher than this.


However - and I have no idea how to make this formal - these constructions feel very "predicative" and my intuition would be that there is some kind of limit to what we can build using these only, I would guess around the Bachmann-Howard ordinal... But maybe I'm wrong and there is a way to formalize something similar to the ordinal collapsing functions using this theory?


General Ptykes on the other hand, feel much more mysterious to me, and I'm not sure how they can be used - I find the literature on the topic doesn't provide many examples - but they do seem more powerful, so I wouldn't be surprised if they could go as high (and probably higher) than everything we get using ordinal collapsing functions... But I don't know how.


Basically, I'd be interested by any reference or answer that gives Dilator/Ptykes based description of Ordinals notations up to and above the Bachman-Howard ordinal. I'd be also interested in results that gives limitations to such methods...



How to build large recursive ordinals using Dillator and/or Ptykes?
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 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.


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 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$.


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 (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.


[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\_1$-comprehension as a well-ordering principle. Adv. Math., 355, 2019


