Recursion on ptykes

In proof theory ordinal analysis of a given formal system is a calculation of a computable ordinal that measures the strength of the system. Results on ordinal analysis are classical and central part of proof theory. The calculation of proof-theoretic ordinal of full second-order arithmetic Z_2 is an open problem that had arised already in the works of G. Gentzen, who had pioneered the field. Since then, the main focus in the works on ordinal analysis were on the fragments of Z_2 and systems that are closely connected to them. J.-Y. Girard had introduced an approach to ordinal analysis based on higher-order (functorial) operators on well-orderings that are known as ptykes. In particular, Girard developed recursion on ptykes in a certain simple case. This already allowed him to describe the proof-theoretic ordinal of Π¹_1-CA_0, which is a relatively strong fragment of Z_2. In this project I plan to develop a general notion of recursion on ptykes. And further, I plan to study several questions that will allow to better understand the connection between Z_2 and this recursion. The grand conjecture is that the proof-theoretic ordinal of Z_2 is the suprema of all ordinals describable in the terms of recursion on ptykes. If the conjecture is indeed true, a proof will be very challenging and represent a major breakthrough in the foundations of mathematics.